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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p = h.p

Tactic:
by
  rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ { f // F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f } ≃
    { g // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g }

Tactic:
refine (adj.homEquiv _ _).subtypeEquiv ?_

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (a : F.obj A.A ⟶ B),
    F.map A.a ≫ a = adj.counit.app (F.obj A.A) ≫ a ↔
      G.map (F.map ((adj.homEquiv A.A B) a)) ≫ G.map (adj.counit.app B) = A.a ≫ (adj.homEquiv A.A B) a
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
x✝¹ x✝ : Transported e
⊢ μ e.inverse x✝¹ x✝ ≫ e.inverse.map (e.functor.mapIso (β_ (e.inverse.obj x✝¹) (e.inverse.obj x✝))).hom =
    (β_ (e.inverse.obj x✝¹) (e.inverse.obj x✝)).hom ≫ μ e.inverse x✝ x✝¹

Tactic:
simp +instances [fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]

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'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
⊢ IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
have w₁ : (coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c = (adj.homEquiv _ _).symm ∘
        (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) ∘ adj.homEquiv _ _ := by ext; simp

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'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
⊢ g ≫ (m • x) = g ≫ m • g ≫ x

Tactic:
rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ (αₗ N M X).inv ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ (αₗ M M X).hom ≫ M ⊴ₗ γ = N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X

Tactic:
← actionHomLeft_action_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ e₁.inv ⊵ₗ (M ⊙ₗ X) ≫ M ⊴ₗ γ = N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ A ⨯ A ≅ A

Tactic:
letI := IsSubterminal.isIso_diag hA

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
this : IsIso (diag A) := isIso_diag hA
⊢ A ⨯ A ≅ A
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
⊢ (α_ R.X (P.X ⊗ Q.X) L.X).inv ≫
      (α_ R.X P.X Q.X).inv ▷ L.X ≫
        (((α_ (R.X ⊗ P.X) Q.X L.X).hom ≫ P.actLeft ▷ (Q.X ⊗ L.X)) ≫
            P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫
          coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
            ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
              P.X ◁ TensorBimod.actLeft Q L) =
    R.X ◁ (α_ P.X Q.X L.X).hom ≫
      R.X ◁ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
        (α_ R.X P.X (Q.tensorBimod L).X).inv ≫
          P.actLeft ▷ (Q.tensorBimod L).X ≫
            coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
              ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)

Tactic:
slice_rhs 2 3 => erw [associator_inv_naturality_right]

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
⊢ (α_ R.X (P.X ⊗ Q.X) L.X).inv ≫
      (α_ R.X P.X Q.X).inv ▷ L.X ≫
        (((α_ (R.X ⊗ P.X) Q.X L.X).hom ≫ P.actLeft ▷ (Q.X ⊗ L.X)) ≫
            P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫
          coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
            ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
              P.X ◁ TensorBimod.actLeft Q L) =
    R.X ◁ (α_ P.X Q.X L.X).hom ≫
      (((α_ R.X P.X (Q.X ⊗ L.X)).inv ≫
            (R.X ⊗ P.X) ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫
          P.actLeft ▷ (Q.tensorBimod L).X) ≫
        coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).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
⊢ (λ_ (R.X ⊗ P.X)).inv ≫
      η ▷ (R.X ⊗ P.X) ≫
        ((α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
          coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))

Tactic:
slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]

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
⊢ (λ_ (R.X ⊗ P.X)).inv ≫
      η ▷ (R.X ⊗ P.X) ≫
        (α_ R.X R.X P.X).inv ≫ μ ▷ P.X ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
obtain ⟨a', u, hu⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.coeqHom f.base g.base)

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ ∃ Z h, f ≫ h = g ≫ h
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
x✝ : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable Z
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ ∃ W u v, u ≫ v = g ∧ P W

Tactic:
have : IsFinitelyPresentable Z := hZ

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
x✝ : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable Z
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P (pres.diag.obj i)
this : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P W
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
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'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ sourceLocalClosure K P ((e.inv ≫ u) ≫ pullback.fst g f')

Tactic:
refine .comp _ (ih _ _ _ _ (.flip (.of_hasPullback _ _))) _
        (K.pullbackArrows_mem (pullback.snd _ _) hR) _ ?_

Goal state after:
case comp
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'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ Presieve.pullbackArrows (pullback.snd g f') R (e.inv ≫ u)
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Y ⟶ T
huv : (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v
⊢ u = v

Tactic:
obtain ⟨u, rfl⟩ := (hg _ hT).surjective u

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
v : Y ⟶ T
u : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) v
⊢ (fun g_1 ↦ g ≫ g_1) u = v
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂

Tactic:
obtain ⟨l₂, a', b', h₄⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
          (hy₁.trans hy₂.symm)

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₁ W Z)

Tactic:
dsimp [D₁]
  infer_instance

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

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂

Tactic:
induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    have := Cardinal.nonempty_ord_toType (c := κ₁) (IsRegular.ne_zero Fact.out)
    let := WellFoundedLT.toOrderBot κ₁.ord.ToType
    simpa [hj.eq_bot]
  | succ j hj hj' =>
    have hκ₂ : κ₂.IsRegular := Fact.out
    rw [transfiniteIterate_succ _ _ _ hj, φ_eq _ _ _ hj']
    refine hasCardinalLT_iUnion _ (hY _ _)
      (fun ⟨C, hC⟩ ↦ hasCardinalLT_union hκ₂.aleph0_le ?_
        (hasCardinalLT_of_finite _ _ hκ₂.aleph0_le))
    refine (C.prop.of_le h₀.le).of_injective (fun ⟨c, hc⟩ ↦ ?_)
      (fun c₁ c₂ hc ↦ ?_)
    · simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at hc
      exact ⟨⟨c, hc.choose⟩, hc.choose_spec⟩
    · simpa only [Subtype.ext_iff] using hc
  | isSuccLimit j hj hj' =>
    rw [transfiniteIterate_limit _ _ _ hj, Set.iSup_eq_iUnion]
    refine hasCardinalLT_iUnion _
      (HasCardinalLT.of_injective ?_ _ Subtype.val_injective) (fun ⟨k, hk⟩ ↦ hj' _ hk)
    simpa [hasCardinalLT_iff_cardinal_mk_lt]

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 : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
⊢ ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
have := Preregular.exists_fac 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 : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
this : ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ π = h ≫ 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.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π) ∈ (regularTopology C) X

Tactic:
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y)
      (fun () ↦ π)))

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ (regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π))

case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π)).arrows f →
      (regularCoverage C).Saturate Y_1
        (Sieve.pullback f (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))
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

pp: case refine_2
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
⊢ ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a

Tactic:
· ext
    simpa [mapToEqualizer] using! ha₁

Goal state after:
case refine_2
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
⊢ ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (op 0))

Tactic:
simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢
  exact isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h

Goal state after: