awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst_1 : Mono f
s : PullbackCone f f
⊢ (fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X = s.snd
have rw : ((fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X) ≫ f = s.snd ≫ f
Tactic: rw [← cancel_mono f, Category.comp_id, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst_1 : Mono f
s : PullbackCone f f
rw : ((fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X) ≫ f = s.snd ≫ f
⊢ (fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X = s.snd
have rw₁ : (fun (s : PullbackCone f f) ↦ s.fst) s ≫ f = s.snd ≫ f
Tactic: rw [← cancel_mono f, Category.comp_id, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst_1 : Mono f
s : PullbackCone f f
rw : ((fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X) ≫ f = s.snd ≫ f
rw₁ : (fun (s : PullbackCone f f) ↦ s.fst) s ≫ f = s.snd ≫ f
⊢ (fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X = s.snd
have rw₂ : s.snd ≫ f = s.snd ≫ f
Tactic: rw [← cancel_mono f, Category.comp_id, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h
have rcases : ∀ (val : Z ⟶ Cone.pt.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) sorry))
  (eq : (val ≫ fst (mk (𝟙 X) (𝟙 X) sorry)) ≫ f = (val ≫ snd (mk (𝟙 X) (𝟙 X) sorry)) ≫ f),
  val ≫ fst (mk (𝟙 X) (𝟙 X) sorry) = val ≫ snd (mk (𝟙 X) (𝟙 X) sorry)
Tactic: rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
Cleared hypotheses: g, h, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
⊢ t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
have rw : (t.fst ≫ x) ≫ h = (t.snd ≫ y) ≫ h
Tactic: rw [← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ f = t.snd ≫ g
have rw : t.fst ≫ x ≫ h = t.snd ≫ g
Tactic: rw [← hxh, ← hyh, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
rw : t.fst ≫ x ≫ h = t.snd ≫ g
rw₁ : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ f = t.snd ≫ g
have rw₂ : t.snd ≫ y ≫ h = t.snd ≫ y ≫ h
Tactic: rw [← hxh, ← hyh, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ fst (mk s.fst s.snd ⋯) = t.fst
hr' : m ≫ snd (mk s.fst s.snd ⋯) = t.snd
⊢ m = hs.lift (mk t.fst t.snd ⋯)
have h₀ : m ≫ s.fst = hs.lift (mk t.fst t.snd sorry) ≫ s.fst
Tactic: apply PullbackCone.IsLimit.hom_ext hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ fst (mk s.fst s.snd ⋯) = t.fst
hr' : m ≫ snd (mk s.fst s.snd ⋯) = t.snd
h₀ : m ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
⊢ m = hs.lift (mk t.fst t.snd ⋯)
have h₁ : m ≫ s.snd = hs.lift (mk t.fst t.snd sorry) ≫ s.snd
Tactic: apply PullbackCone.IsLimit.hom_ext hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ m ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
have h₀ : t.fst = hs.lift (mk t.fst t.snd sorry) ≫ s.fst
Tactic: simp only [hr, hr']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ m ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
have h₁ : t.snd = hs.lift (mk t.fst t.snd sorry) ≫ s.snd
Tactic: simp only [hr, hr']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ t.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
have h₀ : hs.lift (mk t.fst t.snd sorry) ≫ s.fst = t.fst
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ t.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
have h₁ : hs.lift (mk t.fst t.snd sorry) ≫ s.snd = t.snd
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
⊢ s.fst ≫ f ≫ i = s.snd ≫ g ≫ i
have rw : (s.fst ≫ f) ≫ i = s.snd ≫ g ≫ i
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
rw : (s.fst ≫ f) ≫ i = s.snd ≫ g ≫ i
⊢ s.fst ≫ f ≫ i = s.snd ≫ g ≫ i
have rw₁ : (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
rw : (s.fst ≫ f) ≫ i = s.snd ≫ g ≫ i
rw₁ : (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i
⊢ s.fst ≫ f ≫ i = s.snd ≫ g ≫ i
have rw₂ : (s.snd ≫ g) ≫ i = (s.snd ≫ g) ≫ i
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
⊢ IsLimit (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd ⋯)
have create : (s_1 : PullbackCone (f ≫ i) (g ≫ i)) →
  { l : s_1.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd sorry) //
    l ≫ fst (mk s.fst s.snd sorry) = s_1.fst ∧
      l ≫ snd (mk s.fst s.snd sorry) = s_1.snd ∧
        ∀ {m : s_1.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd sorry)},
          m ≫ fst (mk s.fst s.snd sorry) = s_1.fst → m ≫ snd (mk s.fst s.snd sorry) = s_1.snd → m = l }
Tactic: apply PullbackCone.isLimitAux'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯) //
    l ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst ∧
      l ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
          m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → m = l }
have create : (l : s.pt ⟶ s_1.pt) →
  (h₁ : l ≫ s_1.fst = s.fst) →
    (h₂ : l ≫ s_1.snd = s.snd) →
      { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd sorry) //
        l ≫ fst (mk s_1.fst s_1.snd sorry) = s.fst ∧
          l ≫ snd (mk s_1.fst s_1.snd sorry) = s.snd ∧
            ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd sorry)},
              m ≫ fst (mk s_1.fst s_1.snd sorry) = s.fst → m ≫ snd (mk s_1.fst s_1.snd sorry) = s.snd → m = l }
Tactic: rcases PullbackCone.IsLimit.lift' H s.fst s.snd
      ((cancel_mono i).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s_1.pt
h₁ : l ≫ s_1.fst = s.fst
h₂ : l ≫ s_1.snd = s.snd
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯) //
    l ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst ∧
      l ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
          m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → m = l }
have create : ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd sorry)},
  m ≫ fst (mk s_1.fst s_1.snd sorry) = s.fst → m ≫ snd (mk s_1.fst s_1.snd sorry) = s.snd → m = l
Tactic: refine ⟨l, h₁, h₂, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
W_1 X_1 Y_1 Z_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h :
  Eq (α := W ⟶ prod.{v_1, u_1} X Y) (i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
    (i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
⊢ i₁ = i₂
have h₀ : i₁ ≫ pullback.fst f g = i₂ ≫ pullback.fst f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
W_1 X_1 Y_1 Z_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h :
  Eq (α := W ⟶ prod.{v_1, u_1} X Y) (i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
    (i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
h₀ : i₁ ≫ pullback.fst f g = i₂ ≫ pullback.fst f g
⊢ i₁ = i₂
have h₁ : i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f ≫ i) (pullback.snd f g ≫ g ≫ i)
have simp : Eq (α := pullback f g ⟶ Z) ((pullback.fst f g ≫ f) ≫ i) ((pullback.snd f g ≫ g) ≫ i)
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
inst_2 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ Z) ((pullback.fst f g ≫ f) ≫ i) ((pullback.snd f g ≫ g) ≫ i)
have rw : Eq (α := pullback f g ⟶ W) (pullback.fst f g ≫ f) (pullback.snd f g ≫ g)
Tactic: rw [cancel_mono]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ IsIso (X := pullback i (f ≫ i)) (pullback.snd i (f ≫ i))
have this : Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
  (CategoryStruct.comp (Y :=
    Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
      (LimitCone.cone
        { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry,
          isLimit :=
            (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
              IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry)) }))
    (Iso.hom
      (limit.isoLimitCone
        { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry,
          isLimit :=
            (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
              IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry)) }))
    (NatTrans.app
      (Cone.π
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) sorry)) }))
      WalkingCospan.right))
  (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
Tactic: have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono (𝟙 _) f i⟩ WalkingCospan.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
⊢ IsIso (X := pullback i (f ≫ i)) (pullback.snd i (f ≫ i))
have h : i = 𝟙 Z ≫ i
Tactic: convert! (congrArg IsIso (show _ ≫ pullback.snd (𝟙 Z) f = _ from this)).mp inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (𝟙 Z ≫ i) (f ≫ i)) ⟶ (cospan (𝟙 Z ≫ i) (f ≫ i)).obj WalkingCospan.right)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (𝟙 Z ≫ i) (f ≫ i))
        (LimitCone.cone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                  (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
      (NatTrans.app
        (Cone.π
          (LimitCone.cone
            { cone := mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
              isLimit :=
                (pullbackIsPullbackOfCompMono (𝟙 Z) f i :
                  IsLimit (F := cospan (𝟙 Z ≫ i) (f ≫ i))
                    (mk (W := pullback (𝟙 Z) f) (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯)) }))
        WalkingCospan.right))
    (limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right)
h : i = 𝟙 Z ≫ i
⊢ IsIso (X := pullback i (f ≫ i)) (pullback.snd i (f ≫ i))
have h₁ : pullback i (f ≫ i) = limit (cospan (𝟙 Z ≫ i) (f ≫ i)) → i = 𝟙 Z ≫ i
Tactic: convert! (congrArg IsIso (show _ ≫ pullback.snd (𝟙 Z) f = _ from this)).mp inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
⊢ IsIso (X := pullback (f ≫ i) i) (pullback.fst (f ≫ i) i)
have this : Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
  (Iso.hom
      (limit.isoLimitCone
        { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) sorry,
          isLimit :=
            (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
              IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) sorry)) }) ≫
    { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) sorry,
              isLimit :=
                (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                  IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                    (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) sorry)) :
              LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
      WalkingCospan.left)
  (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
Tactic: have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono f (𝟙 _) i⟩ WalkingCospan.left
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
⊢ IsIso (X := pullback (f ≫ i) i) (pullback.fst (f ≫ i) i)
have h : i = 𝟙 Z ≫ i
Tactic: convert! (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst_1 : Mono i
this :
  Eq (α := limit (cospan (f ≫ i) (𝟙 Z ≫ i)) ⟶ (cospan (f ≫ i) (𝟙 Z ≫ i)).obj WalkingCospan.left)
    (Iso.hom
        (limit.isoLimitCone
          { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit :=
              (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                  (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) }) ≫
      { cone := mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit :=
                  (pullbackIsPullbackOfCompMono f (𝟙 Z) i :
                    IsLimit (F := cospan (f ≫ i) (𝟙 Z ≫ i))
                      (mk (W := pullback f (𝟙 Z)) (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯)) :
                LimitCone (cospan (f ≫ i) (𝟙 Z ≫ i)) }.cone.π.app
        WalkingCospan.left)
    (limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left)
h : i = 𝟙 Z ≫ i
⊢ IsIso (X := pullback (f ≫ i) i) (pullback.fst (f ≫ i) i)
have h₁ : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i)) → i = 𝟙 Z ≫ i
Tactic: convert! (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Iso.hom (pullbackSymmetry f f) = 𝟙 (pullback f f)
have h₀ : Iso.hom (pullbackSymmetry f f) ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h₀ : Iso.hom (pullbackSymmetry f f) ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f
⊢ Iso.hom (pullbackSymmetry f f) = 𝟙 (pullback f f)
have h₁ : Iso.hom (pullbackSymmetry f f) ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst
have refine : t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) sorry = 𝟙 t.pt
Tactic: refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt
have h₀ : (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) sorry) ≫ t.fst = 𝟙 t.pt ≫ t.fst
Tactic: apply PullbackCone.IsLimit.hom_ext ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
h₀ : (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt
have h₁ : (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) sorry) ≫ t.snd = 𝟙 t.pt ≫ t.snd
Tactic: apply PullbackCone.IsLimit.hom_ext ht