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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
r : ℤ
α : F ⟶ G
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a

Tactic:
rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable X κ
⊢ IsCardinalPresentable Y κ

Tactic:
have := adj.isCardinalPresentable_leftAdjoint_obj κ X

Goal state after:
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable X κ
this : IsCardinalPresentable (F.obj X) κ
⊢ IsCardinalPresentable Y κ
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
a : ↑J.withTop.obj
⊢ ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S

Tactic:
induction a with
  | some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩
  | none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩

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

Goal state before:
pp: 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)
⊢ W.isLocal.isLocal (toSucc W Z)

Tactic:
refine fun T hT ↦ ⟨fun φ₁ φ₂ h ↦ ?_, fun g ↦ ?_⟩
  · ext ⟨⟩
    simp only [Category.assoc] at h
    dsimp
    ext d
    · apply (hT d.1.1.hom d.1.2).1
      simp only [← D₁.ι_comp_t_assoc, pushout.condition_assoc, h]
    · exact h
  · 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.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 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
i₁ i₂ : ι
j : J
left✝¹ : (D (i₁, i₂, j).1).P (i₁, i₂, j).2.2
right✝¹ : (D (i₁, i₂, j).2.1).P (i₁, i₂, j).2.2
i₁' i₂' : ι
j' : J
left✝ : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right✝ : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h : i₁ = i₁' ∧ i₂ = i₂' ∧ ⟨j, right✝¹⟩ ≍ ⟨j', right✝⟩
⊢ ⟨(i₁, i₂, j), ⋯⟩ = ⟨(i₁', i₂', j'), ⋯⟩

Tactic:
obtain rfl : i₁ = i₁' := h.1

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
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 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
i₁ i₂ : ι
j : J
left✝¹ : (D (i₁, i₂, j).1).P (i₁, i₂, j).2.2
right✝¹ : (D (i₁, i₂, j).2.1).P (i₁, i₂, j).2.2
i₂' : ι
j' : J
left✝ : (D (i₁, i₂', j').1).P (i₁, i₂', j').2.2
right✝ : (D (i₁, i₂', j').2.1).P (i₁, i₂', j').2.2
h : i₁ = i₁ ∧ i₂ = i₂' ∧ ⟨j, right✝¹⟩ ≍ ⟨j', right✝⟩
⊢ ⟨(i₁, i₂, j), ⋯⟩ = ⟨(i₁, i₂', j'), ⋯⟩
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✝⁶ : 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 : X ⟶ H.F.obj j
⊢ ∃ a, (fun g ↦ f ≫ g) a = g ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j

Tactic:
obtain ⟨g', hg'⟩ := iteration_map_succ_surjectivity f hf g

Goal state after:
case refine_2
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 : X ⟶ H.F.obj j
g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)
hg' : f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)
⊢ ∃ a, (fun g ↦ f ≫ g) a = g ≫ { pt := reflectionObj W Z κ, ι := H.incl }.ι.app j
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
⊢ IsFilteredOrEmpty (HasCardinalLT.Set X κ)

Tactic:
by
    have : IsDirectedOrder (HasCardinalLT.Set X κ) :=
      ⟨fun A B ↦ ⟨⟨A.val ∪ B.val, hasCardinalLT_union hκ A.prop B.prop⟩,
        Set.subset_union_left, Set.subset_union_right⟩⟩
    exact isFilteredOrEmpty_of_directed_le _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsSmall.{w, v, u} W
inst✝¹ : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
inst✝ : HasColimitsOfSize.{w, w, v, u} C
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
have : Nonempty κ.ord.ToType := by simpa using Cardinal.IsRegular.ne_zero Fact.out

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsSmall.{w, v, u} W
inst✝¹ : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
inst✝ : HasColimitsOfSize.{w, w, v, u} C
this : Nonempty κ.ord.ToType
⊢ W.isLocal.ι.IsRightAdjoint
Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent

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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ ∀ (b : β),
    (fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b)) b ≫ π₁ (i b) =
      (fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b)) b ≫ f

Tactic:
intro b
      apply F.map_injective
      simp [hh b]

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

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ (extensiveCoverage C).coverings X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)

Tactic:
obtain ⟨α, _, Y, π, h, h'⟩ := hS
      refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
      · have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using! h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩
      · obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F

Tactic:
isSheaf_iff_preservesFiniteProducts_of_projective,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ PreservesFiniteProducts F ↔ IsSheaf (extensiveTopology C) F
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ᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
⊢ ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
    (G.obj.map I₁.f.op ≫ inv (f.hom.app (op I₁.Y))) ≫ F.obj.map r.g₁.op =
      (G.obj.map I₂.f.op ≫ inv (f.hom.app (op I₂.Y))) ≫ F.obj.map r.g₂.op

Tactic:
by
      intro I₁ I₂ r
      have hZ : IsIso (f.hom.app (op r.Z)) := by
        obtain ⟨i, ⟨g⟩⟩ := I₁.hf
        exact hiso r.Z i (r.g₁ ≫ g)
      simp only [Category.assoc, f.hom.naturality_inv]
      rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]

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
s : ↑(presheafHom F G).sections
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    F.map f ≫ (↑s Y).app (op (Over.mk (𝟙 (unop Y)))) = (↑s X).app (op (Over.mk (𝟙 (unop X)))) ≫ G.map f

Tactic:
by
        rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f : X₂ ⟶ X₁⟩
        dsimp
        refine Eq.trans ?_ ((s.1 ⟨X₁⟩).naturality
          (Over.homMk f : Over.mk f ⟶ Over.mk (𝟙 X₁)).op)
        rw [← s.2 f.op]
        dsimp
        rw [presheafHom_map_app_op_mk_id]
        rfl

Goal state after:
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
M : ↑(F.obj { as := op S })
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 ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (f' i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app ((F.map p.op.toLoc).toFunctor.obj M) ≫
        (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app ((F.map p.op.toLoc).toFunctor.obj M) =
    pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M)

Tactic:
rw [F.isoMapOfCommSq_eq _ _ rfl, F.isoMapOfCommSq_eq _ _ rfl]

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
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
M : ↑(F.obj { as := op S })
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
        (((F.mapComp' p.op.toLoc (f' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).symm ≪≫
                  F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app
          M) ≫
      (F.mapComp' (f' i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app ((F.map p.op.toLoc).toFunctor.obj M) ≫
        (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app ((F.map p.op.toLoc).toFunctor.obj M) =
    pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map
        (((F.mapComp' p.op.toLoc (f' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).symm ≪≫
                  F.mapComp' (f (α i₂)).op.toLoc (p' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).inv.toNatTrans.app
          M)
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
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
Z✝ : C
a✝ : F.obj (Opposite.op Z✝)
ha : a✝ ∈ 𝒮 Z✝
⊢ Witness.eval hF ι t (Witness.base Z✝ ((equivShrink ↑(𝒮 Z✝)) ⟨a✝, ha⟩)) = some a✝

Tactic:
grind [Witness.eval]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: case h
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) := ⋯
t : (X : C) → ι X → F.obj (Opposite.op X) := ⋯
x : F.obj (Opposite.op X)
Z✝ W✝ : C
f : Z✝ ⟶ W✝
a✝ : F.obj (Opposite.op W✝)
ha : K.SubsheafClosure 𝒮 W✝ a✝
i : Witness K ι W✝
hi : Witness.eval hF ι t i = some a✝
⊢ Witness.eval hF ι t (Witness.restrict f i) = some ((ConcreteCategory.hom (F.map f.op)) a✝)

Tactic:
grind [Witness.eval]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ b₂✝ b₃✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
h : b₂✝ ⟶ b₃✝
⊢ (Cat.Hom.isoMk (J.overMapPullbackComp A h.unop (f ≫ g).unop).symm).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackComp A g.unop f.unop).symm).hom
          (J.overMapPullback A h.unop).toCatHom ≫
        (Bicategory.associator (J.overMapPullback A f.unop).toCatHom (J.overMapPullback A g.unop).toCatHom
              (J.overMapPullback A h.unop).toCatHom).hom ≫
          Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
              (Cat.Hom.isoMk (J.overMapPullbackComp A h.unop g.unop).symm).inv ≫
            (Cat.Hom.isoMk (J.overMapPullbackComp A (g ≫ h).unop f.unop).symm).inv =
    eqToHom ⋯

Tactic:
ext1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ b₂✝ b₃✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
h : b₂✝ ⟶ b₃✝
⊢ ((Cat.Hom.isoMk (J.overMapPullbackComp A h.unop (f ≫ g).unop).symm).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackComp A g.unop f.unop).symm).hom
            (J.overMapPullback A h.unop).toCatHom ≫
          (Bicategory.associator (J.overMapPullback A f.unop).toCatHom (J.overMapPullback A g.unop).toCatHom
                (J.overMapPullback A h.unop).toCatHom).hom ≫
            Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
                (Cat.Hom.isoMk (J.overMapPullbackComp A h.unop g.unop).symm).inv ≫
              (Cat.Hom.isoMk (J.overMapPullbackComp A (g ≫ h).unop f.unop).symm).inv).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (J.overMapPullbackComp A f.unop (𝟙 b₀✝).unop).symm).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₀✝))).hom
          (J.overMapPullback A f.unop).toCatHom ≫
        (Bicategory.leftUnitor (J.overMapPullback A f.unop).toCatHom).hom =
    eqToHom ⋯

Tactic:
ext1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (J.overMapPullbackComp A f.unop (𝟙 b₀✝).unop).symm).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₀✝))).hom
            (J.overMapPullback A f.unop).toCatHom ≫
          (Bicategory.leftUnitor (J.overMapPullback A f.unop).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (J.overMapPullbackComp A (𝟙 b₁✝).unop f.unop).symm).hom ≫
      Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
          (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₁✝))).hom ≫
        (Bicategory.rightUnitor (J.overMapPullback A f.unop).toCatHom).hom =
    eqToHom ⋯

Tactic:
ext1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (J.overMapPullbackComp A (𝟙 b₁✝).unop f.unop).symm).hom ≫
        Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
            (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₁✝))).hom ≫
          (Bicategory.rightUnitor (J.overMapPullback A f.unop).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).hom } ≫ { hom := (equivYoneda S.obj ⋯).inv } = 𝟙 S

Tactic:
ext1

Goal state after:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ ({ hom := (equivYoneda S.obj ⋯).hom } ≫ { hom := (equivYoneda S.obj ⋯).inv }).hom = (𝟙 S).hom
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).inv } ≫ { hom := (equivYoneda S.obj ⋯).hom } =
    𝟙 (yoneda'.obj (S.obj.obj (op PUnit.{u + 1})))

Tactic:
ext1

Goal state after:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ ({ hom := (equivYoneda S.obj ⋯).inv } ≫ { hom := (equivYoneda S.obj ⋯).hom }).hom =
    (𝟙 (yoneda'.obj (S.obj.obj (op PUnit.{u + 1})))).hom
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: X : Type u
⊢ yoneda'.map
        ((NatIso.ofComponents
                (fun _α ↦
                  { hom := ↾fun x ↦ ↾fun x_1 ↦ x, inv := ↾fun f ↦ (TypeCat.Hom.hom f) PUnit.unit, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ })
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun S ↦ equivYoneda' S) ⋯).symm.hom.app (yoneda'.obj X) =
    𝟙 (yoneda'.obj X)

Tactic:
ext1

Goal state after:
X : Type u
⊢ (yoneda'.map
          ((NatIso.ofComponents
                  (fun _α ↦
                    { hom := ↾fun x ↦ ↾fun x_1 ↦ x, inv := ↾fun f ↦ (TypeCat.Hom.hom f) PUnit.unit, hom_inv_id := ⋯,
                      inv_hom_id := ⋯ })
                  ⋯).hom.app
            X) ≫
        (NatIso.ofComponents (fun S ↦ equivYoneda' S) ⋯).symm.hom.app (yoneda'.obj X)).hom =
    (𝟙 (yoneda'.obj X)).hom
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝))

Tactic:
rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_map, ← MonCat.hom_comp, ← p.naturality,
      MonCat.hom_comp, ← Submonoid.map_map]
    grw [S.map_le]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X : C
φ : X ⟶ 𝒞.Ω
⊢ IsPullback (pullback.fst φ 𝒞.truth) ?m.52 φ 𝒞.truth

Tactic:
convert! IsPullback.of_hasPullback φ 𝒞.truth

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
    (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
        (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
      x₁ = y₁

Tactic:
simpa using! (mono_iff_injective (m.app X)).mp (inferInstance)

Goal state after: