mathlib-initiative/mathlib-tactics huggingface dataset:
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).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 1 3 =>
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]

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).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
⊢ (isCardinalPresentable C κ).ι.isDenseAt X

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
      (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : (isCardinalPresentable C κ).ColimitOfShape J X
⊢ (isCardinalPresentable C κ).ι.isDenseAt X
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
⊢ snd = u ≫ pullback.fst g f'

Tactic:
simp [u]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
⊢ fst ≫ g' = u ≫ pullback.snd g f'

Tactic:
simp [u]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ G.essImage.localEpi = (MorphismProperty.epimorphisms D).inverseImage F

Tactic:
← Functor.isoClosure_eq_essImage,

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ (isoClosure fun x ↦ x ∈ Set.range G.obj).localEpi = (MorphismProperty.epimorphisms D).inverseImage F
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
⊢ (fun z i j k ↦ eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯)
      ((fun z ↦ biproduct.matrix fun j k ↦ if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0) z) (f k)
      ⟨j, w⟩ ⟨k, ⋯⟩ =
    z (f k) ⟨j, w⟩ ⟨k, ⋯⟩

Tactic:
simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
⊢ (if h : f k = g j then z (f k) ⟨j, ⋯⟩ ⟨k, ⋯⟩ ≫ eqToHom ⋯ else 0) ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩
Module: Mathlib.CategoryTheory.Preadditive.Comma

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

Tactic:
by ext <;> simp [add_assoc]

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
by
      { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this✝ : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this✝ a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
this : PartialOrder ↑(Set.range ⇑f) := PartialOrder.lift ⇑e.symm ⋯
e' : ↑(Set.range ⇑f) ≃o ↑J.obj :=
  let __Equiv := e.symm;
  { toEquiv := __Equiv, map_rel_iff' := ⋯ }
⊢ ↑(CardinalDirectedPoset.ι.obj J) ≃o
    ↑(CardinalDirectedPoset.ι.obj (ι ⟨Set.range ⇑f, ⟨inferInstance, { down := { down := ⋯ } }⟩⟩))

Tactic:
by exact e'.symm

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

Goal state before:
pp: case neg
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').ι
h : ¬i' = i
⊢ 0 = if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0

Tactic:
dif_neg

Goal state after:
case neg
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').ι
h : ¬i' = i
⊢ 0 = 0

case neg.hnc
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').ι
h : ¬i' = i
⊢ ¬(i = i' ∧ j ≍ j')
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case pos
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 : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
i j : X.ι
h : j = i
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i

Tactic:
subst h; simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
⊢ (fun i j ↦ MulOpposite.unop (𝟙 X i j)) = 𝟙 (FintypeCat.of X.ι)

Tactic:
ext
    simp only [Mat_.id_def, id_def]
    split_ifs <;> rfl

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:
rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
    have hκ' : Cardinal.aleph0 ≤ κ' := Cardinal.IsRegular.aleph0_le Fact.out
    refine ⟨⟨(⋃ (k : K), α k) ∪ {⊤},
      hasCardinalLT_union hκ' (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).property.left))
        (hasCardinalLT_of_finite _ _ hκ'), by simp⟩, fun k ↦ ?_⟩
    rw [Subtype.mk_le_mk]
    exact subset_trans (Set.subset_iUnion (fun i ↦ (α i).1) k) Set.subset_union_left

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
ι : Type (w + 1) := (J : Type w) × (x : SmallCategory J) × { F // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun x ↦
    match x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
x✝ : ⊤ X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : J ⥤ P.FullSubcategory := P.lift p.diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
⊢ (ofObj φ).isoClosure X

Tactic:
have : HasColimit p.diag := ⟨_, p.isColimit⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
ι : Type (w + 1) := (J : Type w) × (x : SmallCategory J) × { F // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun x ↦
    match x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
x✝ : ⊤ X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : J ⥤ P.FullSubcategory := P.lift p.diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this : HasColimit p.diag
⊢ (ofObj φ).isoClosure X
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
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
g : Z ⟶ T
⊢ ∃ a, (fun g ↦ toSucc W Z ≫ g) a = g

Tactic:
· choose f hf using fun (d : D₁ W Z) ↦ (hT d.1.1.hom d.1.2).2 (d.2 ≫ g)
    exact ⟨Multicoequalizer.desc _ _ (fun ⟨⟩ ↦ pushout.desc (Sigma.desc f) g)
      (fun d ↦ (hT d.1.1.hom d.1.2).1 (by simp [reassoc_of% d.2.2])), by simp⟩

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

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

Tactic:
choose Y hY hY' using fun (B : Set X) hB ↦ h B hB

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
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)
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
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₁ g₂ : Y ⟶ H.F.obj j
h : f ≫ g₁ ≫ H.incl.app j = f ≫ g₂ ≫ H.incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk : (f ≫ g₁) ≫ H.F.map u = (f ≫ g₂) ≫ H.F.map u
hg : g₁ ≫ H.F.map u ≫ (iteration W Z κ).map (homOfLE ⋯) = g₂ ≫ H.F.map u ≫ (iteration W Z κ).map (homOfLE ⋯)
this : H.F.map (u ≫ homOfLE ⋯) ≫ H.incl.app (Order.succ k) = H.incl.app j
⊢ g₁ ≫ H.F.map u ≫ H.F.map (homOfLE ⋯) ≫ H.incl.app (Order.succ k) =
    g₂ ≫ H.F.map u ≫ H.F.map (homOfLE ⋯) ≫ H.incl.app (Order.succ k)

Tactic:
rw [reassoc_of% hg]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ (Presieve.ofArrows X₂ π₂).FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
rintro _ _ ⟨b⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
Y : C
b : β
⊢ ∃ W i e, Presieve.ofArrows X₁ π₁ e ∧ i ≫ e = π₂ b ≫ f
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ ((adjunction J adj).unit.app X).hom =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj ≫ whiskerRight (toSheafify J (X.obj ⋙ G)) F

Tactic:
change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _
  simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
    Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app,
    sheafificationAdjunction_unit_app, whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app,
    Functor.comp_map, Functor.map_id, whiskerRight_id', Category.comp_id]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
by cases h; exact hπ.2 _

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

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
this :
  generate (Presieve.ofArrows X fun i ↦ Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ (Presieve.ofArrows X fun i ↦ Sigma.ι X i) ∈ (extensiveCoverage C ⊔ regularCoverage C).coverings (∐ X)

Tactic:
refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩

Goal state after:
case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
this :
  generate (Presieve.ofArrows X fun i ↦ Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ IsIso (Sigma.desc fun i ↦ Sigma.ι X i)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))

Tactic:
specialize hP π _ hc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP : Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))
hc : IsLimit c
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : (extensiveCoverage C).Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → (extensiveCoverage C).Saturate Y (Sieve.pullback f S)
a : ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, w, Y₁, π, h, h'⟩ := a
      choose β _ Y_n π_n H using fun a => b (h' a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
        fun c => (H c.fst).2 c.snd⟩

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
⊢ F.IsCoverDense (coherentTopology D)

Tactic:
by
  refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
  apply Coverage.Saturate.of
  refine ⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B,
    fun _ => F.effectiveEpiOver B, ?_, ?_⟩
  · funext; ext -- Do we want `Presieve.ext`?
    refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
    rintro ⟨⟩
    simp
  · rw [← effectiveEpi_iff_effectiveEpiFamily]
    infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)

Tactic:
let X' := S.categoryMk π ⟨_, 𝟙 _, π, ofArrows.mk (), Category.id_comp _⟩

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)
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
X Y : C
𝒰 : J.ZeroHypercover X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
⊢ f = g

Tactic:
have hs : 𝒰.presieve₀.IsSheafFor (yoneda.obj Y) :=
    (GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor_of_mem_precoverage
      𝒰.mem₀

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.toGrothendieck.Subcanonical
X Y : C
𝒰 : J.ZeroHypercover X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
hs : Presieve.IsSheafFor (yoneda.obj Y) 𝒰.presieve₀
⊢ f = g
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)

Tactic:
presheafHom_map_app _ _ W.hom (by simp)

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ (x g hg).app (op (Over.mk W.hom)) = (x g hg).app (op W)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
⊢ (fun f ↦
        {
          app := fun j ↦
            uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
          naturality := ⋯ })
      ((fun g ↦ end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯) g) =
    g

Tactic:
by
    dsimp
    ext j
    dsimp
    simp only [uncurry_curry, end_.lift_π]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
⊢ ∀ {x y z : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous z → x.IsCohomologous z

Tactic:
rintro γ₁ γ₂ γ₂ ⟨α, h⟩ ⟨β, h'⟩
    exact ⟨_, h.trans h'⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
K : Type u_1
inst✝ : Category.{v_1, u_1} K
⊢ ∀ {K_1 : K ⥤ C}, PreservesLimit K_1 J.yoneda

Tactic:
intro F
    have : PreservesLimitsOfShape K (J.yoneda ⋙ sheafToPresheaf J (Type v)) :=
      preservesLimitsOfShape_of_natIso (yonedaCompSheafToPresheaf J).symm
    exact preservesLimit_of_reflects_of_preserves (F := J.yoneda) (G := sheafToPresheaf ..)

Goal state after: