awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Elements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
i : I
⊢ (hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → A.obj (F.obj i).fst)
      (liftedConeElement F : A.obj (limit (F ⋙ π A))) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)
have this : Eq (α := A.obj ((F ⋙ π A).obj i))
  (((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := A.obj (limit (F ⋙ π A))) (Iso.inv (preservesLimitIso A (F ⋙ π A)))
              (A.map (limit.π (F ⋙ π A) i))) :
          TypeCat.Fun (limit ((F ⋙ π A) ⋙ A)) (A.obj ((F ⋙ π A).obj i))) :
        (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
      (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
    A.obj ((F ⋙ π A).obj i))
  ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) : (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
      (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
    A.obj ((F ⋙ π A).obj i))
Tactic: have := congr_hom
    (preservesLimitIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f ↔ c.fst = c.snd
have mp : Mono f → c.fst = c.snd
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
mp : Mono f → c.fst = c.snd
⊢ Mono f ↔ c.fst = c.snd
have mpr : c.fst = c.snd → Mono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ Mono f
have mpr : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'
have mpr : ∀ (φ : Z ⟶ c.pt) (h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f), φ ≫ c.fst = φ ≫ c.snd
Tactic: obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h
Cleared hypotheses: g, g', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
φ : Z ⟶ c.pt
h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f
⊢ φ ≫ c.fst = φ ≫ c.snd
have mpr : φ ≫ c.snd = φ ≫ c.snd
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f ↔ IsIso c.fst
have rw : c.fst = c.snd ↔ IsIso c.fst
Tactic: rw [mono_iff_fst_eq_snd hc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd ↔ IsIso c.fst
have mp : c.fst = c.snd → IsIso c.fst
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
mp : c.fst = c.snd → IsIso c.fst
⊢ c.fst = c.snd ↔ IsIso c.fst
have mpr : IsIso c.fst → c.fst = c.snd
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
⊢ IsIso c.fst
have mp : ∀ (φ : X ⟶ c.pt) (hφ₁ : φ ≫ c.fst = 𝟙 X) (hφ₂ : φ ≫ c.snd = 𝟙 X), IsIso c.fst
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ IsIso c.fst
have mp : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
Tactic: refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
mp : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
⊢ IsIso c.fst
have mp₁ : (c.fst ≫ φ) ≫ c.snd = 𝟙 c.pt ≫ c.snd
Tactic: refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
⊢ c.fst = c.snd
have mpr : ∀ (φ : X ⟶ c.pt) (hφ₁ : φ ≫ c.fst = 𝟙 X) (hφ₂ : φ ≫ c.snd = 𝟙 X), c.fst = c.snd
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ = 𝟙 c.pt
have rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
Tactic: rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
⊢ c.fst ≫ φ = 𝟙 c.pt
have rw₁ : c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
Tactic: rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₁ : c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
⊢ c.fst ≫ φ = 𝟙 c.pt
have rw₂ : c.fst ≫ φ ≫ c.fst = c.fst
Tactic: rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₁ : c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₂ : c.fst ≫ φ ≫ c.fst = c.fst
⊢ c.fst ≫ φ = 𝟙 c.pt
have rw₃ : c.fst ≫ 𝟙 X = c.fst
Tactic: rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₁ : c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₂ : c.fst ≫ φ ≫ c.fst = c.fst
rw₃ : c.fst ≫ 𝟙 X = c.fst
⊢ c.fst ≫ φ = 𝟙 c.pt
have rw₄ : c.fst = c.fst
Tactic: rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst = c.snd
have this : IsSplitEpi φ
Tactic: have : IsSplitEpi φ := IsSplitEpi.mk ⟨SplitEpi.mk c.fst (by
      rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id])⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
⊢ c.fst = c.snd
have mpr : φ ≫ c.fst = φ ≫ c.snd
Tactic: rw [← cancel_epi φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
mpr : φ ≫ c.fst = φ ≫ c.snd
⊢ c.fst = c.snd
have mpr₁ : 𝟙 X = φ ≫ c.snd
Tactic: rw [← cancel_epi φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
mpr : φ ≫ c.fst = φ ≫ c.snd
mpr₁ : 𝟙 X = φ ≫ c.snd
⊢ c.fst = c.snd
have mpr₂ : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
Tactic: rw [← cancel_epi φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f
have mp : Mono f → IsPullback (𝟙 X) (𝟙 X) f f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Mono f → IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f
have mpr : IsPullback (𝟙 X) (𝟙 X) f f → Mono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ c.inl = c.inr
have mp : Epi f → c.inl = c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
mp : Epi f → c.inl = c.inr
⊢ Epi f ↔ c.inl = c.inr
have mpr : c.inl = c.inr → Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ Epi f
have mpr : ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'
have mpr : ∀ (φ : c.pt ⟶ Z) (h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ), c.inl ≫ φ = c.inr ≫ φ
Tactic: obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
Cleared hypotheses: g, g', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
φ : c.pt ⟶ Z
h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ
⊢ c.inl ≫ φ = c.inr ≫ φ
have mpr : c.inr ≫ φ = c.inr ≫ φ
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ IsIso c.inl
have rw : c.inl = c.inr ↔ IsIso c.inl
Tactic: rw [epi_iff_inl_eq_inr hc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr ↔ IsIso c.inl
have mp : c.inl = c.inr → IsIso c.inl
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
mp : c.inl = c.inr → IsIso c.inl
⊢ c.inl = c.inr ↔ IsIso c.inl
have mpr : IsIso c.inl → c.inl = c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
⊢ IsIso c.inl
have mp : ∀ (φ : c.pt ⟶ Y) (hφ₁ : c.inl ≫ φ = 𝟙 Y) (hφ₂ : c.inr ≫ φ = 𝟙 Y), IsIso c.inl
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ IsIso c.inl
have mp : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
Tactic: refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
mp : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
⊢ IsIso c.inl
have mp₁ : c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt
Tactic: refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
⊢ c.inl = c.inr
have mpr : ∀ (φ : c.pt ⟶ Y) (hφ₁ : c.inl ≫ φ = 𝟙 Y) (hφ₂ : c.inr ≫ φ = 𝟙 Y), c.inl = c.inr
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ φ ≫ c.inl = 𝟙 c.pt
have rw : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
Tactic: rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
rw : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
⊢ φ ≫ c.inl = 𝟙 c.pt
have rw₁ : c.inl = c.inl ≫ 𝟙 c.pt
Tactic: rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
rw : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
rw₁ : c.inl = c.inl ≫ 𝟙 c.pt
⊢ φ ≫ c.inl = 𝟙 c.pt
have rw₂ : c.inl = c.inl
Tactic: rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl = c.inr
have this : IsSplitMono φ
Tactic: have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by
      rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
⊢ c.inl = c.inr
have mpr : c.inl ≫ φ = c.inr ≫ φ
Tactic: rw [← cancel_mono φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
mpr : c.inl ≫ φ = c.inr ≫ φ
⊢ c.inl = c.inr
have mpr₁ : 𝟙 Y = c.inr ≫ φ
Tactic: rw [← cancel_mono φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
mpr : c.inl ≫ φ = c.inr ≫ φ
mpr₁ : 𝟙 Y = c.inr ≫ φ
⊢ c.inl = c.inr
have mpr₂ : Eq.{v_1 + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
Tactic: rw [← cancel_mono φ, hφ₁, hφ₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ IsPushout f f (𝟙 Y) (𝟙 Y)
have mp : Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.EpiMono (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f ↔ IsPushout f f (𝟙 Y) (𝟙 Y)
have mpr : IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : leftExactFunctor C D X
⊢ leftExactFunctor C D Y
have h₁ : PreservesFiniteLimits X
Tactic: simp only [leftExactFunctor_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : rightExactFunctor C D X
⊢ rightExactFunctor C D Y
have h₁ : PreservesFiniteColimits X
Tactic: simp only [rightExactFunctor_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
G : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := leftExactFunctor C D))) G)
have dsimp : leftExactFunctor C E (F.obj (P := leftExactFunctor C D) ⋙ G.obj (P := leftExactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := leftExactFunctor D E))) G)
have dsimp : leftExactFunctor C E (G.obj (P := leftExactFunctor C D) ⋙ F.obj (P := leftExactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
G : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := rightExactFunctor C D))) G)
have dsimp : rightExactFunctor C E (F.obj (P := rightExactFunctor C D) ⋙ G.obj (P := rightExactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := rightExactFunctor D E))) G)
have dsimp : rightExactFunctor C E (G.obj (P := rightExactFunctor C D) ⋙ F.obj (P := rightExactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := exactFunctor C D))) G)
have dsimp : leftExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := exactFunctor C D))) G)
have dsimp : rightExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := exactFunctor D E))) G)
have dsimp : leftExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ExactFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := exactFunctor D E))) G)
have dsimp : rightExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsFiltered.{v, u} C ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have rw : (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
Tactic: rw [IsFiltered.iff_cocone_nonempty.{v}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have refine_1 : ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) (J : Type v)
  (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
  ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
Tactic: refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) (J : Type v)
    (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have refine_2 : ∀
  (h :
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X)))
  (J : Type v) (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C), Nonempty (Cocone F)
Tactic: refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩