awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst_9 : Category.{v₁₀, u₁₀} A'''
inst_10 : Category.{v₁₁, u₁₁} B'''
inst_11 : Category.{v₁₂, u₁₂} C'''
F''' : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A''' B'''
G''' : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C''' B'''
ψ_1 ψ'_1 ψ'' : CatCospanTransform F G F' G'
η_1 : ψ_1 ⟶ ψ'_1
η' : ψ'_1 ⟶ ψ''
φ_1 φ'_1 φ'' : CatCospanTransform F' G' F'' G''
θ_1 : φ_1 ⟶ φ'_1
θ' : φ'_1 ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst_12 : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst_13 : IsIso θ
⊢ ψ ◁ inv θ ≫ ψ ◁ θ = 𝟙 (ψ.comp φ')

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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 θ
hom_inv_id : ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)
⊢ inv (ψ ◁ θ) = ψ ◁ inv θ

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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 θ = 𝟙 (ψ.comp φ)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst_9 : Category.{v₁₀, u₁₀} A'''
inst_10 : Category.{v₁₁, u₁₁} B'''
inst_11 : Category.{v₁₂, u₁₂} C'''
F''' : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A''' B'''
G''' : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C''' B'''
ψ_1 ψ'_1 ψ'' : CatCospanTransform F G F' G'
η_1 : ψ_1 ⟶ ψ'_1
η' : ψ'_1 ⟶ ψ''
φ_1 φ'_1 φ'' : CatCospanTransform F' G' F'' G''
θ_1 : φ_1 ⟶ φ'_1
θ' : φ'_1 ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst_12 : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst_13 : IsIso θ
⊢ η ▷ φ ≫ inv η ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst_9 : Category.{v₁₀, u₁₀} A'''
inst_10 : Category.{v₁₁, u₁₁} B'''
inst_11 : Category.{v₁₂, u₁₂} C'''
F''' : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A''' B'''
G''' : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C''' B'''
ψ_1 ψ'_1 ψ'' : CatCospanTransform F G F' G'
η_1 : ψ_1 ⟶ ψ'_1
η' : ψ'_1 ⟶ ψ''
φ_1 φ'_1 φ'' : CatCospanTransform F' G' F'' G''
θ_1 : φ_1 ⟶ φ'_1
θ' : φ'_1 ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst_12 : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst_13 : IsIso θ
⊢ inv η ▷ φ ≫ η ▷ φ = 𝟙 (ψ'.comp φ)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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''
hom_inv_id : η ▷ φ ≫ inv η ▷ φ = 𝟙 (ψ.comp φ)
⊢ inv (η ▷ φ) = inv η ▷ φ

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
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 η ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
rw₁ rw₂ : h.p = h.p
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
rw [← h.condition, hp₁]

Premises used: CategoryTheory.Limits.ChosenPullback.condition, CategoryTheory.Limits.ChosenPullback.hp₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
f g : Y ⟶ h.pullback
h₁ : f ≫ h.p₁ = g ≫ h.p₁
h₂ : f ≫ h.p₂ = g ≫ h.p₂
⊢ f = g

Tactic:
h.isPullback.hom_ext h₁ h₂

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.Limits.ChosenPullback.isPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
l : h.LiftStruct g₁ g₂ b
⊢ g₁ ≫ f₁ = g₂ ≫ f₂

Tactic:
simp only [← l.f_p₁, ← l.f_p₂, Category.assoc, h.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁, CategoryTheory.Limits.ChosenPullback.condition, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
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 }
⊢ { 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 }

Tactic:
obtain rfl : f = f' := by cat_disch

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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'_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 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
obtain : ∀ (l : Y ⟶ h.pullback) (h₁ : l ≫ h.p₁ = g₁) (h₂ : l ≫ h.p₂ = g₂), Nonempty.{v + 1} (h.LiftStruct g₁ g₂ b)
⊢ Nonempty.{v + 1} (h.LiftStruct g₁ g₂ b)

Tactic:
obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.IsPullback.exists_lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₁
rw₂ rw₃ : g₁ ≫ f₁ = g₁ ≫ f₁
⊢ l ≫ h.p = b

Tactic:
rw [← h.hp₁, ← hf₁, reassoc_of% h₁]

Premises used: CategoryTheory.Limits.ChosenPullback.hp₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂
⊢ Nonempty.{v + 1} (h.LiftStruct g₁ g₂ b)

Tactic:
exact ⟨{
    f := l
    f_p₁ := h₁
    f_p₂ := h₂
    f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] }⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
Goal:
C : Type u
inst : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
w : 𝟙 X ≫ f = 𝟙 X ≫ f
hf₁ : 𝟙 X ≫ f = f
⊢ Nonempty.{v + 1} h.Diagonal

Tactic:
apply LiftStruct.nonempty

Premises used: CategoryTheory.Limits.ChosenPullback.LiftStruct.nonempty
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
Goal:
C : Type u
inst : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
w w₁ w₂ w₃ : 𝟙 X ≫ f = 𝟙 X ≫ f
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₁

Tactic:
simp [p₁₂, hp₁]

Premises used: CategoryTheory.Limits.ChosenPullback₃.hp₁, CategoryTheory.Limits.ChosenPullback₃.p₁₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂

Tactic:
simp [p₁₂, p₂]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₁₂, CategoryTheory.Limits.ChosenPullback₃.p₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂

Tactic:
simp [p₂₃, p₂]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₂, CategoryTheory.Limits.ChosenPullback₃.p₂₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃

Tactic:
simp [p₂₃, hp₃]

Premises used: CategoryTheory.Limits.ChosenPullback₃.hp₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₁

Tactic:
simp [p₁₃]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₁₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃

Tactic:
simp [p₁₃]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₁₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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

Tactic:
simpa only [← hp₁, Category.assoc, h₁₃.hp₁, h.l.f_p] using h.l.f_p₁.symm =≫ f₁

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁, CategoryTheory.Limits.ChosenPullback₃.hp₁, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p, CategoryTheory.Limits.ChosenPullback₃.l, CategoryTheory.Limits.ChosenPullback.hp₁, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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

Tactic:
simpa only [← hp₃, Category.assoc, h₁₃.hp₂, h.l.f_p] using h.l.f_p₂.symm =≫ f₃

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p, CategoryTheory.Limits.ChosenPullback₃.hp₃, CategoryTheory.Limits.ChosenPullback₃.l, CategoryTheory.Limits.ChosenPullback.hp₂, CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃
rw₃ rw₄ : h.p₃ ≫ f₃ = h.p₃ ≫ f₃
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc, CategoryTheory.Limits.ChosenPullback.condition, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂_assoc, CategoryTheory.Limits.ChosenPullback₃.w₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
rw₂ rw₃ : h.p = h.p
⊢ h.p₁₂ ≫ h₁₂.p = h.p

Tactic:
rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]

Premises used: CategoryTheory.Limits.ChosenPullback₃.w₂, CategoryTheory.Limits.ChosenPullback.hp₂, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
rw₂ rw₃ : h.p = h.p
⊢ h.p₂₃ ≫ h₂₃.p = h.p

Tactic:
rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc, CategoryTheory.Limits.ChosenPullback.hp₂, CategoryTheory.Limits.ChosenPullback₃.w₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
rw₂ rw₃ : h.p = h.p
⊢ h.p₁₃ ≫ h₁₃.p = h.p

Tactic:
rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁]

Premises used: CategoryTheory.Limits.ChosenPullback.hp₁, CategoryTheory.Limits.ChosenPullback₃.w₁, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂ ≫ f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃ ≫ f₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃ ≫ f₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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
obtain :
  ∀ (φ₁₂ : Y ⟶ h₁₂.pullback) (w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁) (w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂),
    ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ 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)

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.Limits.ChosenPullback₃.w₂, CategoryTheory.IsPullback.exists_lift, CategoryTheory.Limits.ChosenPullback₃.w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂
obtain :
  ∀ (φ₂₃ : Y ⟶ h₂₃.pullback) (w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂) (w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃),
    ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ 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)

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.IsPullback.exists_lift, CategoryTheory.Limits.ChosenPullback₃.w₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃
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₃
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃

Tactic:
obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by cat_disch)

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.IsPullback.exists_lift, CategoryTheory.Limits.ChosenPullback₃.chosenPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₃

Tactic:
⟨φ, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
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₂
refine_3 : φ ≫ h.p₃ = g₃
⊢ ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃

Tactic:
refine ⟨φ, ?_, ?_, ?_⟩