mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ inv f.snd = (inv f).snd

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ f.snd ≫ (inv f).snd = 𝟙 x.snd
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro X Y ⟨f⟩
    exact Quotient.sound (comp_id f)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Quotient.map₂ Hom.tensor ⋯ f₁ f₂ ≫ Quotient.map₂ Hom.tensor ⋯ g₁ g₂ = Quotient.map₂ Hom.tensor ⋯ (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
by
    rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩
    exact Quotient.sound (tensorHom_comp_tensorHom _ _ _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.α_inv
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X Y Z : F C
⊢ motive ⟦Hom.α_inv X Y Z⟧

Tactic:
| α_inv X Y Z =>

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.tensor
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
⊢ motive ⟦f.tensor g⟧

Tactic:
have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
      change motive (homMk f ⊗ₘ homMk g)
      rw [this]
      exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝

Tactic:
hf,

Goal state after:
case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ { app := fun X ↦ ↾pure, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝))

Tactic:
by ext; exact joinM_pure _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsIso (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))

Tactic:
rw [← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsSplitMono (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R

Tactic:
exact NatIso.ofComponents (fun _ ↦ asIso (adj.unit.app ((ihom _).obj _)))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⊗ (ihom A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((ihom A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj ((ihom A).obj B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj ((ihom A).obj B)
e_4✝ : F.obj (A ⊗ (ihom A).obj B) = ((curriedTensor C).obj A ⋙ F).obj ((ihom A).obj B)
⊢ inv (prodComparison F A ((ihom A).obj B)) = (prodComparisonNatIso F A).inv.app ((ihom A).obj B)

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
case e'_3.e'_6
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⊗ (ihom A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((ihom A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj ((ihom A).obj B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj ((ihom A).obj B)
e_4✝ : F.obj (A ⊗ (ihom A).obj B) = ((curriedTensor C).obj A ⋙ F).obj ((ihom A).obj B)
⊢ prodComparison F A ((ihom A).obj B) ≫ (prodComparisonNatIso F A).inv.app ((ihom A).obj B) =
    𝟙 (F.obj (A ⊗ (ihom A).obj B))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: case e'_3.e'_7.e'_8
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (ihom (F.obj A)).obj (F.obj (A ⊗ B)) = (ihom (F.obj A)).obj (((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ inv (prodComparison F A B) = (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B)

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
case e'_3.e'_7.e'_8
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (ihom (F.obj A)).obj (F.obj (A ⊗ B)) = (ihom (F.obj A)).obj (((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B) = 𝟙 (F.obj (A ⊗ B))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : F C
f g : X ⟶ Y
⊢ f = g

Tactic:
have hfg : (fullNormalize C).map f = (fullNormalize C).map g := Subsingleton.elim _ _
    have hf := NatIso.naturality_2 (fullNormalizeIso.{u} C) f
    have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g
    exact hf.symm.trans (Eq.trans (by simp only [Functor.comp_map, hfg]) hg)

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

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ 𝒮 ▷ A ≫ A ◁ 𝒮 ≫ μ = ε ≫ η

Tactic:
← comm,

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ 𝒮 ▷ A ≫ A ◁ 𝒮 ≫ (β_ A A).hom ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) (x ⊗ₜ[R] z + y ⊗ₜ[R] z)

Tactic:
← TensorProduct.add_tmul

Goal state after:
case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) ((x + y) ⊗ₜ[R] z)
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 W Z : C
g : Y ⟶ Z
f : X ⟶ Z
fst : W ⟶ X
snd : W ⟶ Y
h : IsPullback fst snd f g
hf : sourceLocalClosure K P f
⊢ sourceLocalClosure K P snd

Tactic:
induction hf generalizing W snd with
    | of f' hf' => exact .of _ (P.of_isPullback h hf')
    | of_iso f' g' e hf' ih =>
      exact ih _ (g ≫ e.inv.right) (fst ≫ e.inv.left) _ (h.paste_horiz (.of_horiz_isIso ⟨e.inv.w⟩))
    | comp f' hf' R hR g' hg' ih =>
      let u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') (by simp [h.w.symm])
      have : snd = u ≫ pullback.fst g f' := by simp [u]
      rw [this] at h ⊢
      let e : W ≅ pullback g' (pullback.snd g f') :=
        IsPullback.isoPullback (.of_bot h (by simp [u]) (.flip <| .of_hasPullback _ _))
      rw [← (sourceLocalClosure K P).cancel_left_of_respectsIso e.inv, ← Category.assoc]
      refine .comp _ (ih _ _ _ _ (.flip (.of_hasPullback _ _))) _
        (K.pullbackArrows_mem (pullback.snd _ _) hR) _ ?_
      simpa [e, u] using .mk _ _ hg'
    | of_presieve f R hR h ih =>
      refine .of_presieve _ _ (K.pullbackArrows_mem fst hR) ?_
      intro U v ⟨Z, u, hu⟩
      exact ih _ _ hu _ g (pullback.fst _ _) _ (.paste_vert (.of_hasPullback _ _) h)

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

Goal state before:
pp: case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
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
S : Presieve X✝
hS : S ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), S g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)

Tactic:
rw [K.mem_iff_exists_zeroHypercover] at hS hR

Goal state after:
case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
U✝ : C
g : U✝ ⟶ X✝
hg : R g
S : Presieve X✝
hS : ∃ 𝒰, S = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ (U : C) (g : U ⟶ X✝), S g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
have := Subobject.subsingleton_of_isZero hX

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
this : Subsingleton (Subobject X)
⊢ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
have := Subobject.subsingleton_of_isZero hX

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
this : Subsingleton (Subobject X)
⊢ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).hom ≫ (isoMk fun i ↦ β_ (X i) ((Y ⊗ Z) i)).hom ≫ (α_ Y Z X).hom) i =
    ((isoMk fun i ↦ β_ (X i) (Y i)).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (isoMk fun i ↦ β_ (X i) (Z i)).hom) i

Tactic:
apply hexagon_forward

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Tactic:
by
  split_ifs with h
  · exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h
  · exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x : CoconePt hc
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = x), x' ≤ y'

Tactic:
by
    obtain ⟨j, x', hx⟩ := Types.jointly_surjective_of_isColimit hc x
    exact ⟨j, x', x', hx, hx, le_rfl⟩

Goal state after:
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 ⋯)
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j

Tactic:
simp only [homOfLE_leOfHom, Category.assoc] at hg

Goal state after:
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 ⋯)
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app 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)
Y : C
a : α
⊢ pullback.snd f (π a) ≫ π a = π' a ≫ f

Tactic:
rw [CategoryTheory.Limits.pullback.condition]

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

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
dsimp only [pointwiseCocone_pt]

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_1
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 :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
⊢ (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) a

Tactic:
ext
    simpa [mapToEqualizer] using! ha₁

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

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.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
· rw [mem_inducedTopology_iff_of_isCoverDense] at hS
    obtain ⟨Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpi _).mp hS
    let g₀ := F.effectiveEpiOver Y
    refine ⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : S.arrows (F.preimage _))⟩
    · refine F.effectiveEpi_of_map _ ?_
      simp only [map_preimage]
      infer_instance
    · obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂
      rw [h₂]
      convert! S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))
      exact F.map_injective (by simp)

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
· intro hP
    apply EqualizerCondition.mk
    intro X B π _ _
    rw [mapToEqualizer_eq_comp, ← isIso_iff_bijective]
    infer_instance

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ (Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z)

Tactic:
intro ⟨Z⟩

Goal state after:
case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
⊢ Nonempty (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ op Z)