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 ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst_1 : Epi f
s : PushoutCocone f f
⊢ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = s.inr
have rw : f ≫ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
Tactic: rw [← cancel_epi f, Category.id_comp, 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 ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst_1 : Epi f
s : PushoutCocone f f
rw : f ≫ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
⊢ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = s.inr
have rw₁ : f ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
Tactic: rw [← cancel_epi f, Category.id_comp, 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 ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst_1 : Epi f
s : PushoutCocone f f
rw : f ≫ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
rw₁ : f ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
⊢ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = s.inr
have rw₂ : f ≫ s.inr = f ≫ s.inr
Tactic: rw [← cancel_epi f, Category.id_comp, 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 : IsColimit.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h
have rcases : ∀ (val : Cocone.pt.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) sorry) ⟶ Z)
  (eq : f ≫ inl (mk (𝟙 Y) (𝟙 Y) sorry) ≫ val = f ≫ inr (mk (𝟙 Y) (𝟙 Y) sorry) ≫ val),
  inl (mk (𝟙 Y) (𝟙 Y) sorry) ≫ val = inr (mk (𝟙 Y) (𝟙 Y) sorry) ≫ val
Tactic: rcases PushoutCocone.IsColimit.desc' 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ h ≫ x ≫ s.inl = f ≫ s.inl
have rw : (h ≫ x) ≫ s.inl = f ≫ s.inl
Tactic: rw [← 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ h ≫ y ≫ s.inr = g ≫ s.inr
have rw : (h ≫ y) ≫ s.inr = g ≫ s.inr
Tactic: rw [← 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr
have rw : f ≫ s.inl = h ≫ y ≫ s.inr
Tactic: rw [reassoc₁, reassoc₂, 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
rw : f ≫ s.inl = h ≫ y ≫ s.inr
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr
have rw₁ : f ≫ s.inl = g ≫ s.inr
Tactic: rw [reassoc₁, reassoc₂, 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
rw : f ≫ s.inl = h ≫ y ≫ s.inr
rw₁ : f ≫ s.inl = g ≫ s.inr
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr
have rw₂ : g ≫ s.inr = g ≫ s.inr
Tactic: rw [reassoc₁, reassoc₂, 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
⊢ f ≫ t.inl = g ≫ t.inr
have rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
Tactic: rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
⊢ f ≫ t.inl = g ≫ t.inr
have rw₁ : (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
Tactic: rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
rw₁ : (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
⊢ f ≫ t.inl = g ≫ t.inr
have rw₂ : h ≫ x ≫ t.inl = (h ≫ y) ≫ t.inr
Tactic: rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
rw₁ : (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
rw₂ : h ≫ x ≫ t.inl = (h ≫ y) ≫ t.inr
⊢ f ≫ t.inl = g ≫ t.inr
have rw₃ : h ≫ x ≫ t.inl = h ≫ y ≫ t.inr
Tactic: rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
rw₁ : (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
rw₂ : h ≫ x ≫ t.inl = (h ≫ y) ≫ t.inr
rw₃ : h ≫ x ≫ t.inl = h ≫ y ≫ t.inr
⊢ f ≫ t.inl = g ≫ t.inr
have rw₄ : h ≫ y ≫ t.inr = h ≫ y ≫ t.inr
Tactic: rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : inl (mk s.inl s.inr ⋯) ≫ m = t.inl
hr' : inr (mk s.inl s.inr ⋯) ≫ m = t.inr
⊢ m = hs.desc (mk t.inl t.inr ⋯)
have h₀ : s.inl ≫ m = s.inl ≫ hs.desc (mk t.inl t.inr sorry)
Tactic: apply PushoutCocone.IsColimit.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : inl (mk s.inl s.inr ⋯) ≫ m = t.inl
hr' : inr (mk s.inl s.inr ⋯) ≫ m = t.inr
h₀ : s.inl ≫ m = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
⊢ m = hs.desc (mk t.inl t.inr ⋯)
have h₁ : s.inr ≫ m = s.inr ≫ hs.desc (mk t.inl t.inr sorry)
Tactic: apply PushoutCocone.IsColimit.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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inl ≫ m = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
have h₀ : t.inl = s.inl ≫ hs.desc (mk t.inl t.inr sorry)
Tactic: simp only [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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ t.inl = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
have h₀ : s.inl ≫ hs.desc (mk t.inl t.inr sorry) = t.inl
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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inr ≫ m = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
have h₁ : t.inr = s.inr ≫ hs.desc (mk t.inl t.inr sorry)
Tactic: simp only [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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ t.inr = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
have h₁ : s.inr ≫ hs.desc (mk t.inl t.inr sorry) = t.inr
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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ (h ≫ f) ≫ s.inl = (h ≫ g) ≫ s.inr
have rw : h ≫ f ≫ s.inl = (h ≫ g) ≫ s.inr
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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
rw : h ≫ f ≫ s.inl = (h ≫ g) ≫ s.inr
⊢ (h ≫ f) ≫ s.inl = (h ≫ g) ≫ s.inr
have rw₁ : h ≫ f ≫ s.inl = h ≫ g ≫ s.inr
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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
rw : h ≫ f ≫ s.inl = (h ≫ g) ≫ s.inr
rw₁ : h ≫ f ≫ s.inl = h ≫ g ≫ s.inr
⊢ (h ≫ f) ≫ s.inl = (h ≫ g) ≫ s.inr
have rw₂ : h ≫ g ≫ s.inr = h ≫ g ≫ s.inr
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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ IsColimit (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr ⋯)
have create : (s_1 : PushoutCocone (h ≫ f) (h ≫ g)) →
  { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr sorry) ⟶ s_1.pt //
    inl (mk s.inl s.inr sorry) ≫ l = s_1.inl ∧
      inr (mk s.inl s.inr sorry) ≫ l = s_1.inr ∧
        ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr sorry) ⟶ s_1.pt},
          inl (mk s.inl s.inr sorry) ≫ m = s_1.inl → inr (mk s.inl s.inr sorry) ≫ m = s_1.inr → m = l }
Tactic: apply PushoutCocone.isColimitAux'
-- 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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
⊢ { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt //
    inl (mk s_1.inl s_1.inr ⋯) ≫ l = s.inl ∧
      inr (mk s_1.inl s_1.inr ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
          inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l }
have create : (l : s_1.pt ⟶ s.pt) →
  (h₁ : s_1.inl ≫ l = s.inl) →
    (h₂ : s_1.inr ≫ l = s.inr) →
      { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr sorry) ⟶ s.pt //
        inl (mk s_1.inl s_1.inr sorry) ≫ l = s.inl ∧
          inr (mk s_1.inl s_1.inr sorry) ≫ l = s.inr ∧
            ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr sorry) ⟶ s.pt},
              inl (mk s_1.inl s_1.inr sorry) ≫ m = s.inl → inr (mk s_1.inl s_1.inr sorry) ≫ m = s.inr → m = l }
Tactic: rcases PushoutCocone.IsColimit.desc' H s.inl s.inr
      ((cancel_epi h).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 ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s_1.pt ⟶ s.pt
h₁ : s_1.inl ≫ l = s.inl
h₂ : s_1.inr ≫ l = s.inr
⊢ { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt //
    inl (mk s_1.inl s_1.inr ⋯) ≫ l = s.inl ∧
      inr (mk s_1.inl s_1.inr ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
          inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l }
have create : ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr sorry) ⟶ s.pt},
  inl (mk s_1.inl s_1.inr sorry) ≫ m = s.inl → inr (mk s_1.inl s_1.inr sorry) ≫ m = s.inr → 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 ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasBinaryCoproduct.{v_1, u_1} Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h :
  Eq (α := coprod.{v_1, u_1} Y Z ⟶ W) (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁)
    (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂)
⊢ i₁ = i₂
have h₀ : pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂
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 ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasBinaryCoproduct.{v_1, u_1} Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h :
  Eq (α := coprod.{v_1, u_1} Y Z ⟶ W) (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁)
    (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂)
h₀ : pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂
⊢ i₁ = i₂
have h₁ : pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂
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 ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
⊢ Eq (α := W ⟶ pushout f g) ((h ≫ f) ≫ pushout.inl f g) ((h ≫ g) ≫ pushout.inr f g)
have simp : Eq (α := W ⟶ pushout f g) (h ≫ f ≫ pushout.inl f g) (h ≫ g ≫ pushout.inr f g)
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 ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
⊢ Eq (α := W ⟶ pushout f g) (h ≫ f ≫ pushout.inl f g) (h ≫ g ≫ pushout.inr f g)
have rw : Eq (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (g ≫ pushout.inr f g)
Tactic: rw [cancel_epi]
-- 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
h : W ⟶ X
inst_1 : Epi h
⊢ IsIso (Y := pushout h (h ≫ f)) (pushout.inr h (h ≫ f))
have h₁ : h = h ≫ 𝟙 X
Tactic: convert!
    (congrArg IsIso
          (show pushout.inr _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp (𝟙 _) f h⟩
              WalkingSpan.right)).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
h : W ⟶ X
inst_1 : Epi h
h₁ : h = h ≫ 𝟙 X
⊢ IsIso (Y := pushout h (h ≫ f)) (pushout.inr h (h ≫ f))
have h₂ : Z = (span (h ≫ 𝟙 X) (h ≫ f)).obj WalkingSpan.right → pushout h (h ≫ f) = colimit (span (h ≫ 𝟙 X) (h ≫ f)) → h = h ≫ 𝟙 X
Tactic: convert!
    (congrArg IsIso
          (show pushout.inr _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp (𝟙 _) f h⟩
              WalkingSpan.right)).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_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
⊢ IsIso (Y := pushout (h ≫ f) h) (pushout.inl (h ≫ f) h)
have h₁ : h = h ≫ 𝟙 X
Tactic: convert!
    (congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩
              WalkingSpan.left)).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_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
h₁ : h = h ≫ 𝟙 X
⊢ IsIso (Y := pushout (h ≫ f) h) (pushout.inl (h ≫ f) h)
have h₂ : Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left → pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X)) → h = h ≫ 𝟙 X
Tactic: convert!
    (congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩
              WalkingSpan.left)).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 : Epi f
⊢ Iso.hom (pushoutSymmetry f f) = 𝟙 (pushout f f)
have h₀ : CategoryStruct.comp (Y := pushout f f) (pushout.inl f f) (Iso.hom (pushoutSymmetry f f)) =
  pushout.inl f f ≫ 𝟙 (pushout 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 : Epi f
h₀ :
  CategoryStruct.comp (Y := pushout f f) (pushout.inl f f) (Iso.hom (pushoutSymmetry f f)) =
    pushout.inl f f ≫ 𝟙 (pushout f f)
⊢ Iso.hom (pushoutSymmetry f f) = 𝟙 (pushout f f)
have h₁ : CategoryStruct.comp (Y := pushout f f) (pushout.inr f f) (Iso.hom (pushoutSymmetry f f)) =
  pushout.inr f f ≫ 𝟙 (pushout 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 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsIso t.inl
have refine : IsColimit.desc ht (𝟙 Y) (𝟙 Y) sorry ≫ t.inl = 𝟙 t.pt
Tactic: refine ⟨⟨PushoutCocone.IsColimit.desc 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 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt
have h₀ : t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) sorry ≫ t.inl = t.inl ≫ 𝟙 t.pt
Tactic: apply PushoutCocone.IsColimit.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 : Epi f
t : PushoutCocone f f
ht : IsColimit t
h₀ : t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt
⊢ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt
have h₁ : t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) sorry ≫ t.inl = t.inr ≫ 𝟙 t.pt
Tactic: apply PushoutCocone.IsColimit.hom_ext ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
have rw : t₁.snd ≫ i₂ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
Tactic: rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
rw : t₁.snd ≫ i₂ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
have rw₁ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.snd ≫ i₃
Tactic: rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
rw : t₁.snd ≫ i₂ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
rw₁ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.snd ≫ i₃
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
have rw₂ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.fst ≫ g₂
Tactic: rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
rw : t₁.snd ≫ i₂ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
rw₁ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.snd ≫ i₃
rw₂ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.fst ≫ g₂
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
have rw₃ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ i₂ ≫ g₂
Tactic: rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
⊢ IsLimit (t₂.pasteHoriz t₁ hi₂)
have create : (s : PullbackCone (g₁ ≫ g₂) i₃) →
  { l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt //
    l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
      l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
          m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }
Tactic: apply PullbackCone.isLimitAux'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ (s.fst ≫ g₁) ≫ g₂ = s.snd ≫ i₃
have rw : (s.fst ≫ g₁) ≫ g₂ = s.fst ≫ g₁ ≫ g₂
Tactic: rw [← s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
rw : (s.fst ≫ g₁) ≫ g₂ = s.fst ≫ g₁ ≫ g₂
⊢ (s.fst ≫ g₁) ≫ g₂ = s.snd ≫ i₃
have rw₁ : s.fst ≫ g₁ ≫ g₂ = s.fst ≫ g₁ ≫ g₂
Tactic: rw [← s.condition, Category.assoc]