Skip to content

Commit

Permalink
chore: classify added instance porting notes (#10884)
Browse files Browse the repository at this point in the history
Classifies by adding issue number (#10754) to porting notes claiming `added instance`.
  • Loading branch information
pitmonticone committed Feb 23, 2024
1 parent 29cdb91 commit 45fab6c
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
6 changes: 3 additions & 3 deletions Mathlib/Geometry/RingedSpace/OpenImmersion.lean
Expand Up @@ -1147,14 +1147,14 @@ image is contained in the image of `f`, we can lift this morphism to a unique `Y
commutes with these maps.
-/
def lift (H' : Set.range g.1.base ⊆ Set.range f.1.base) : Y ⟶ X :=
-- Porting note: added instance manually
-- Porting note (#10754): added instance manually
have := pullback_snd_isIso_of_range_subset f g H'
inv (pullback.snd : pullback f g ⟶ _) ≫ pullback.fst
#align algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift

@[simp, reassoc]
theorem lift_fac (H' : Set.range g.1.base ⊆ Set.range f.1.base) : lift f g H' ≫ f = g := by
-- Porting note: added instance manually
-- Porting note (#10754): added instance manually
haveI := pullback_snd_isIso_of_range_subset f g H'
erw [Category.assoc]; rw [IsIso.inv_comp_eq]; exact pullback.condition
#align algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_fac AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac
Expand All @@ -1165,7 +1165,7 @@ theorem lift_uniq (H' : Set.range g.1.base ⊆ Set.range f.1.base) (l : Y ⟶ X)

theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
Set.range (lift f g H').1.base = f.1.base ⁻¹' Set.range g.1.base := by
-- Porting note: added instance manually
-- Porting note (#10754): added instance manually
have := pullback_snd_isIso_of_range_subset f g H'
dsimp only [lift]
have : _ = (pullback.fst : pullback f g ⟶ _).val.base :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/GroupTheory/SpecificGroups/Alternating.lean
Expand Up @@ -51,7 +51,7 @@ def alternatingGroup : Subgroup (Perm α) :=
sign.ker
#align alternating_group alternatingGroup

-- Porting note: manually added instance
-- Porting note (#10754): manually added instance
instance fta : Fintype (alternatingGroup α) :=
@Subtype.fintype _ _ sign.decidableMemKer _

Expand Down

0 comments on commit 45fab6c

Please sign in to comment.