mathlib-initiative/mathlib-tactics huggingface dataset:
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,
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.π
          j ≫
        { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.ι
          j =
    𝟙
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
          π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
          ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.pt

Tactic:
by
            dsimp
            ext1 ⟨i, j⟩
            rintro ⟨i', j'⟩
            rw [Finset.sum_apply, Finset.sum_apply]
            dsimp
            rw [Finset.sum_eq_single i]; rotate_left
            · intro b _ hb
              apply Finset.sum_eq_zero
              intro x _
              rw [dif_neg hb.symm, zero_comp]
            · intro hi
              simp at hi
            rw [Finset.sum_eq_single j]; rotate_left
            · intro b _ hb
              rw [dif_pos rfl, dif_neg, zero_comp]
              simp only
              tauto
            · intro hj
              simp at hj
            simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp,
              Sigma.mk.inj_iff, id_def]
            by_cases h : i' = i
            · subst h
              rw [dif_pos rfl]
              simp only [heq_eq_eq, true_and]
              by_cases h : j' = j
              · subst h
                simp
              · rw [dif_neg h, dif_neg (Ne.symm h)]
            · rw [dif_neg h, dif_neg]
              tauto

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : Cardinal.mk K < κ'
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : HasCardinalLT K κ'
⊢ ∃ j, ∀ (k : K), α k ≤ j
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : Cardinal.mk K < κ
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
⊢ ∃ j, ∀ (k : K), α k ≤ j
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
⊢ pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
· exact h

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
let : OrderTop S :=
      { top := ⟨m, by simp [S]⟩
        le_top := by
          rintro ⟨s, hs⟩
          simp only [Set.union_singleton, Set.mem_insert_iff, Set.mem_iUnion, S] at hs
          obtain rfl | ⟨k, hs⟩ := hs
          · simp
          · simp only [Subtype.mk_le_mk]
            exact leOfHom ((by exact terminal.from (C := (α k).val) ⟨_, hs⟩) ≫
              IsCardinalFiltered.toMax _ hK k) }

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
this : OrderTop ↑S := { top := ⟨m, ⋯⟩, le_top := ⋯ }
⊢ ∃ j, ∀ (k : K), α k ≤ j
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
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
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : #K < κ₁
⊢ ∃ j, ∀ (k : K), f k ≤ j

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
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
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : HasCardinalLT K κ₁
⊢ ∃ j, ∀ (k : K), f 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : Cardinal.mk ι < κ
⊢ ∃ j, ∀ (k : ι), D k ≤ j

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt

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

Tactic:
have hD {i : ι} : ¬ (D i).P m := fun hi ↦ (hm₀ i).false ((D i).isTerminal.lift hi)

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
⊢ ∃ j, ∀ (k : ι), D k ≤ j
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f

Tactic:
refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ Presieve.ofArrows Z' π' ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ (Presieve.ofArrows Z' π').FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, ofArrows w✝¹ w✝ f → ∀ {g : Z ⟶ X}, ofArrows w✝¹ w✝ g → HasPullback f g

Tactic:
intro _

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ : C
⊢ ∀ {Z : C} {f : Y✝ ⟶ X}, ofArrows w✝¹ w✝ f → ∀ {g : Z ⟶ X}, ofArrows w✝¹ w✝ g → HasPullback f g
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F

Tactic:
intro _

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F
Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular

Goal state before:
pp: case refine_2
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✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
W : D
f' : W ⟶ F.obj X✝
w✝ : EffectiveEpi f'
i : W ⟶ F.obj Z✝
w : i ≫ F.map g = f' ≫ F.map f
⊢ F.map (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g) = F.map (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f)

Tactic:
simp [w]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (regularCoverage C).coverings X, IsSheafFor (yoneda.obj W) R

Tactic:
intro X S ⟨_, hS⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X : C
S : Presieve X
w✝ : C
hS : ∃ f, (S = ofArrows (fun x ↦ w✝) fun x ↦ f) ∧ EffectiveEpi f
⊢ IsSheafFor (yoneda.obj W) S
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (F.map g.op.toLoc).toFunctor.map φ =
    (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).inv.toNatTrans.app M₁ ≫
      pullHom φ g gf₁ gf₂ hgf₁ hgf₂ ≫ (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).hom.toNatTrans.app M₂

Tactic:
by
  simp [Cat.Hom.comp_toFunctor, pullHom, ← reassoc_of% Cat.Hom₂.comp_app, ← Cat.Hom₂.comp_app]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map
          ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
            (F.map g.op.toLoc).toFunctor.map φ ≫
              (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂) ≫
        (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂

Tactic:
Functor.map_comp_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map
            ((F.map g.op.toLoc).toFunctor.map φ ≫
              (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂) ≫
          (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map
            ((F.map g.op.toLoc).toFunctor.map φ ≫
              (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂) ≫
          (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂

Tactic:
Functor.map_comp_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.map g'.op.toLoc).toFunctor.map ((F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂) ≫
            (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ J S
⊢ (F.toDescentData f).IsEquivalence

Tactic:
rw [← isStackFor_ofArrows_iff, ← IsStackFor_generate_iff]
  exact F.isStackFor _ (by simpa)

Goal state after:
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₃
φ : D₁ ⟶ D₂
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
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (φ.hom i₂)) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
Functor.map_comp_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₃
φ : D₁ ⟶ D₂
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
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
        (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (φ.hom i₂)) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄ (h₁ : (sieve f f' i).arrows f₁)
    (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
g₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
⊢ ∀ ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄ (h₁ : (sieve f f' i).arrows f₁)
    (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
⊢ IsIso (f.hom.app W)

Tactic:
let S : K.Cover W.unop := hX.cover W.unop

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
⊢ IsIso (f.hom.app W)