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

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

Tactic:
intro f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
f : X ⟶ Y
⊢ biprod.lift f 0 = f ≫ biprod.inl
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

Tactic:
intro f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.desc 0 f = biprod.snd ≫ f
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

Tactic:
intro f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
f : X ⟶ Y
⊢ biprod.desc f 0 = biprod.fst ≫ f
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
⊢ ∀ (w : X ⟶ X), ∃ c, c • 𝟙 X = w

Tactic:
intro f

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
⊢ ∃ c, c • 𝟙 X = f
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ 𝟙 M i i = 𝟙 (M.X i)

Tactic:
by simp [id_apply]

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

Goal state before:
pp: 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 : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ (biproduct.ι (fun i ↦ F.obj ((embedding C).obj (M.X i))) j ≫
      (additiveObjIsoBiproduct F M).inv ≫ F.map f ≫ F.map fun j x ↦ if h : j = i then eqToHom ⋯ else 0) =
    biproduct.ι (fun i ↦ F.obj ((embedding C).obj (M.X i))) j ≫ biproduct.desc fun j ↦ F.map ((embedding C).map (f j i))

Tactic:
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
    biproduct.ι_desc, ← F.map_comp]

Goal state after:
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 : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ F.map ((fun x k ↦ if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x ↦ if h : j = i then eqToHom ⋯ else 0) =
    F.map ((embedding C).map (f j i))
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : Mat R
i : M.obj
⊢ 𝟙 M i i = 1

Tactic:
by simp [id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : HasCardinalLT (↑B) κ₂
⊢ B ⊆ φ₀ Y m B hB

Tactic:
intro b hb
    obtain ⟨C, hC, hC'⟩ := hY' B hB ⟨{⟨b, hb⟩},
      hasCardinalLT_of_finite _ _ (IsRegular.aleph0_le Fact.out)⟩
    refine Set.subset_iUnion _ ⟨C, hC⟩ (Or.inl ?_)
    simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
    exact ⟨hb, @hC' ⟨b, hb⟩ (by simp)⟩

Goal state after:
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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ
c : Multicofork index := cocone index.multispan hshape
i₁ i₂ : ι
j : J
h₁ : (D i₁).P j
h₂ : (D i₂).P j
⊢ (D i₁).isTerminal.lift h₁ ≫ (fun i ↦ u i ≫ c.π PUnit.unit) i₁ =
    (D i₂).isTerminal.lift h₂ ≫ (fun i ↦ u i ≫ c.π PUnit.unit) i₂

Tactic:
simpa [index, shape] using c.condition ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩

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

Goal state before:
pp: case inl.inl
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 : D.W f
⊢ f = 𝟙 m₁

Tactic:
exact (h₁ (D.src hf)).elim

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ (α_ M.X Y.X N.X).hom ≫
      M.X ◁ coequalizer.π (μ ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
        M.X ◁ coequalizer.desc N.actLeft ⋯ ≫
          colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
slice_lhs 2 3 => rw [← whiskerLeft_comp, coequalizer.π_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ (α_ M.X Y.X N.X).hom ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∃ α x, ∃ (_ : IsCardinalFiltered α κ), ∃ F, F.Final

Tactic:
have := isFiltered_of_isCardinalFiltered κ.ord.ToType κ
  obtain ⟨α, _, _, F, _⟩ :=
    exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
        have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)
  exact ⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) ≫
        (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom ≫ (F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M) ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).r.toFunctor.map
          ((F.map (f i₂).op.toLoc).l.toFunctor.map ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))

Tactic:
Adj.unit_naturality

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M : ↑(F.obj { as := op S }).obj
i₁ i₂ i₃ : ι
⊢ (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.obj ((F.map (f i₃).op.toLoc).l.toFunctor.obj M))) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map
      ((F.map (f i₃).op.toLoc).adj.unit.toNatTrans.app M ≫
        (F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
          ((F.map (f i₃).op.toLoc).r.toFunctor.1 ((F.map (f i₃).op.toLoc).l.toFunctor.obj M)))
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
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map (f.h₀ (g.s₀ i)).op ≫ G.map (g.h₀ i).op = t.ι i

Tactic:
← Functor.map_comp,

Goal state after:
case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map ((f.h₀ (g.s₀ i)).op ≫ (g.h₀ i).op) = t.ι i
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
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι i ≫ G.map (F.p₂ (hgf.H i)).op ≫ G.map (hgf.a i).op = t.ι i

Tactic:
← Functor.map_comp,

Goal state after:
case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι i ≫ G.map ((F.p₂ (hgf.H i)).op ≫ (hgf.a i).op) = t.ι i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S✝ : ?m.2
S : C
inst✝ : HasPullbacks C
X Y : J.HOneHypercover S
f g : X.as ⟶ Y.as
W : J.OneHypercover S
h : W.Hom X.as
H : Homotopy (Hom.comp h f) (Hom.comp h g)
⊢ (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map f =
    (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map g

Tactic:
← Functor.map_comp,

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S✝ : ?m.2
S : C
inst✝ : HasPullbacks C
X Y : J.HOneHypercover S
f g : X.as ⟶ Y.as
W : J.OneHypercover S
h : W.Hom X.as
H : Homotopy (Hom.comp h f) (Hom.comp h g)
⊢ (toHOneHypercover J S).map (h ≫ f) = (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map g
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
rw [heq]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (H'.isoPullback.inv ≫ ⋯.isoPullback.hom)
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
⊢ FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor

Tactic:
rintro ⟨X⟩
  let ι (X : C) := Shrink.{max u v} (𝒮 X)
  let t (X : C) (i : ι X) : F.obj (Opposite.op X) := ((equivShrink _).symm i).val
  have (x : F.obj (.op X)) (hx : K.SubsheafClosure 𝒮 X x) :
      ∃ (i : Witness K ι X), Witness.eval hF _ t i = x := by
    induction hx with
    | base ha => exact ⟨.base _ (equivShrink _ ⟨_, ha⟩), by grind [Witness.eval]⟩
    | restrict f ha ih =>
      obtain ⟨i, hi⟩ := ih
      use .restrict f i
      grind [Witness.eval]
    | amalgamate hR hy hmem ht ih =>
      choose x hx using ih
      exact ⟨.amalgamate hR x, by simp [Witness.eval, hx]; grind⟩
  choose i hi using this
  have : Function.Injective (fun x : { x // K.SubsheafClosure 𝒮 X x } ↦ i x x.prop) := by
    intro x y hxy
    ext
    apply Option.some_injective
    simp [← hi _ x.prop, ← hi _ y.prop, hxy]
  exact small_of_injective this

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
⊢ (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:
have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
        Classical.choose_spec hf₁ (g₁ <| g x) ▸
          Classical.choose_spec hf₂ (g₂ <| g x) ▸ ConcreteCategory.congr_hom h _

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.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₂))