mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ 𝒮 ≫ Δ * Δ = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ * Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮) = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ Δ ▷ A ≫ (A ⊗ A) ◁ (Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)) ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            A ◁ (β_ A A).hom ▷ A ≫
              A ◁ (α_ A A A).hom ≫
                ((((((A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫ (α_ (A ⊗ A) A A).inv) ≫
                        (α_ A A A).hom ▷ A) ≫
                      (A ◁ μ) ▷ A) ≫
                    μ ▷ A) ≫
                  μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 5 7 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_forward]
    simp only [whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            (((((((A ◁ (α_ A A A).hom ≫ A ◁ (β_ A (A ⊗ A)).hom ≫ A ◁ (α_ A A A).hom) ≫ (α_ A A (A ⊗ A)).inv) ≫
                        (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫
                      (α_ (A ⊗ A) A A).inv) ≫
                    (α_ A A A).hom ▷ A) ≫
                  (A ◁ μ) ▷ A) ≫
                μ ▷ A) ≫
              μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ ≫ 𝒮 * μ = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 ≫ 𝒮 * 𝒮 = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 * 𝟙 A = 1

Tactic:
rw [Conv.mul_eq, Conv.one_eq]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = (Hom.hom (MonoidalCategoryStruct.rightUnitor A).hom) (x ⊗ₜ[R] 1)

Tactic:
rw [MonoidalCategory.rightUnitor_hom_apply, one_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z) =
    (Hom.hom
        ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)

Tactic:
rw [hom_comp, LinearMap.comp_apply, hom_comp, LinearMap.comp_apply, hom_comp,
        LinearMap.comp_apply]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
⊢ { app := fun X ↦ (α.app X).hom, naturality := ⋯ } ≫ Δ =
    Δ ≫ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ⊗ₘ { app := fun X ↦ (α.app X).hom, naturality := ⋯ })

Tactic:
by ext x; dsimp; rw [IsComonHom.hom_comul (α.app x).hom]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: case of_isoClosure
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : P.limitsClosure J X✝
hX' : (P.limitsClosure J).shift a X✝
⊢ (P.limitsClosure J).shift a Y✝

Tactic:
| of_isoClosure e hX hX' =>

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 j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then
          eqToHom ⋯ ≫ if h : x_1.fst = j' then if h' : h ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0
        else 0 ≫ if h : x_1.fst = j' then if h' : h ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0
      else 0 ≫ if h : x_1.fst = j' then if h' : h ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
comp_dite

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').ι
⊢ (∑ x_1,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then
          if h_2 : x_1.fst = j' then if h_3 : ⋯ ▸ x_1.snd = y then eqToHom ⋯ ≫ eqToHom ⋯ else eqToHom ⋯ ≫ 0
          else eqToHom ⋯ ≫ 0
        else if h : x_1.fst = j' then if h_2 : ⋯ ▸ x_1.snd = y then 0 ≫ eqToHom ⋯ else 0 ≫ 0 else 0 ≫ 0
      else if h : x_1.fst = j' then if h_1 : ⋯ ▸ x_1.snd = y then 0 ≫ eqToHom ⋯ else 0 ≫ 0 else 0 ≫ 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
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
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ c,
      ∑ j_1,
        (if h : i = c then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = c then if h' : h ▸ j' = j_1 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:
Finset.sum_eq_single i

Goal state after:
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_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 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'⟩

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 ≠ i →
      (∑ j_1,
          (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
            if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
        0

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').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
⊢ (fun x x_1 ↦ 𝟙 x✝) = 𝟙 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ }

Tactic:
by ext ⟨⟩; simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (fun x x_1 ↦ x✝¹ ≫ x✝) = (fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝

Tactic:
by ext ⟨⟩; simp

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
i j : M.ι
⊢ ∑ c, ((fun j x ↦ if h : j = c then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : c = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

Tactic:
Finset.sum_eq_single i

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ i ∉ Finset.univ →
    ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j = 0
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
⊢ IsRegularEpi (strongEpiMonoFactorisation f).e

Tactic:
dsimp [strongEpiMonoFactorisation]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
⊢ IsRegularEpi (coequalizer.π (pullback.fst f f) (pullback.snd f f))
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P ↑⟨j, hj⟩

Tactic:
exact Or.inl hj

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

Goal state before:
pp: case inr
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 κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
f : m₁ ⟶ m₁
hf : MorphismProperty.ofHoms φ f
⊢ f = 𝟙 m₁

Tactic:
· rw [MorphismProperty.ofHoms_iff] at hf
      obtain ⟨⟨j, hj⟩, hf⟩ := hf
      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
      exact (h₁ hj).elim

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F

Tactic:
rw [extensiveTopology, Presieve.isSheaf_coverage]

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
⊢ IsLocallySurjective φ

Tactic:
let data := (locallySurjective J A).factorizationData (locallyInjective J A) φ

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
⊢ IsLocallySurjective φ
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ᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z)

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 π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
· intro ⟨Z⟩
    obtain ⟨_, f, g, ⟨⟩, hh⟩ := Z.property
    let X' : (Presieve.ofArrows (fun () ↦ X) (fun () ↦ π)).category :=
      Presieve.categoryMk _ π (ofArrows.mk ())
    let f' : Z.obj.left ⟶ X'.obj.left := f
    exact ⟨(ObjectProperty.homMk (Over.homMk f')).op⟩

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 j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a
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
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)
b : E.multicospanShape.R
⊢ t.ι (f.s₀ b.fst.1) ≫ G.map (f.h₁ b.snd ≫ F.p₁ (f.s₁ b.snd)).op =
    t.ι (f.s₀ b.fst.2) ≫ G.map (f.h₁ b.snd ≫ F.p₂ (f.s₁ b.snd)).op

Tactic:
simp only [op_comp, Functor.map_comp]

Goal state after:
case refine_1
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)
b : E.multicospanShape.R
⊢ t.ι (f.s₀ b.fst.1) ≫ G.map (F.p₁ (f.s₁ b.snd)).op ≫ G.map (f.h₁ b.snd).op =
    t.ι (f.s₀ b.fst.2) ≫ G.map (F.p₂ (f.s₁ b.snd)).op ≫ G.map (f.h₁ b.snd).op
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
H : ∀ (i' : ι'), ∃ i p, p ≫ f i = f' i'
⊢ (F.toDescentData f).IsEquivalence

Tactic:
choose α p hp using H

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (F.toDescentData f).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
inst✝ : IsCofiltered N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : fiberMk f₁ = fiberMk f₂
⊢ ∃ V g, p.map g ≫ f₁ = p.map g ≫ f₂

Tactic:
by
  obtain ⟨V, g, hg⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff'
      (colimit.isColimit (p.op ⋙ shrinkYoneda.{w}.obj X)) _ _).1 hf
  refine ⟨V.unop, g.unop, ?_⟩
  simpa [shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}] using hg

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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
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₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ φ ≫ (Triangle.mk (G.map T.mor₁) f g).mor₃ = 0

Tactic:
dsimp
        simp only [homEquiv_unit, Functor.comp_obj] at hφ
        rw [← cancel_mono ((G.commShiftIso (1 : ℤ)).inv.app T.obj₁), assoc, h₂', zero_comp,
          homEquiv_unit, assoc, reassoc_of% hφ, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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
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₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : (adj.homEquiv P✝ T.obj₂) ((adj.homEquiv P✝ T.obj₂).symm ψ) = (adj.homEquiv P✝ T.obj₂) (α ≫ T.mor₁)
⊢ ψ ≫ f = 0

Tactic:
simp only [homEquiv_counit, homEquiv_unit, comp_id,
        Functor.map_comp, unit_naturality_assoc, right_triangle_components] at eq

Goal state after:
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₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
⊢ ψ ≫ f = 0
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₃)) = 𝟙 (op (F.obj (unop X✝).obj₃)) ≫ (F.map f✝.unop.hom₃).op

Tactic:
simp only [id_comp, comp_id]

Goal state after: