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₁ 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
rw₂ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
have rw₃ : f₁ ≫ i₂ ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
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
H : IsColimit t₁
H' : IsColimit t₂
⊢ IsColimit (t₁.pasteHoriz t₂ hi₂)
have create : (s : PushoutCocone i₁ (f₁ ≫ f₂)) →
  { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
Tactic: apply PushoutCocone.isColimitAux'
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ i₁ ≫ s.inl = f₁ ≫ f₂ ≫ s.inr
have rw : (f₁ ≫ f₂) ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
rw : (f₁ ≫ f₂) ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
⊢ i₁ ≫ s.inl = f₁ ≫ f₂ ≫ s.inr
have rw₁ : f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
have create : (l₁ : t₁.pt ⟶ s.pt) →
  (hl₁ : t₁.inl ≫ l₁ = s.inl) →
    (hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr) →
      { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
        (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
          (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
            ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
              (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
Tactic: obtain ⟨l₁, hl₁, hl₁'⟩ := PushoutCocone.IsColimit.desc' H s.inl (f₂ ≫ s.inr)
    (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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
⊢ «i₂» ≫ l₁ = f₂ ≫ s.inr
have rw : «i₂» ≫ l₁ = t₁.inr ≫ l₁
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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
rw : «i₂» ≫ l₁ = t₁.inr ≫ l₁
⊢ «i₂» ≫ l₁ = f₂ ≫ s.inr
have rw₁ : t₁.inr ≫ l₁ = t₁.inr ≫ l₁
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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
have create : (l₂ : t₂.pt ⟶ s.pt) →
  (hl₂ : t₂.inl ≫ l₂ = l₁) →
    (hl₂' : t₂.inr ≫ l₂ = s.inr) →
      { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
        (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
          (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
            ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
              (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
Tactic: obtain ⟨l₂, hl₂, hl₂'⟩ := PushoutCocone.IsColimit.desc' H' l₁ s.inr (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₁ 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
have create : ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
  (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l₂
Tactic: refine ⟨l₂, by simp [hl₂, hl₁], hl₂', ?_⟩
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ m = l₂
have apply : t₂.inl ≫ m = t₂.inl ≫ l₂
Tactic: apply PushoutCocone.IsColimit.hom_ext H' _ (by simpa [hl₂'] using hm₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (hypothesis)
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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inl ≫ m = t₂.inl ≫ l₂
have hm₃ : t₁.inl ≫ t₂.inl ≫ m = s.inl
Tactic: simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hm₁ hm₂
Cleared hypotheses: hm₁
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₂.inl ≫ m = t₂.inl ≫ l₂
have h₀ : t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
Tactic: apply PushoutCocone.IsColimit.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₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₀ : t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
⊢ t₂.inl ≫ m = t₂.inl ≫ l₂
have h₁ : t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
Tactic: apply PushoutCocone.IsColimit.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₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
have h₀ : s.inl = t₁.inl ≫ t₂.inl ≫ l₂
Tactic: rw [hm₁, ← hl₁, hl₂]
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₀ : s.inl = t₁.inl ≫ t₂.inl ≫ l₂
⊢ t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
have h₁ : t₁.inl ≫ l₁ = t₁.inl ≫ t₂.inl ≫ l₂
Tactic: rw [hm₁, ← hl₁, hl₂]
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₀ : s.inl = t₁.inl ≫ t₂.inl ≫ l₂
h₁ : t₁.inl ≫ l₁ = t₁.inl ≫ t₂.inl ≫ l₂
⊢ t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
have h₂ : t₁.inl ≫ l₁ = t₁.inl ≫ l₁
Tactic: rw [hm₁, ← hl₁, hl₂]
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
have h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
Tactic: rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
have h₂ : f₂ ≫ t₂.inr ≫ m = «i₂» ≫ t₂.inl ≫ l₂
Tactic: rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₂ : f₂ ≫ t₂.inr ≫ m = «i₂» ≫ t₂.inl ≫ l₂
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
have h₃ : f₂ ≫ t₂.inr ≫ m = f₂ ≫ t₂.inr ≫ l₂
Tactic: rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₂ : f₂ ≫ t₂.inr ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₃ : f₂ ≫ t₂.inr ≫ m = f₂ ≫ t₂.inr ≫ l₂
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
have h₄ : f₂ ≫ s.inr = f₂ ≫ t₂.inr ≫ l₂
Tactic: rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
-- 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
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₂ : f₂ ≫ t₂.inr ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₃ : f₂ ≫ t₂.inr ≫ m = f₂ ≫ t₂.inr ≫ l₂
h₄ : f₂ ≫ s.inr = f₂ ≫ t₂.inr ≫ l₂
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
have h₅ : f₂ ≫ s.inr = f₂ ≫ s.inr
Tactic: rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
-- 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
⊢ IsColimit t₂
have create : (s : PushoutCocone «i₂» f₂) →
  { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
Tactic: apply PushoutCocone.isColimitAux'
-- 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
have rw : f₁ ≫ t₁.inr ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
Tactic: rw [reassoc_of% t₁.condition, ← hi₂, 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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
rw : f₁ ≫ t₁.inr ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
have rw₁ : f₁ ≫ «i₂» ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
Tactic: rw [reassoc_of% t₁.condition, ← hi₂, 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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
rw : f₁ ≫ t₁.inr ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
rw₁ : f₁ ≫ «i₂» ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
have rw₂ : f₁ ≫ f₂ ≫ s.inr = (f₁ ≫ f₂) ≫ s.inr
Tactic: rw [reassoc_of% t₁.condition, ← hi₂, 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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
rw : f₁ ≫ t₁.inr ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
rw₁ : f₁ ≫ «i₂» ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
rw₂ : f₁ ≫ f₂ ≫ s.inr = (f₁ ≫ f₂) ≫ s.inr
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
have rw₃ : f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
Tactic: rw [reassoc_of% t₁.condition, ← hi₂, 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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
⊢ { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
have create : (l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt) →
  (hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl) →
    (hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr) →
      { l : t₂.pt ⟶ s.pt //
        t₂.inl ≫ l = s.inl ∧
          t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
Tactic: obtain ⟨l, hl, hl'⟩ := PushoutCocone.IsColimit.desc' H' (g₁ ≫ s.inl) s.inr
    (by rw [reassoc_of% t₁.condition, ← hi₂, 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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
have create : t₂.inl ≫ l = s.inl
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₁ 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
create : t₂.inl ≫ l = s.inl
⊢ { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
have create₁ : ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l
Tactic: refine ⟨l, ?_, hl', ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (hypothesis)
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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ t₂.inl ≫ l = s.inl
have hl₁ : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
Tactic: simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hl hl'
Cleared hypotheses: hl
-- 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
⊢ t₂.inl ≫ l = s.inl
have create : t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
Tactic: apply PushoutCocone.IsColimit.hom_ext H hl
-- 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- 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
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']