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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
c : C
v : V
f g : (F ⊛ G).obj c ⟶ v
h : ∀ {x y : C} (u : x ⊗ y ⟶ c), (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g
j : CostructuredArrow (tensor C) c
⊢ ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ f =
    ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ g

Tactic:
by simpa using h j.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
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ P.underObj.ind (CategoryTheory.Under.mk f)

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ P.ind f

Tactic:
· refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
    · exact { app j := CategoryTheory.Under.homMk (s.app j) (by simp [hst]) }
    · have : Nonempty J := IsFiltered.nonempty
      exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs
    · simp [underObj, hst]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ P.ind f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) → localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))

Tactic:
rintro h _ ⟨Z, rfl⟩ u v huv
    obtain ⟨u, rfl⟩ := G.map_surjective u
    obtain ⟨v, rfl⟩ := G.map_surjective v
    simp only [← G.map_comp, G.map_injective_iff, cancel_epi] at huv
    rw [huv]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isNoetherianObject Y✝
⊢ isNoetherianObject X✝

Tactic:
by
    rw [← isNoetherianObject.is_iff] at hY ⊢
    exact isNoetherianObject_of_mono f

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str

Tactic:
rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim j

Goal state after:
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 g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
have h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (f +ₗ h) (g +ₗ k) := by
    ext <;> simp [reassoc_of% hd₁, reassoc_of% hd₂]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
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
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

Tactic:
apply eqToHom

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
⊢ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X x = (f j).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
j : Fin n
x : (f j).ι
y : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
h : y.fst = j
h' : h ▸ y.snd = x
⊢ (fun i j_1 ↦
      (f j).X i ⟶ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X j_1)
    x y

Tactic:
apply eqToHom

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)

Tactic:
dsimp [φ]

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom f) x =
    (ConcreteCategory.hom (c.ι.app m)) ((ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x))
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : 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
⊢ B ⊆ φ Y m B

Tactic:
dsimp [φ]

Goal state after:
κ₁ κ₂ : 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
⊢ B ⊆ if hB : HasCardinalLT (↑B) κ₂ then φ₀ Y m B hB else B
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : κ.ord.ToType
g₁ : Y ⟶ H.F.obj j₁
j₂ : κ.ord.ToType
g₂ : Y ⟶ H.F.obj j₂
h :
  (fun g ↦ f ≫ g) (g₁ ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j₁) =
    (fun g ↦ f ≫ g) (g₂ ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j₂)
⊢ ∃ j g₁' g₂',
    g₁' ≫ H.incl.app j = g₁ ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j₁ ∧
      g₂' ≫ H.incl.app j = g₂ ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j₂

Tactic:
exact ⟨max j₁ j₂, g₁ ≫ H.F.map (homOfLE (le_max_left _ _)),
        g₂ ≫ H.F.map (homOfLE (le_max_right _ _)), by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
⊢ IsIso (uliftYonedaEquiv.symm { down := x })

Tactic:
by
    rwa [IsRepresentedBy.iff_isIso_uliftYonedaEquiv] at h

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ι : Cardinal.mk ι < κ
⊢ ∃ j, ∀ (k : ι), D k ≤ j

Tactic:
rw [← hasCardinalLT_iff_cardinal_mk_lt] at hι
    obtain ⟨m, u, hm₀, hm⟩ := isCardinalFiltered_aux J κ hJ D hι
    let φ (x : (Σ (i : ι), (Subtype (D i).P))) : x.2.1 ⟶ m :=
      (D x.1).isTerminal.lift x.2.2 ≫ u x.1
    have hD {i : ι} : ¬ (D i).P m := fun hi ↦ (hm₀ i).false ((D i).isTerminal.lift hi)
    let he : (D₂ D hι u).IsTerminal m := by
      have H {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f) :
          f = φ ⟨i, ⟨_, hj⟩⟩ := by
        simp only [D₂_W] at hf
        obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := hf
        · simp only [MorphismProperty.iSup_iff] at hf
          obtain ⟨i, hf⟩ := hf
          exact (hD ((D i).tgt hf)).elim
        · exact (hD hj).elim
        · apply hm
      refine .ofExistsUnique ?_ ?_ ?_ ?_
      · exact Or.inl (Or.inr ⟨⟨⟩⟩)
      · simp only [D₂_P, D₂_W]
        rintro j (⟨i, hi⟩ | rfl)
        · exact ⟨φ ⟨i, _, hi⟩, Or.inr (.mk _)⟩
        · exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩
      · intro j hj l₁ l₂ hl₁ hl₂
        simp only [D₂_P] at hj
        obtain (⟨i, hj⟩ | rfl) := hj
        · obtain rfl := H hj hl₁
          obtain rfl := H hj hl₂
          rfl
        · rw [eq_id_of_D₂_W D hι u hD hl₁, eq_id_of_D₂_W D hι u hD hl₂]
      · rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨i, j, hj⟩⟩)
        · simp only [Diagram.iSup_W, MorphismProperty.iSup_iff] at hf
          obtain ⟨i, hf⟩ := hf
          exact ⟨φ ⟨i, j, (D i).src hf⟩, φ ⟨i, k, (D i).tgt hf⟩, Or.inr ⟨_⟩, Or.inr ⟨_⟩,
            by simp [φ, (D i).isTerminal.comm_assoc _ hf]⟩
        · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
        · refine ⟨φ ⟨i, j, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp [φ]⟩
    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 }
    refine ⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩
    · exact le_trans (le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left) le_sup_left
    · exact le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left

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

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

Tactic:
have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using! h'

Goal state after:
case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ Nonempty (IsColimit (Cofan.mk X π))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

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

Tactic:
Iso.map_hom_inv_id_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom =
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

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

Tactic:
obtain ⟨(g : X.1 ⟶ Y.1), rfl⟩ := (toHOneHypercover J S).map_surjective g

Goal state after:
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 h, h ≫ (toHOneHypercover J S).map f = 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₀),
    isomorphisms C (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
isomorphisms.iff

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₀),
    IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft 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₁).hom ≫
      (F.map f₁.op.toLoc).toFunctor.map (e i₁).inv ≫ D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom =
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯

Tactic:
Iso.map_hom_inv_id_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
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
⊢ D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom =
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ p ≫ (sq i₁ i₂).p = ?m.156

Tactic:
← (sq i₁ i₂).hp₁,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ p ≫ (sq i₁ i₂).p₁ ≫ f i₁ = ?m.156
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : autoParam (f₁ ≫ f' j₁ = q) pullFunctorObjHom_eq._auto_1
hf₂ : autoParam (f₂ ≫ f' j₂ = q) pullFunctorObjHom_eq._auto_3
hq' : autoParam (q ≫ p = q') pullFunctorObjHom_eq._auto_5
hf₁' : autoParam (f₁ ≫ p' j₁ = f₁') pullFunctorObjHom_eq._auto_7
hf₂' : autoParam (f₂ ≫ p' j₂ = f₂') pullFunctorObjHom_eq._auto_9
⊢ f₁' ≫ f (α j₁) = q'

Tactic:
by rw [← hq', ← hf₁', Category.assoc, w, reassoc_of% hf₁]

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

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

Tactic:
rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ ⟨f : Y ⟶ X⟩ ⟨g : Z ⟶ Y⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ↾(Over.map (op f ≫ op g).unop).op.whiskerLeft =
    ↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫ ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft
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
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
⊢ S.SheafCondition F.obj

Tactic:
rw [sheafCondition_iff_comp_coyoneda]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
⊢ ∀ (X : Aᵒᵖ), S.SheafCondition (F.obj ⋙ coyoneda.obj X)
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)
X : C
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))

Tactic:
let ι (X : C) := Shrink.{max u v} (𝒮 X)

Goal state after:
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)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))
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:
by
  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: