mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m) 0) 0 = (f 1) ![m]

Tactic:
foldl_ι,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (((LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f 0) 0 = (f 1) ![m]
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
⊢ Function.Injective ⇑f

Tactic:
simpa [f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
T : Type w
inst✝¹ : Unique T
F : C ⥤ Discrete T
inst✝ : IsConnected C
⊢ F.Initial

Tactic:
rwa [← isConnected_iff_initial_of_unique F]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
this : IsSiftedOrEmpty C
⊢ IsSifted C

Tactic:
have := nonempty_of_colim_preservesLimitsOfShapeFinZero C

Goal state after:
C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
this✝ : IsSiftedOrEmpty C
this : Nonempty C
⊢ IsSifted C
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
this✝ : IsIso (𝟙 T)
this : (map₂ f (𝟙 T)).Final
⊢ (map f).Final

Tactic:
apply final_of_natIso (mapIsoMap₂ f).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
          (x, x')).1 =
      (m, m').1 ∧
    ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
          (x, x')).2 =
      (m, m').2
⊢ ∃ U x x', ιM x = m ∧ ιM x' = m'

Tactic:
obtain ⟨rfl, rfl⟩ := h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 x_1 x'_1,
    ιM x_1 =
        ((ConcreteCategory.hom
              ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
            (x, x')).1 ∧
      ιM x'_1 =
        ((ConcreteCategory.hom
              ((((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).ι.app U))
            (x, x')).2
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
          (a, x)).1 =
      (r, m).1 ∧
    ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
          (a, x)).2 =
      (r, m).2
⊢ ∃ U a x, (ιR cR) a = r ∧ ιM x = m

Tactic:
obtain ⟨rfl, rfl⟩ := h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 a_1 x_1,
    (ιR cR) a_1 =
        ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
            (a, x)).1 ∧
      ιM x_1 =
        ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
            (a, x)).2
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv (f ≫ F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
partialRightAdjointHomEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.map f ≫ F.partialRightAdjointHomEquiv (F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g.hom
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑(M₁.obj X✝)) (n : ↑(M₂.obj X✝)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (f ≫ g))) (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n) =
      (ModuleCat.Hom.hom
          (tensorObjMap M₁ M₂ f ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
                (tensorObjMap M₁ M₂ g) ≫
              (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map g))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (f ≫ g))) ⋯).inv.app
                (M₁.obj Z✝ ⊗ M₂.obj Z✝)))
        (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n)

Tactic:
intro m₁ m₂
    dsimp [tensorObjMap]
    simp +instances

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
T : C
u : T ⟶ S
hu : Presieve.ofArrows (fun p ↦ Y p.fst p.snd) (fun x ↦ g x.fst x.snd ≫ f x.fst) u
⊢ Presieve.ofArrows (fun p ↦ Y (incl p.fst) (fibincl p.fst p.snd))
    (fun p ↦ g (incl p.fst) (fibincl p.fst p.snd) ≫ f (incl p.fst)) u

Tactic:
exact .mk' ⟨Sum.inr ⟨⟨_, _⟩, hu⟩, .inl ⟨⟩⟩ hu.obj_idx.symm hu.eq_eqToHom_comp_hom_idx

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C = ⊤

Tactic:
apply le_antisymm
      · exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)
      · intro X S _
        apply Set.mem_univ

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
I : S.shape.R
⊢ P.map I.fst.f.op ≫ P.map I.r.g₁.op = P.map I.snd.f.op ≫ P.map I.r.g₂.op

Tactic:
simp only [← P.map_comp, ← op_comp, I.r.w]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (S.index P)
I : S.shape.R
⊢ P.map I.fst.f.op ≫ P.map I.r.g₁.op = P.map I.snd.f.op ≫ P.map I.r.g₂.op

Tactic:
simp only [← P.map_comp, ← op_comp, I.r.w]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Tactic:
by
  funext W
  ext h
  constructor
  · rintro ⟨W, _, _, _⟩
    exact singleton.mk
  · rintro ⟨_⟩
    exact pullbackArrows.mk Z g singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h

Tactic:
· rintro ⟨W, k, ⟨_⟩⟩
    apply ofArrows.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ (ofArrows U fun x ↦ g x ≫ f) ≤ pushforward f (ofArrows U g)

Tactic:
rw [ofArrows_le_iff]
    intro i
    use g i, rfl
    exact ⟨i⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
intro t₁ t₂ ht₁ ht₂

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap
        (J.diagramNatTrans
          { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ } (unop X)) =
    colimit.ι (J.diagram P (unop X)) S ≫
      ⊤.toMultiequalizer (J.plusObj P) ≫ colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)

Tactic:
let e : S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap
        (J.diagramNatTrans
          { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ } (unop X)) =
    colimit.ι (J.diagram P (unop X)) S ≫
      ⊤.toMultiequalizer (J.plusObj P) ≫ colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map φ.op))
      ((ConcreteCategory.hom (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁)) =
    (ConcreteCategory.hom (P.map φ.op))
      ((ConcreteCategory.hom (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂))
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
simp only [← comp_apply, ← Functor.map_comp, ← op_comp] at this

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((sheafify J G).toFunctor.map f_1 ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
      (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map f_1

Tactic:
by
    intro U V i
    ext s
    apply (h _ ((Subfunctor.sheafify J G).toFunctor.map i s).prop).isSeparatedFor.ext
    intro W j hj
    refine (Presieve.IsSheafFor.valid_glue (h _ ((G.sheafify J).toFunctor.map i s).2)
      ((G.family_of_elements_compatible _).map _) _ hj).trans ?_
    dsimp
    simp only [← comp_apply, ← Functor.map_comp]
    change _ = F'.map (j ≫ i.unop).op _
    refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
    · simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]
      rfl
    · dsimp [Presieve.FamilyOfElements.map] at hj ⊢
      rwa [Functor.map_comp, comp_apply]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)))

Tactic:
simp only [continuous_def, isOpen_iff_of_isColimit _ hc]

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ (∀ (s : Set X), IsOpen s → ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' f ⁻¹' s)) ↔
    ∀ (j : J) (s : Set X), IsOpen s → IsOpen (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' s)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) =
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Tactic:
by
  ext x
  constructor
  · rintro ⟨y, rfl⟩
    simp only [← ConcreteCategory.comp_apply, Set.mem_ofPred_eq]
    simp [pullback.condition]
  · rintro (h : f (_, _).1 = g (_, _).2)
    use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
    apply Concrete.limit_ext
    rintro ⟨⟨⟩⟩ <;>
      rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
      -- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
      cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂

Tactic:
apply (TopCat.mono_iff_injective _).mp H₃

Goal state after:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom i₃) ((ConcreteCategory.hom f₁) x₁) = (ConcreteCategory.hom i₃) ((ConcreteCategory.hom f₂) x₂)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
convert! H₂.comp (snd_isOpenEmbedding_of_left H₁ g)

Goal state after:
case e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom (pullback.snd f g))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U

Tactic:
refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩

Goal state after:
case mpr.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(y, x), eq⟩ ∈
    ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U

case mpr.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(y, x), eq⟩) = x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U

Tactic:
rintro ⟨y, hy, rfl⟩
    exact
      ⟨(pullback.snd f g) y, hy,
        (CategoryTheory.congr_fun pullback.condition y).symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k ↦ X ↑k
ι : Unit → I := fun x ↦ i
⊢ Mono (c.inj i)

Tactic:
have hι : Function.Injective ι := fun _ _ _ ↦ rfl

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k ↦ X ↑k
ι : Unit → I := fun x ↦ i
hι : Function.Injective ι
⊢ Mono (c.inj i)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
⊢ ∀ (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
αX

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
⊢ ∀ (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right

Tactic:
simp only [Cocone.w]

Goal state after: