awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
⊢ { 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 }
have create : (l₂ : s.pt ⟶ t₂.pt) →
  (hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁) →
    (hl₂' : l₂ ≫ t₂.snd = s.snd) →
      { 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: obtain ⟨l₂, hl₂, hl₂'⟩ := PullbackCone.IsLimit.lift' H (s.fst ≫ g₁) s.snd
    (by 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
⊢ s.fst ≫ g₁ = l₂ ≫ i₂
have rw : l₂ ≫ t₂.fst = l₂ ≫ i₂
Tactic: rw [← hl₂, 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
rw : l₂ ≫ t₂.fst = l₂ ≫ i₂
⊢ s.fst ≫ g₁ = l₂ ≫ i₂
have rw₁ : l₂ ≫ t₂.fst = l₂ ≫ t₂.fst
Tactic: rw [← hl₂, 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
⊢ { 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 }
have create : (l₁ : s.pt ⟶ t₁.pt) →
  (hl₁ : l₁ ≫ t₁.fst = s.fst) →
    (hl₁' : l₁ ≫ t₁.snd = l₂) →
      { 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: obtain ⟨l₁, hl₁, hl₁'⟩ := PullbackCone.IsLimit.lift' H' s.fst l₂ (by rw [← hl₂, 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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ { 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 }
have create : ∀ {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: refine ⟨l₁, hl₁, by simp [reassoc_of% hl₁', hl₂'], ?_⟩
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m = l₁
have create : m ≫ t₁.snd = l₁ ≫ t₁.snd
Tactic: apply PullbackCone.IsLimit.hom_ext H' (by simpa [hl₁] using hm₁)
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.snd = l₁ ≫ t₁.snd
have create : (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
Tactic: apply PullbackCone.IsLimit.hom_ext H
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
⊢ m ≫ t₁.snd = l₁ ≫ t₁.snd
have create₁ : (m ≫ t₁.snd) ≫ t₂.snd = (l₁ ≫ t₁.snd) ≫ t₂.snd
Tactic: apply PullbackCone.IsLimit.hom_ext H
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₃ : s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₃ : s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₄ : s.fst ≫ g₁ = l₂ ≫ i₂
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₃ : s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₄ : s.fst ≫ g₁ = l₂ ≫ i₂
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₅ : s.fst ≫ g₁ = l₂ ≫ t₂.fst
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₃ : s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₄ : s.fst ≫ g₁ = l₂ ≫ i₂
create₅ : s.fst ≫ g₁ = l₂ ≫ t₂.fst
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
have create₆ : s.fst ≫ g₁ = s.fst ≫ g₁
Tactic: rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
-- 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₂.pasteHoriz t₁ hi₂)
⊢ IsLimit t₁
have create : (s : PullbackCone g₁ i₂) →
  { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
⊢ s.fst ≫ g₁ ≫ g₂ = (s.snd ≫ t₂.snd) ≫ i₃
have rw : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.snd ≫ i₃
Tactic: rw [Category.assoc, ← t₂.condition, reassoc_of% s.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
rw : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.snd ≫ i₃
⊢ s.fst ≫ g₁ ≫ g₂ = (s.snd ≫ t₂.snd) ≫ i₃
have rw₁ : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
Tactic: rw [Category.assoc, ← t₂.condition, reassoc_of% s.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
rw : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.snd ≫ i₃
rw₁ : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
⊢ s.fst ≫ g₁ ≫ g₂ = (s.snd ≫ t₂.snd) ≫ i₃
have rw₂ : s.snd ≫ i₂ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
Tactic: rw [Category.assoc, ← t₂.condition, reassoc_of% s.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
rw : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.snd ≫ i₃
rw₁ : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
rw₂ : s.snd ≫ i₂ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
⊢ s.fst ≫ g₁ ≫ g₂ = (s.snd ≫ t₂.snd) ≫ i₃
have rw₃ : s.snd ≫ i₂ ≫ g₂ = s.snd ≫ i₂ ≫ g₂
Tactic: rw [Category.assoc, ← t₂.condition, reassoc_of% s.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
⊢ { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
have create : (l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt) →
  (hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst) →
    (hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd) →
      { l : s.pt ⟶ t₁.pt //
        l ≫ t₁.fst = s.fst ∧
          l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
Tactic: obtain ⟨l, hl, hl'⟩ := PullbackCone.IsLimit.lift' H' s.fst (s.snd ≫ f₂)
    (by rw [Category.assoc, ← t₂.condition, reassoc_of% s.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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
have create : l ≫ t₁.snd = s.snd
Tactic: refine ⟨l, hl, ?_, ?_⟩
-- 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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
create : l ≫ t₁.snd = s.snd
⊢ { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
have create₁ : ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l
Tactic: refine ⟨l, hl, ?_, ?_⟩
-- 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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ l ≫ t₁.snd = s.snd
have create : (l ≫ t₁.snd) ≫ t₂.fst = s.snd ≫ t₂.fst
Tactic: apply PullbackCone.IsLimit.hom_ext H
-- 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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
create : (l ≫ t₁.snd) ≫ t₂.fst = s.snd ≫ t₂.fst
⊢ l ≫ t₁.snd = s.snd
have create₁ : (l ≫ t₁.snd) ≫ t₂.snd = s.snd ≫ t₂.snd
Tactic: apply PullbackCone.IsLimit.hom_ext H
-- 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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m = l
have create : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = l ≫ (t₂.pasteHoriz t₁ hi₂).fst
Tactic: apply PullbackCone.IsLimit.hom_ext H'
-- 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₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
create : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = l ≫ (t₂.pasteHoriz t₁ hi₂).fst
⊢ m = l
have create₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = l ≫ (t₂.pasteHoriz t₁ hi₂).snd
Tactic: apply PullbackCone.IsLimit.hom_ext H'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁
have rw : (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
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₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
rw : (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁
have rw₁ : t₂.fst ≫ t₁.fst ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
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₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
rw : (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
rw₁ : t₂.fst ≫ t₁.fst ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁
have rw₂ : t₂.fst ≫ t₁.snd ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁
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₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
rw : (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
rw₁ : t₂.fst ≫ t₁.fst ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
rw₂ : t₂.fst ≫ t₁.snd ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁
have rw₃ : t₂.fst ≫ i₂ ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁
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₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
have rw : f₁ ≫ t₁.inr ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
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₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
rw : f₁ ≫ t₁.inr ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
have rw₁ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ f₂ ≫ t₂.inr
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₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
rw : f₁ ≫ t₁.inr ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
rw₁ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ f₂ ≫ t₂.inr
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
have rw₂ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
Tactic: rw [reassoc_of% t₁.condition, Category.assoc, ← t₂.condition, ← hi₂]