mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h

Goal state after:
case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : HasCardinalFilteredGenerator C κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
P : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ P, ∃ (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ

Tactic:
exact ⟨P.map F, inferInstance, adj.isCardinalFilteredGenerator hP⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ((biproduct.desc fun i x k ↦ if h : i = k then eqToHom ⋯ else 0) ≫
      biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) =
    𝟙 (⨁ fun i ↦ (embedding C).obj (M.X i))

Tactic:
apply biproduct.hom_ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ∀ (j : M.ι),
    ((biproduct.desc fun i x k ↦ if h : i = k then eqToHom ⋯ else 0) ≫
          biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.π (fun i ↦ (embedding C).obj (M.X i)) j =
      𝟙 (⨁ fun i ↦ (embedding C).obj (M.X i)) ≫ biproduct.π (fun i ↦ (embedding C).obj (M.X i)) j
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case e_a.e_a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom =
    (α.app (X✝.X j)).hom ≫ ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))

Tactic:
apply biproduct.hom_ext

Goal state after:
case e_a.e_a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ ∀ (j_1 : ((embedding C).obj (Y✝.X k)).ι),
    (L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
        biproduct.π (fun i ↦ F.obj (((embedding C).obj (Y✝.X k)).X i)) j_1 =
      ((α.app (X✝.X j)).hom ≫ ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
        biproduct.π (fun i ↦ F.obj (((embedding C).obj (Y✝.X k)).X i)) j_1
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
x✝ : IsCardinalPresentable J κ'
⊢ HasCardinalLT (↑J.obj) κ'

Tactic:
obtain ⟨X, f, hf⟩ :=
    IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J κ')
      (ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom))

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
x✝ : IsCardinalPresentable J κ'
X : Subtype (J.PropSetWithTop κ')
f : J ⟶ (functorOfPredicateSet (J.PropSetWithTop κ')).obj X
hf : f ≫ (J.coconeWithTop κ').ι.app X = ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom)
⊢ HasCardinalLT (↑J.obj) κ'
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredColimits C κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J W.isLocal.ι

Tactic:
have := W.isClosedUnderColimitsOfShape_isLocal J κ hW
    have := HasCardinalFilteredColimits.hasColimitsOfShape C κ J
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
d : D₁ W Z
⊢ Sigma.ι D₁.obj₂ d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Sigma.ι D₁.obj₂ d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)

Tactic:
simp only [Category.assoc] at hf

Goal state after:
case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι D₁.obj₂ d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Sigma.ι D₁.obj₂ d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ (Presieve.ofArrows Z' π').FactorsThruAlong S f

Tactic:
· intro W g hg
      rcases hg with ⟨a⟩
      refine ⟨Z a, pullback.snd _ _, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩
      rw [hS]
      exact Presieve.ofArrows.mk a

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, ofArrows w✝¹ w✝ f → ∀ {g : Z ⟶ X}, ofArrows w✝¹ w✝ g → HasPullback f g

Tactic:
intro _ _ _ _ _ hg

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : ofArrows w✝¹ w✝ f✝
g✝ : Z✝ ⟶ X
hg : ofArrows w✝¹ w✝ g✝
⊢ HasPullback f✝ g✝
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
⊢ ⊤.arrows (𝟙 Y)

Tactic:
simp only [Sieve.top_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)

Tactic:
obtain ⟨rfl, _⟩ := h

Goal state after:
case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
⊢ ∀ (x : Unit → F.obj (op Y)),
    Arrows.Compatible F (fun x ↦ f) x → ∃! t, ∀ (i : Unit), (ConcreteCategory.hom (F.map f.op)) t = x i

Tactic:
refine fun x hx ↦ ⟨F.map (Projective.factorThru (𝟙 _) f).op <| x (), fun _ ↦ ?_, fun y h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x ↦ f) x
x✝ : Unit
⊢ (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map (Projective.factorThru (𝟙 X) f).op)) (x ())) = x x✝

case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x ↦ f) x
y : (fun X ↦ X) (F.obj (op X))
h : (fun t ↦ ∀ (i : Unit), (ConcreteCategory.hom (F.map f.op)) t = x i) y
⊢ y = (ConcreteCategory.hom (F.map (Projective.factorThru (𝟙 X) f).op)) (x ())
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁) ≫
      pullHom (pullHom' D₂.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) p f₁ f₂ ⋯ ⋯ =
    pullHom (pullHom' D₁.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) p f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
pullHom'_p₁_p₂,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁) ≫ pullHom (D₂.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ =
    pullHom (pullHom' D₁.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) p f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ =
    𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (D.obj i))

Tactic:
by
    obtain ⟨p, h₁, h₂⟩ := (sq i i).isPullback.exists_lift (𝟙 _) (𝟙 _) (by simp)
    have : p ≫ (sq i i).p = f i := by rw [← (sq i i).hp₁, reassoc_of% h₁]
    rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]
    all_goals cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
h : Z ⟶ X
w : f ≫ g = h
α : (presheafHom F G).obj (op X)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map g.op)) α).app (op (Over.mk f)) = α.app (op (Over.mk h))

Tactic:
subst w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map g.op)) α).app (op (Over.mk f)) = α.app (op (Over.mk (f ≫ g)))
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) =
    (ConcreteCategory.hom ((presheafHom F G).map (𝟙 Z₂.left).op)) (x (Z₂.hom ≫ g) hZ₂)
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ a = b

Tactic:
by simpa only [← cancel_mono sq.f₃₄] using fac

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ x✝⁻¹ * x✝ = 1

Tactic:
by ext; apply inv_mul_cancel

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

Goal state before:
pp: case hunique
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
intro y₁ y₂ hy₁ hy₂
    rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂
    apply NatTrans.ext
    ext ⟨Y : Over X⟩
    apply (hG Y.hom).hom_ext
    rintro ⟨Z : Over Y.left, hZ⟩
    dsimp
    let φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom
    refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))
    rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾(J.overMapPullback A (f ≫ g).unop).map = ↾(J.overMapPullback A f.unop).map ≫ ↾(J.overMapPullback A g.unop).map

Tactic:
by
    ext φ : 4
    exact ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_comp f g) φ.1

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
X : C
⊢ Mono (S.ι.app X)

Tactic:
exact ConcreteCategory.mono_of_injective _ Subtype.val_injective

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f'
⊢ (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x) =
    (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯))

Tactic:
← NatTrans.naturality_apply,

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f'
⊢ (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x) =
    (ConcreteCategory.hom (m.app (Opposite.op Z))) ((ConcreteCategory.hom (F.map f'.op)) (⋯.amalgamate a ⋯))
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case right
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
⊢ Function.Surjective fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h

Tactic:
intro φ
        obtain ⟨ψ, hψ⟩ := Triangle.coyoneda_exact₁ _ mem (φ ≫ G.map T.mor₃ ≫
          (G.commShiftIso (1 : ℤ)).hom.app T.obj₁) (by
            dsimp
            rw [assoc, assoc, ← G.commShiftIso_hom_naturality, ← G.map_comp_assoc,
              comp_distTriang_mor_zero₃₁ _ hT, G.map_zero, zero_comp, comp_zero])
        dsimp at ψ hψ
        obtain ⟨α, hα⟩ : ∃ α, α = φ - ψ ≫ adj.homEquiv _ _ h := ⟨_, rfl⟩
        have hα₀ : α ≫ G.map T.mor₃ = 0 := by
          rw [hα, sub_comp, ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).hom.app T.obj₁),
            assoc, sub_comp, assoc, assoc, hψ, zero_comp, sub_eq_zero,
            ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).inv.app T.obj₁), assoc,
            assoc, assoc, assoc, h₂', Iso.hom_inv_id_app, comp_id]
        suffices ∃ (β : Y ⟶ Z), β ≫ adj.homEquiv _ _ h = α by
          obtain ⟨β, hβ⟩ := this
          refine ⟨ψ + β, ?_⟩
          dsimp
          rw [add_comp, hβ, hα, add_sub_cancel]
        obtain ⟨β, hβ⟩ := T.coyoneda_exact₃ hT ((adj.homEquiv _ _).symm α)
          ((adj.homEquiv _ _).injective (by simpa [homEquiv_unit, homEquiv_counit] using hα₀))
        refine ⟨adj.homEquiv _ _ β ≫ f, ?_⟩
        simpa [homEquiv_unit, h₁'] using congr_arg (adj.homEquiv _ _).toFun hβ.symm

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
this : BijOn f A (f '' A)
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Tactic:
simp +contextual only
    [((hf.bijOn.injOn.mono hAs).bijOn_image (f := f)).forall,
    hf.mul_eq_mul (hAs _) (hAs _) (hAs _) (hAs _), this.injOn.eq_iff]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = b → a = c

Tactic:
rintro rfl
    exact (add_left_cancel habc).symm

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ mulRothNumber {a} = 1

Tactic:
refine ThreeGPFree.mulRothNumber_eq ?_
  rw [coe_singleton]
  exact threeGPFree_singleton a

Goal state after: