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

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝² x✝¹ x✝ : u ⟶ v
⊢ (x✝² + x✝¹ + x✝).right = (x✝² + (x✝¹ + x✝)).right

Tactic:
simp [add_assoc]

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (x : u ⟶ v), 0 • x = 0

Tactic:
[

Goal state after:
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (x : u ⟶ v), 0 • x = 0
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
[

Goal state after:
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (a : u ⟶ v), 0 • a = 0

Tactic:
[

Goal state after:
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (a : u ⟶ v), 0 • a = 0
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
[

Goal state after:
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
[

Goal state after:
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.snd = (f ≫ biprod.inr) ≫ biprod.snd

Tactic:
simp [Category.assoc]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ (f.comp g).comp h i✝ j✝ = f.comp (g.comp h) i✝ j✝

Tactic:
[

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ (f.comp g).comp h i✝ j✝ = f.comp (g.comp h) i✝ j✝
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 j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ j_1,
      (if h : j_1.fst = j then if h' : h ▸ j_1.snd = x then eqToHom ⋯ else 0 else 0) ≫
        if h : j_1.fst = j' then if h' : h ▸ j_1.snd = y then eqToHom ⋯ else 0 else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
[

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ j_1,
      (if h : j_1.fst = j then if h' : h ▸ j_1.snd = x then eqToHom ⋯ else 0 else 0) ≫
        if h : j_1.fst = j' then if h' : h ▸ j_1.snd = y then eqToHom ⋯ else 0 else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
h : (ConcreteCategory.hom (c.ι.app j)) x = (ConcreteCategory.hom (c.ι.app j)) y
⊢ x = y

Tactic:
obtain ⟨k, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc x y).1 h
        exact (F.map a).injective ha

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.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
      biproduct.desc fun i x k ↦ if h : i = k then eqToHom ⋯ else 0) =
    𝟙 M

Tactic:
by
    simp only [biproduct.lift_desc]
    funext i j
    dsimp [id_def]
    rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]; rotate_left
    · intro b _ hb
      dsimp
      rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_comp]
    · intro h
      simp at h
    simp

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
⊢ HasCardinalLT X κ

Tactic:
obtain rfl : A = .univ := by
    ext x
    have := congr_hom hf x
    dsimp at this
    rw [← this]
    simp

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
hA : HasCardinalLT (↑Set.univ) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨Set.univ, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨Set.univ, hA⟩)) f = 𝟙 X
⊢ HasCardinalLT X κ
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
⊢ ∃ j, ∀ (k : ι), D k ≤ j

Tactic:
let D₂' : DiagramWithUniqueTerminal J κ :=
      { toDiagram := D₂ D hι u
        top := _
        isTerminal := he
        uniq_terminal j hj := by
          have := hj.prop
          simp only [D₂_P] at this
          obtain (⟨i, hi⟩ | rfl) := this
          · exfalso
            exact (hm₀ i).false (hj.lift (by simp) ≫ (D i).isTerminal.lift hi)
          · rfl }

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
⊢ ∃ j, ∀ (k : ι), D k ≤ j
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
⊢ (functor J κ).Final

Tactic:
have := isCardinalFiltered J κ hJ

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
⊢ (functor J κ).Final
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ (fun t ↦ x.IsAmalgamation t) t

Tactic:
convert!
    Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg
    exact (Presieve.restrict_extend hx).symm

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X

Tactic:
intro ⟨α, _, Y, π, hπ⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (coherentTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst✝ : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ EffectiveEpiFamily Z fun a ↦ f a ≫ π a

Tactic:
[

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst✝ : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ EffectiveEpiFamily Z fun a ↦ f a ≫ π a
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝¹ : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
⊢ EqualizerCondition (F.op ⋙ P)

Tactic:
intro X B π _ c hc
  have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp
  refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩
  · simp only [Functor.comp_map, op_map, Quiver.Hom.unop_op, ← map_comp, ← op_comp, c.condition]
  · refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some
    · simp only [← map_comp, c.condition]
    · exact (isLimitMapConePullbackConeEquiv F c.condition)
        (isLimitOfPreserves F (hc.ofIsoLimit (PullbackCone.ext (Iso.refl _) (by simp) (by simp))))

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
⊢ ∀ (i j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ op Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
⟨i⟩

Goal state after:
case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
⊢ ∀ (j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ op Z),
    ∃ a,
      op i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (op 0))

Tactic:
[

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (op 0))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F

Tactic:
by
  dsimp [regularTopology]
  rw [Presheaf.isSheaf_iff_isLimit_coverage]
  constructor
  · rintro hF X _ ⟨Y, f, rfl, _⟩
    exact (equalizerConditionMap_iff_nonempty_isLimit F f).1 (hF f)
  · intro hF Y X f _
    exact (equalizerConditionMap_iff_nonempty_isLimit F f).2 (hF _ ⟨_, f, rfl, inferInstance⟩)

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ m ≫ (F.multifork G).ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op

Tactic:
reassoc_of% hm

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    (pullback.snd (E.toPullback k)
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯))

Tactic:
[

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    (pullback.snd (E.toPullback k)
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i✝ j✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (E.f i✝.fst) (E.f j✝.fst)
          (pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd))
          (pullback.fst (pullback.lift (f.h₀ j✝.fst) (g.h₀ j✝.fst) ⋯) (F.toPullback j✝.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      E.p₁ k.down =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)

Tactic:
this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i✝ j✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (E.f i✝.fst) (E.f j✝.fst)
          (pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd))
          (pullback.fst (pullback.lift (f.h₀ j✝.fst) (g.h₀ j✝.fst) ⋯) (F.toPullback j✝.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst) =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      E.p₂ k.down =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)

Tactic:
this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst) =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)