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

Goal state before:
pp: C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫
        inclusionObj (X'.normalizeObj n) ◁ f ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
ih

Goal state after:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom ≫ inclusion.map (eqToHom ⋯) =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X η').inv ≫
      (inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom) ▷ η' ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X η').inv ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ (normalizeIsoApp' C η' (X.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
ih

Goal state after:
C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X η').inv ≫
      ((normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)) ▷ η' ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X η').inv ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ (normalizeIsoApp' C η' (X.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : X ⟶ Y), (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f

Tactic:
f

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

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

Tactic:
f

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 _ _

Goal state after:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X Q.X L.X).hom ≫
      P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
        (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫
          coequalizer.desc
            ((α_ P.X Q.X L.X).inv ≫
              coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
                coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                  ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft))
            ⋯ =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X Q.X L.X).hom ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      ((PreservesCoequalizer.iso (tensorLeft R.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
          colimMap
            (parallelPairHom (R.X ◁ μ ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (μ ▷ P.X)
              ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
              ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ μ ▷ R.X ▷ P.X)
              ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X) ⋯ ⋯)) ≫
        coequalizer.desc P.actLeft ⋯ =
    R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
slice_lhs 1 4 => rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X) ≫ P.actLeft =
    R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      ((PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
          colimMap
            (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)) (P.actRight ▷ S.X)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
              ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X)
              ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯)) ≫
        coequalizer.desc P.actRight ⋯ =
    R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft

Tactic:
slice_lhs 1 4 => rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ≫ P.actRight =
    R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P.inverseImage F (pres.diag.obj i)
⊢ P.ind.inverseImage F X

Tactic:
simp only [prop_inverseImage_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P.inverseImage F (pres.diag.obj i)
⊢ P.ind (F.obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → P.ind f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ P f → P.ind f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
⊢ ∀ (f : X ⟶ Y), sourceLocalClosure K P f → Q f

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f → Q f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P.localEpi f → P.isoClosure.localEpi f

Tactic:
f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.localEpi f → P.isoClosure.localEpi f
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
k l : Under j₁
a : k ⟶ l
⊢ ((Functor.const (Under j₁)).obj X).map a ≫ s₁.app l.right ≫ pushout.inl ((Under.post D₁).obj l).hom f' =
    (s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f') ≫ D'.map a

Tactic:
have h2 := s₁.naturality a.right
          simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp] at h2
          simp [h2, D']

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
  { app := fun k ↦ s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f', naturality := ⋯ }
k : Under j₁
⊢ s'.app k ≫ c'.ι.app k = p ≫ q

Tactic:
by
      simp [c', s', hcomp, reassoc_of% (h₁ k.right).right]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y : C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ Mono (simpleSubobjectArrow h)

Tactic:
by
  dsimp only [simpleSubobjectArrow]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
Y : C
f : Y ⟶ X
hf : R f
hX : P X
⊢ P Y

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X Y : C
f : Y ⟶ X
hX : P X
𝒰 : K.ZeroHypercover X
hf : Presieve.ofArrows 𝒰.X 𝒰.f f
⊢ P Y
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ P X

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y
⊢ P X
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
⊢ ∀ (f : P ⟶ Y) (e : X ⟶ Y) [Epi e], ∃ f', f' ≫ e = f

Tactic:
f

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
⊢ ∀ (e : X ⟶ Y) [Epi e], ∃ f', f' ≫ e = f
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✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun i j ↦ MulOpposite.unop ((f ≫ g) i j)) = (fun i j ↦ MulOpposite.unop (f i j)) ≫ fun i j ↦ MulOpposite.unop (g i j)

Tactic:
ext
    simp only [Mat_.comp_apply, comp_apply]
    convert! Finset.unop_sum _ _

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}
⊢ ∀ (a : ↑S), a ≤ ⟨m, ⋯⟩

Tactic:
rintro ⟨s, hs⟩

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}
s : ↑J.obj
hs : s ∈ S
⊢ ⟨s, hs⟩ ≤ ⟨m, ⋯⟩
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

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

Tactic:
f

Goal state after:
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
⊢ W f → Function.Bijective fun g ↦ f ≫ g
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) κ₂
K : Type w
j : κ₁.ord.ToType
⊢ ∀ (f : K → ↑(transfiniteIterate (φ Y m) j A)), HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x

Tactic:
f

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) κ₂
K : Type w
j : κ₁.ord.ToType
f : K → ↑(transfiniteIterate (φ Y m) j A)
⊢ HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
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
⊢ Nonempty κ.ord.ToType

Tactic:
simpa using Cardinal.IsRegular.ne_zero Fact.out

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✝ : Preregular C
X Y : C
⊢ ∀ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
      ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
⊢ ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
    ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f
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 ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
      ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f

Tactic:
f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
⊢ ∀ S ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
    ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
R : F.RepresentableBy X
⊢ F.IsRepresentedBy (R.homEquiv (𝟙 X))

Tactic:
by
  rw [IsRepresentedBy.iff_isIso_uliftYonedaEquiv]
  convert!
    (RepresentableBy.equivUliftYonedaIso _ _ <|
        representableByUliftFunctorEquiv.{v}.symm R).isIso_hom
  ext
  simpa [uliftYonedaEquiv] using (homEquiv_eq _ _).symm

Goal state after: