mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
u : j ⟶ j'
⊢ P.diag.map u ≫ (Q j').isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } } =
    (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } } ≫
      ((Functor.const J).obj c.pt).map u

Tactic:
by
        refine (Q j).isColimit.hom_ext fun i ↦ ?_
        simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id,
          (Q j).isColimit.fac]
        obtain ⟨i', hom, rfl⟩ := Total.exists_hom_of_hom (P := Q) i u
        rw [reassoc_of% hom.w, (Q j').isColimit.fac]
        simpa using c.ι.naturality hom

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
W : Under X
u : CategoryTheory.Under.mk p ⟶ W
v : W ⟶ CategoryTheory.Under.mk f
huv : u ≫ v = CategoryTheory.Under.homMk g hpg
hW : P.underObj W
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

Tactic:
use W.right, u.right, v.right, congr($(huv).right)

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
W : Under X
u : CategoryTheory.Under.mk p ⟶ W
v : W ⟶ CategoryTheory.Under.mk f
huv : u ≫ v = CategoryTheory.Under.homMk g hpg
hW : P.underObj W
⊢ P (p ≫ Under.Hom.right u)
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f - β.f) ≫ G.a = F.a ≫ (α.f - β.f)

Tactic:
by simp only [Functor.map_sub, sub_comp, Monad.Algebra.Hom.h, comp_sub]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f✝ g✝ : u ⟶ v
f g : v ⟶ w
h : LeftHomotopy f g
e : u ⟶ v
⊢ Hom.left (e ≫ f) - Hom.left (e ≫ g) = u.hom ≫ Hom.right e ≫ h.hom

Tactic:
by simp [← reassoc_of% e.w, ← h.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₁ g₂ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ (quotient V).map g₂
⊢ (quotient V).map g₁ = (quotient V).map g₂

Tactic:
set h : RightHomotopy (f ≫ g₁) (f ≫ g₂) := homotopyOfEq _ _ eq

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₁ g₂ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ (quotient V).map g₂
h : RightHomotopy (f ≫ g₁) (f ≫ g₂) := homotopyOfEq (f ≫ g₁) (f ≫ g₂) eq
⊢ (quotient V).map g₁ = (quotient V).map g₂
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
⊢ IsCardinalFiltered (CoconePt hc) κ

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
  refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)
  rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
  choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k)
  let j := IsCardinalFiltered.max j₀ hK
  let x₁ (k : K) : F.obj j := F.map (IsCardinalFiltered.toMax j₀ hK k) (x₀ k)
  have hx₁ (k : K) : c.ι.app j (x₁ k) = c.ι.app (j₀ k) (x₀ k) :=
    ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j₀ hK k)) _
  refine ⟨(cocone hc).ι.app j (IsCardinalFiltered.max x₁ hK),
    fun k ↦ ?_⟩
  rw [← hx₀, ← hx₁]
  exact ((cocone hc).ι.app j).hom.monotone
    (leOfHom (IsCardinalFiltered.toMax x₁ hK k))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
y : (f j).ι
h : x.fst = j
⊢ (fun i j_1 ↦
      { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X i ⟶ (f j).X j_1)
    x y

Tactic:
refine if h' : @Eq.ndrec (Fin n) x.1 (fun j => (f j).ι) x.2 _ h = y then ?_ else 0

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
y : (f j).ι
h : x.fst = j
h' : h ▸ x.snd = y
⊢ (fun i j_1 ↦
      { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X i ⟶ (f j).X j_1)
    x y
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

pp: case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ j ∉ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
      0

pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
· intro b _ hb
              rw [dif_pos rfl, dif_neg, zero_comp]
              simp only
              tauto

Goal state after:
case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ j ∉ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
      0

C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

Tactic:
dif_neg h,

Goal state after:
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ 0 = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ (if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) = if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0

Tactic:
dif_neg h,

Goal state after:
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ 0 = if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : f ≫ g₁ ≫ p.ι.app j₁ = f ≫ g₂ ≫ p.ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv : f ≫ g₁ ≫ p.diag.map u = f ≫ g₂ ≫ p.diag.map v
⊢ g₁ ≫ p.diag.map u ≫ p.ι.app j₃ = g₂ ≫ p.ι.app j₂

Tactic:
← p.w v,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : f ≫ g₁ ≫ p.ι.app j₁ = f ≫ g₂ ≫ p.ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv : f ≫ g₁ ≫ p.diag.map u = f ≫ g₂ ≫ p.diag.map v
⊢ g₁ ≫ p.diag.map u ≫ p.ι.app j₃ = g₂ ≫ p.diag.map v ≫ p.ι.app j₃
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : Preadditive A
x✝ : ℕ
⊢ PreservesBiproductsOfShape (Fin x✝) colim

Tactic:
apply preservesBiproductsOfShape_of_preservesCoproductsOfShape

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
⊢ (ConcreteCategory.hom (f.app (op (Z a))))
      ((ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
        ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
          ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
            ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)))) =
    (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)

Tactic:
have : f.app ⟨Z a⟩ (x a) = G.map (π a).op y := (h' a).choose_spec

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (f.app (op (Z a))))
      ((ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
        ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
          ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
            ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)))) =
    (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).obj.obj (op X))
n : ℕ
⊢ EffectiveEpi ((preimageDiagram hF X y).map (homOfLE ⋯).op)

Tactic:
simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ Presieve.ofArrows (cylinder f g).X (cylinder f g).f ≤
    (Sieve.generate
        (Presieve.bindOfArrows E.X E.f fun i ↦
          (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)).arrows

Tactic:
rintro - - ⟨i⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
Y : C
i : (cylinder f g).I₀
⊢ (Sieve.generate
        (Presieve.bindOfArrows E.X E.f fun i ↦
          (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)).arrows
    ((cylinder f g).f i)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

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
D D₁ D₂ : F.DescentData f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ ⦃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),
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯ =
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom
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
⊢ (F.map f₁.op.toLoc).toFunctor.map (e i₁).inv ≫ D₁.hom q f₁ f₂ ⋯ ⋯ =
    D₂.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).inv

Tactic:
rw [← cancel_mono ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom), Category.assoc,
          Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
          ← cancel_epi ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom),
          Iso.map_hom_inv_id_assoc, comm q f₁ f₂ hf₁ hf₂]

Goal state after:
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)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ S.toPullbackObj P x = S.toPullbackObj P y

Tactic:
ext <;> assumption

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₁.op))
        ((fun x g hg ↦
            (ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
              (f ((ConcreteCategory.hom g) (Classical.choose hg))))
          β f₁ hf₁)) =
    (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₂.op))
        ((fun x g hg ↦
            (ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
              (f ((ConcreteCategory.hom g) (Classical.choose hg))))
          γ f₂ hf₂))

Tactic:
simp_rw [← comp_apply, ← Functor.map_comp, this, ← op_comp]

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map (g ≫ g₁ ≫ ↾fun x ↦ PUnit.unit).op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂))) =
    (ConcreteCategory.hom (S.map (g ≫ g₂ ≫ ↾fun x ↦ PUnit.unit).op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi ((presheafToSheaf J D).map p)

Tactic:
exact ⟨⟨{
      W := (presheafToSheaf J D).obj (pullback f f).obj
      left := (presheafToSheaf J D).map (pullback.fst f f).hom
      right := (presheafToSheaf J D).map (pullback.snd f f).hom
      w := by
        rw [← Functor.map_comp, ← Functor.map_comp]
        congr 1
        rw [← cancel_mono i]
        simp [hpi, ← ObjectProperty.FullSubcategory.comp_hom, pullback.condition]
      isColimit := by
        have := IsRegularEpiCategory.regularEpiOfEpi p
        exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f f))))) }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ Ω₀} {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
intro χ₀' χ' hχ'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' = 𝒞.χ m ≫ eΩ.hom
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀} {χ' : G ⟶ e.functor.obj 𝒞₁.Ω},
    IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth) → χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
intro χ₀' χ' hχ'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

Tactic:
obtain rfl := ha hc hb ((mul_comm _ _).trans h)

Goal state after:
case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
h : b * d = d * d
hc : d ∈ s
⊢ b = d
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ ThreeGPFree ↑(image (invFunOn f ↑A) s)

Tactic:
rw [coe_image]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ ThreeGPFree (invFunOn f ↑A '' ↑s)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ f a * f b = f c * f d ↔ a * b = c * d

Tactic:
simp_rw [← prod_pair]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ {f a, f b}.prod = {f c, f d}.prod ↔ {a, b}.prod = {c, d}.prod