awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
left : IsIso f.left
left_1 : IsIso f.base
right : IsIso f.right
⊢ IsIso f
have h : f ≫ (mkIso (asIso f.left) (asIso f.right) (asIso f.base) sorry sorry).inv = 𝟙 ψ' ∧
  (mkIso (asIso f.left) (asIso f.right) (asIso f.base) sorry sorry).inv ≫ f = 𝟙 ψ'
Tactic: use mkIso (asIso f.left) (asIso f.right) (asIso f.base)
      f.left_coherence f.right_coherence |>.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ : CatCospanTransform F G F' G'
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst_9 : IsIso θ
⊢ inv (ψ ◁ θ) = ψ ◁ inv θ
have hom_inv_id : ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst_9 : IsIso η
φ : CatCospanTransform F' G' F'' G''
⊢ inv (η ▷ φ) = inv η ▷ φ
have hom_inv_id : η ▷ φ ≫ inv η ▷ φ = 𝟙 (ψ.comp φ)
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
⊢ h.p₂ ≫ f₂ = h.p
have rw : h.p₁ ≫ f₁ = h.p
Tactic: rw [← h.condition, hp₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
rw : h.p₁ ≫ f₁ = h.p
⊢ h.p₂ ≫ f₂ = h.p
have rw₁ : h.p = h.p
Tactic: rw [← h.condition, hp₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
f : Y ⟶ h.pullback
f_p₁ : f ≫ h.p₁ = g₁
f_p₂ : f ≫ h.p₂ = g₂
f_p : f ≫ h.p = b
f' : Y ⟶ h.pullback
f'_p₁ : f' ≫ h.p₁ = g₁
f'_p₂ : f' ≫ h.p₂ = g₂
f_p_1 : f' ≫ h.p = b
⊢ { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p : h.LiftStruct g₁ g₂ b } =
    { f := f', f_p₁ := f'_p₁, f_p₂ := f'_p₂, f_p := f_p_1 }
have obtain : ∀ (f'_p₁ : f ≫ h.p₁ = g₁) (f'_p₂ : f ≫ h.p₂ = g₂) (f_p_2 : f ≫ h.p = b),
  { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p : h.LiftStruct g₁ g₂ b } =
    { f := f, f_p₁ := f'_p₁, f_p₂ := f'_p₂, f_p := f_p_2 }
Tactic: obtain rfl : f = f' := by cat_disch
Cleared hypotheses: f', f'_p₁, f'_p₂, f_p_1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
⊢ Nonempty.{v + 1} (h.LiftStruct g₁ g₂ b)
have obtain : ∀ (l : Y ⟶ h.pullback) (h₁ : l ≫ h.p₁ = g₁) (h₂ : l ≫ h.p₂ = g₂), Nonempty.{v + 1} (h.LiftStruct g₁ g₂ b)
Tactic: obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ l ≫ h.p = b
have rw : l ≫ h.p₁ ≫ f₁ = b
Tactic: rw [← h.hp₁, ← hf₁, reassoc_of% h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
rw : l ≫ h.p₁ ≫ f₁ = b
⊢ l ≫ h.p = b
have rw₁ : l ≫ h.p₁ ≫ f₁ = g₁ ≫ f₁
Tactic: rw [← h.hp₁, ← hf₁, reassoc_of% h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
rw : l ≫ h.p₁ ≫ f₁ = b
rw₁ : l ≫ h.p₁ ≫ f₁ = g₁ ≫ f₁
⊢ l ≫ h.p = b
have rw₂ : g₁ ≫ f₁ = g₁ ≫ f₁
Tactic: rw [← h.hp₁, ← hf₁, reassoc_of% h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ Nonempty.{v + 1} h.Diagonal
have w : 𝟙 X ≫ f = 𝟙 X ≫ f
Tactic: apply LiftStruct.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
w : 𝟙 X ≫ f = 𝟙 X ≫ f
⊢ Nonempty.{v + 1} h.Diagonal
have hf₁ : 𝟙 X ≫ f = f
Tactic: apply LiftStruct.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p
have rw : h.p₂₃ ≫ h₂₃.p₁ ≫ f₂ = h.p
Tactic: rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₂₃ ≫ h₂₃.p₁ ≫ f₂ = h.p
⊢ h.p₂ ≫ f₂ = h.p
have rw₁ : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
Tactic: rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₂₃ ≫ h₂₃.p₁ ≫ f₂ = h.p
rw₁ : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
⊢ h.p₂ ≫ f₂ = h.p
have rw₂ : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p₃ ≫ f₃
Tactic: rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₂₃ ≫ h₂₃.p₁ ≫ f₂ = h.p
rw₁ : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
rw₂ : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p₃ ≫ f₃
⊢ h.p₂ ≫ f₂ = h.p
have rw₃ : h.p₃ ≫ f₃ = h.p₃ ≫ f₃
Tactic: rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p = h.p
have rw : h.p₁₂ ≫ h₁₂.p₂ ≫ f₂ = h.p
Tactic: rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₁₂ ≫ h₁₂.p₂ ≫ f₂ = h.p
⊢ h.p₁₂ ≫ h₁₂.p = h.p
have rw₁ : h.p₂ ≫ f₂ = h.p
Tactic: rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₁₂ ≫ h₁₂.p₂ ≫ f₂ = h.p
rw₁ : h.p₂ ≫ f₂ = h.p
⊢ h.p₁₂ ≫ h₁₂.p = h.p
have rw₂ : h.p = h.p
Tactic: rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p = h.p
have rw : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
Tactic: rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
⊢ h.p₂₃ ≫ h₂₃.p = h.p
have rw₁ : h.p₃ ≫ f₃ = h.p
Tactic: rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p
rw₁ : h.p₃ ≫ f₃ = h.p
⊢ h.p₂₃ ≫ h₂₃.p = h.p
have rw₂ : h.p = h.p
Tactic: rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₃ ≫ h₁₃.p = h.p
have rw : h.p₁₃ ≫ h₁₃.p₁ ≫ f₁ = h.p
Tactic: rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₁₃ ≫ h₁₃.p₁ ≫ f₁ = h.p
⊢ h.p₁₃ ≫ h₁₃.p = h.p
have rw₁ : h.p₁ ≫ f₁ = h.p
Tactic: rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
rw : h.p₁₃ ≫ h₁₃.p₁ ≫ f₁ = h.p
rw₁ : h.p₁ ≫ f₁ = h.p
⊢ h.p₁₃ ≫ h₁₃.p = h.p
have rw₂ : h.p = h.p
Tactic: rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have obtain : ∀ (φ₁₂ : Y ⟶ h₁₂.pullback) (w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁) (w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂),
  ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
Tactic: obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have obtain : ∀ (φ₂₃ : Y ⟶ h₂₃.pullback) (w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂) (w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃),
  ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
Tactic: obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have obtain : ∀ (φ : Y ⟶ h.chosenPullback.pullback) (w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂) (w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃),
  ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
Tactic: obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have refine_1 : φ ≫ h.p₁ = g₁
Tactic: refine ⟨φ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = g₁
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have refine_2 : φ ≫ h.p₂ = g₂
Tactic: refine ⟨φ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = g₁
refine_2 : φ ≫ h.p₂ = g₂
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
have refine_3 : φ ≫ h.p₃ = g₃
Tactic: refine ⟨φ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = g₁
have refine_1 : φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
Tactic: rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
⊢ φ ≫ h.p₁ = g₁
have refine_1₁ : φ ≫ h.p₁ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₁
Tactic: rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
refine_1₁ : φ ≫ h.p₁ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₁
⊢ φ ≫ h.p₁ = g₁
have refine_1₂ : φ ≫ h.p₁ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₁
Tactic: rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
refine_1₁ : φ ≫ h.p₁ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₁
refine_1₂ : φ ≫ h.p₁ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₁
⊢ φ ≫ h.p₁ = g₁
have refine_1₃ : φ ≫ h.p₁ = φ ≫ h.p₁₂ ≫ h₁₂.p₁
Tactic: rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_1 : φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
refine_1₁ : φ ≫ h.p₁ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₁
refine_1₂ : φ ≫ h.p₁ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₁
refine_1₃ : φ ≫ h.p₁ = φ ≫ h.p₁₂ ≫ h₁₂.p₁
⊢ φ ≫ h.p₁ = g₁
have refine_1₄ : φ ≫ h.p₁ = φ ≫ h.p₁
Tactic: rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₂ = g₂
have refine_2 : φ ≫ h.p₂ = φ₁₂ ≫ h₁₂.p₂
Tactic: rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_2 : φ ≫ h.p₂ = φ₁₂ ≫ h₁₂.p₂
⊢ φ ≫ h.p₂ = g₂
have refine_2₁ : φ ≫ h.p₂ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₂
Tactic: rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
refine_2 : φ ≫ h.p₂ = φ₁₂ ≫ h₁₂.p₂
refine_2₁ : φ ≫ h.p₂ = (φ ≫ h.chosenPullback.p₁) ≫ h₁₂.p₂
⊢ φ ≫ h.p₂ = g₂
have refine_2₂ : φ ≫ h.p₂ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₂
Tactic: rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]