awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsIso.{v, u} (C := C) (X := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (Y :=
    pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    (Sigma.desc fun (p : ι × ι') ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯)
have apply : Nonempty (IsColimit c)
Tactic: apply c.nonempty_isColimit_iff_isIso_sigmaDesc.mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ Nonempty (IsColimit c)
have refine_1 : IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
  (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
Tactic: refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
refine_1 :
  IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
⊢ Nonempty (IsColimit c)
have refine_2 : IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
  (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
Tactic: refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
refine_1 :
  IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
refine_2 :
  IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
⊢ Nonempty (IsColimit c)
have refine_3 : IsLimit (F :=
  cospan (X :=
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
      (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i))
    (Y :=
    Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
      (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i))
    (Sigma.desc f) (Sigma.desc g))
  (pullback.cone (Sigma.desc f) (Sigma.desc g))
Tactic: refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsPullback (P := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (X :=
    sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y)
    (Sigma.desc fun (p : ι × ι') ↦ pullback.fst (f p.1) (g p.2) ≫ Sigma.ι X p.1)
    (Sigma.desc fun (p : ι × ι') ↦ pullback.snd (f p.1) (g p.2) ≫ Sigma.ι Y p.2) (Sigma.desc f) (Sigma.desc g)
have h : Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))) →
  sigmaObj.{u_1, v, u} X =
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
        (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i) →
    Eq (α :=
      {P : C} →
        (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
          (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
      (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) sorry)
      (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
        (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
        (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))
Tactic: convert!
    IsUniversalColimit.isPullback_prod_of_isColimit (d :=
      Cofan.mk _ (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (hd :=
      coproductIsCoproduct (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (a :=
      Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) ?_ ?_ f g
      (Sigma.desc f) (Sigma.desc g) (fun i j ↦ IsPullback.of_hasPullback (f i) (g j))
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_4 :
  sigmaObj.{u_1, v, u} X =
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
      (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
⊢ Eq (α :=
    {P : C} →
      (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
        (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
    (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) ⋯)
    (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))
have h : ∀ (x : C) (x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x) (b : ι × ι'),
  CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
      (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_5 :
  sigmaObj.{u_2, v, u} Y =
    Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor Y)
      (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
⊢ Eq (α :=
    {P : C} →
      (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
        (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
    (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) ⋯)
    (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))
have h : ∀ (x : C) (x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x) (b : ι × ι'),
  CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
      (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : ExtremalEpi f
A : Subobject.{v, u} Y
hA : A.Factors f
⊢ A = ⊤
have rw : IsIso A.arrow
Tactic: rw [← Subobject.isIso_arrow_iff_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
⊢ p = q
have this : IsIso (X := equalizer p q) (equalizer.ι p q)
Tactic: have := hf (equalizer.lift f h) (equalizer.ι p q) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
this : IsIso (X := equalizer p q) (equalizer.ι p q)
⊢ p = q
have rw : Eq (α := equalizer p q ⟶ Z) (equalizer.ι p q ≫ p) (equalizer.ι p q ≫ q)
Tactic: rw [← cancel_epi (equalizer.ι p q), equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
this : IsIso (X := equalizer p q) (equalizer.ι p q)
rw : Eq (α := equalizer p q ⟶ Z) (equalizer.ι p q ≫ p) (equalizer.ι p q ≫ q)
⊢ p = q
have rw₁ : Eq (α := equalizer p q ⟶ Z) (equalizer.ι p q ≫ q) (equalizer.ι p q ≫ q)
Tactic: rw [← cancel_epi (equalizer.ι p q), equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
h : Mono i
⊢ IsIso i
have sq : CommSq p f i (𝟙 Y)
Tactic: have sq : CommSq p f i (𝟙 Y) := { }
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
⊢ ExtremalEpi f ↔ StrongEpi f
have refine : ExtremalEpi f → (A B : C) → (i : A ⟶ B) → Mono i → {t : X ⟶ A} → {b : Y ⟶ B} → (sq : CommSq t f i b) → sq.LiftStruct
Tactic: refine ⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩,
    fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
⊢ sq.LiftStruct
have this : IsIso (X := pullback i b) (pullback.snd i b)
Tactic: have := ExtremalEpi.isIso f (pullback.lift _ _ sq.w)
    (pullback.snd _ _) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
⊢ f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b) = t
have rw : f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = f ≫ b
Tactic: rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
⊢ f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = f ≫ b
have e_a : CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
⊢ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b
have e_a : Eq (α := pullback i b ⟶ B)
  (pullback.snd i b ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i))
  (pullback.snd i b ≫ b)
Tactic: rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
e_a :
  Eq (α := pullback i b ⟶ B)
    (pullback.snd i b ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i))
    (pullback.snd i b ≫ b)
⊢ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b
have e_a₁ : Eq (α := pullback i b ⟶ B) (pullback.fst i b ≫ i) (pullback.snd i b ≫ b)
Tactic: rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.ExtremalEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
e_a :
  Eq (α := pullback i b ⟶ B)
    (pullback.snd i b ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i))
    (pullback.snd i b ≫ b)
e_a₁ : Eq (α := pullback i b ⟶ B) (pullback.fst i b ≫ i) (pullback.snd i b ≫ b)
⊢ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b
have e_a₂ : Eq (α := pullback i b ⟶ B) (pullback.snd i b ≫ b) (pullback.snd i b ≫ b)
Tactic: rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
𝒵 : BasedCategory.{v₄, u₄, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ (F.toFunctor ⋙ G.toFunctor) ⋙ 𝒵.p = 𝒳.p
have rw : F.toFunctor ⋙ G.toFunctor ⋙ 𝒵.p = 𝒳.p
Tactic: rw [Functor.assoc, G.w, F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
𝒵 : BasedCategory.{v₄, u₄, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
rw : F.toFunctor ⋙ G.toFunctor ⋙ 𝒵.p = 𝒳.p
⊢ (F.toFunctor ⋙ G.toFunctor) ⋙ 𝒵.p = 𝒳.p
have rw₁ : F.toFunctor ⋙ 𝒴.p = 𝒳.p
Tactic: rw [Functor.assoc, G.w, F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
𝒵 : BasedCategory.{v₄, u₄, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
rw : F.toFunctor ⋙ G.toFunctor ⋙ 𝒵.p = 𝒳.p
rw₁ : F.toFunctor ⋙ 𝒴.p = 𝒳.p
⊢ (F.toFunctor ⋙ G.toFunctor) ⋙ 𝒵.p = 𝒳.p
have rw₂ : 𝒳.p = 𝒳.p
Tactic: rw [Functor.assoc, G.w, F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒴.p.obj (F.obj a) = 𝒳.p.obj a
have rw : (F.toFunctor ⋙ 𝒴.p).obj a = 𝒳.p.obj a
Tactic: rw [← Functor.comp_obj, F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
rw : (F.toFunctor ⋙ 𝒴.p).obj a = 𝒳.p.obj a
⊢ 𝒴.p.obj (F.obj a) = 𝒳.p.obj a
have rw₁ : 𝒳.p.obj a = 𝒳.p.obj a
Tactic: rw [← Functor.comp_obj, F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒳.p.IsHomLift f φ
⊢ 𝒴.p.IsHomLift f (F.map φ)
have apply : f = eqToHom sorry ≫ 𝒴.p.map (F.map φ) ≫ eqToHom sorry
Tactic: apply of_fac 𝒴.p f (F.map φ) (Eq.trans (F.w_obj a) (domain_eq 𝒳.p f φ))
    (Eq.trans (F.w_obj b) (codomain_eq 𝒳.p f φ))
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ 𝒴.p.map (F.map φ) ≫ eqToHom ⋯
have rw : f = eqToHom sorry ≫ (eqToHom sorry ≫ 𝒳.p.map φ ≫ eqToHom sorry) ≫ eqToHom sorry
Tactic: rw [← Functor.comp_map, congr_hom F.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒴.p.IsHomLift f (F.map φ)
⊢ 𝒳.p.IsHomLift f φ
have apply : f = eqToHom sorry ≫ 𝒳.p.map φ ≫ eqToHom sorry
Tactic: apply of_fac 𝒳.p f φ (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ))
    (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α β : BasedNatTrans F G
h : α.toNatTrans = β.toNatTrans
⊢ α = β
have mk : ∀ (toNatTrans : NatTrans F.toFunctor G.toFunctor)
  (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans.app a))
  (h : { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G }.toNatTrans = β.toNatTrans),
  { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β
Tactic: cases α
Cleared hypotheses: α, h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
toNatTrans : NatTrans F.toFunctor G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans.app a)
h : { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G }.toNatTrans = β.toNatTrans
⊢ { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β
have mk : ∀ (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)),
  { toNatTrans := β.toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β
Tactic: subst h
Cleared hypotheses: toNatTrans, isHomLift', h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)
have subst : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)
Tactic: subst ha
Cleared hypotheses: S, ha
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G H : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
β : BasedNatTrans G H
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((α.vcomp β.toNatTrans).app a)
have rw : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a ≫ β.app a)
Tactic: rw [CategoryTheory.NatTrans.vcomp_app]