awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ = φ₁₂ ≫ 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₁
refine_1₄ refine_1₅ : φ ≫ h.p₁ = φ ≫ h.p₁
⊢ φ ≫ h.p₁ = g₁

Tactic:
rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂, CategoryTheory.Limits.ChosenPullback₃.p₁₂_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₁₃
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₂
refine_2₂ : φ ≫ h.p₂ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₂
refine_2₃ : φ ≫ h.p₂ = φ ≫ h.p₁₂ ≫ h₁₂.p₂
refine_2₄ refine_2₅ : φ ≫ h.p₂ = φ ≫ h.p₂
⊢ φ ≫ h.p₂ = g₂

Tactic:
rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂, CategoryTheory.Limits.ChosenPullback₃.p₁₂_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₁₃
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_3 : φ ≫ h.p₃ = φ₂₃ ≫ h₂₃.p₂
refine_3₁ : φ ≫ h.p₃ = (φ ≫ h.chosenPullback.p₂) ≫ h₂₃.p₂
refine_3₂ : φ ≫ h.p₃ = φ ≫ h.chosenPullback.p₂ ≫ h₂₃.p₂
refine_3₃ : φ ≫ h.p₃ = φ ≫ h.p₂₃ ≫ h₂₃.p₂
refine_3₄ refine_3₅ : φ ≫ h.p₃ = φ ≫ h.p₃
⊢ φ ≫ h.p₃ = g₃

Tactic:
rw [← w₃, ← w₂₃, Category.assoc, ← p₂₃, p₂₃_p₃]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ChosenPullback₃.p₂₃_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₁₃
⊢ IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁

Tactic:
h.chosenPullback.isPullback

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.Limits.ChosenPullback₃.p₁₂, CategoryTheory.Limits.ChosenPullback₃.chosenPullback, 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₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
h₀ : φ ≫ h.p₁₂ = φ' ≫ h.p₁₂
h₄ : φ ≫ h.p₂₃ = φ' ≫ h.p₂₃
⊢ φ = φ'

Tactic:
apply h.isPullback₂.hom_ext

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₂ 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₁₃ ≫ h₁₃.p₁

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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₂ = x_2 ≫ h.p₁₂
h₂ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
⊢ x_1 ≫ h.p₁ = x_2 ≫ h.p₁

Tactic:
simpa using h₁ =≫ h₁₂.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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₂ = x_2 ≫ h.p₁₂
h₂ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
⊢ x_1 ≫ h.p₂ = x_2 ≫ h.p₂

Tactic:
simpa using h₁ =≫ h₁₂.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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₂ = x_2 ≫ h.p₁₂
h₂ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
⊢ x_1 ≫ h.p₃ = x_2 ≫ h.p₃

Tactic:
simpa using h₂ =≫ h₁₃.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₁₃
x : C
a : x ⟶ h₁₂.pullback
b : x ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ (a ≫ h₁₂.p₂) ≫ f₂ = (a ≫ 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₁₃
x : C
a : x ⟶ h₁₂.pullback
b : x ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ (b ≫ h₁₃.p₂) ≫ f₃ = (a ≫ h₁₂.p₁) ≫ f₁

Tactic:
simpa using w.symm =≫ f₁

Premises used: 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₁₃
x : C
a : x ⟶ h₁₂.pullback
b : x ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
obtain :
  ∀ (φ : x ⟶ h.pullback) (hφ₁ : φ ≫ h.p₁ = a ≫ h₁₂.p₁) (hφ₂ : φ ≫ h.p₂ = a ≫ h₁₂.p₂) (hφ₃ : φ ≫ h.p₃ = b ≫ h₁₃.p₂),
    ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₂ = a ∧ l ≫ h.p₁₃ = b
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₂ = a ∧ l ≫ h.p₁₃ = b

Tactic:
obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
        h.exists_lift (a ≫ h₁₂.p₁) (a ≫ h₁₂.p₂) (b ≫ h₁₃.p₂) _ rfl
          (by simp) (by simpa using w.symm =≫ f₁)

Premises used: CategoryTheory.Limits.ChosenPullback.p₂, CategoryTheory.Limits.ChosenPullback.p₁, CategoryTheory.CategoryStruct.comp, rfl, CategoryTheory.Limits.ChosenPullback₃.exists_lift
-- 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₁₃
x : C
a : x ⟶ h₁₂.pullback
b : x ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
φ : x ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₂.p₁
hφ₂ : φ ≫ h.p₂ = a ≫ h₁₂.p₂
hφ₃ : φ ≫ h.p₃ = b ≫ h₁₃.p₂
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₂ = a ∧ l ≫ h.p₁₃ = b

Tactic:
exact ⟨φ, by cat_disch, by 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₂₃ ≫ h₂₃.p₂

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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
h₂ : x_1 ≫ h.p₂₃ = x_2 ≫ h.p₂₃
⊢ x_1 ≫ h.p₁ = x_2 ≫ h.p₁

Tactic:
simpa using h₁ =≫ h₁₃.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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
h₂ : x_1 ≫ h.p₂₃ = x_2 ≫ h.p₂₃
⊢ x_1 ≫ h.p₂ = x_2 ≫ h.p₂

Tactic:
simpa using h₂ =≫ h₂₃.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₁₃
x : C
x_1 x_2 : x ⟶ h.pullback
h₁ : x_1 ≫ h.p₁₃ = x_2 ≫ h.p₁₃
h₂ : x_1 ≫ h.p₂₃ = x_2 ≫ h.p₂₃
⊢ x_1 ≫ h.p₃ = x_2 ≫ h.p₃

Tactic:
simpa using h₁ =≫ h₁₃.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₁₃
x : C
a : x ⟶ h₁₃.pullback
b : x ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ (b ≫ h₂₃.p₁) ≫ f₂ = (a ≫ h₁₃.p₁) ≫ f₁

Tactic:
simpa using w.symm =≫ f₃

Premises used: 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₁₃
x : C
a : x ⟶ h₁₃.pullback
b : x ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ (a ≫ h₁₃.p₂) ≫ f₃ = (a ≫ 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₁₃
x : C
a : x ⟶ h₁₃.pullback
b : x ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
obtain :
  ∀ (φ : x ⟶ h.pullback) (hφ₁ : φ ≫ h.p₁ = a ≫ h₁₃.p₁) (hφ₂ : φ ≫ h.p₂ = b ≫ h₂₃.p₁) (hφ₃ : φ ≫ h.p₃ = a ≫ h₁₃.p₂),
    ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b

Tactic:
obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
        h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl
          (by simpa using w.symm =≫ f₃) (by simp)

Premises used: CategoryTheory.Limits.ChosenPullback.p₂, CategoryTheory.Limits.ChosenPullback.p₁, CategoryTheory.CategoryStruct.comp, rfl, CategoryTheory.Limits.ChosenPullback₃.exists_lift
-- 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₁₃
x : C
a : x ⟶ h₁₃.pullback
b : x ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
φ : x ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₃.p₁
hφ₂ : φ ≫ h.p₂ = b ≫ h₂₃.p₁
hφ₃ : φ ≫ h.p₃ = a ≫ h₁₃.p₂
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b

Tactic:
exact ⟨φ, by cat_disch, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
⊢ Eq (α := s.pt ⟶ G.obj (Classical.arbitrary I)) (s.π.app (Classical.arbitrary I) ≫ α.app (Classical.arbitrary I))
    (hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app (Classical.arbitrary I))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j i : I
⊢ s.π.app i ≫ α.app i = hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j_1 : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j : I
⊢ f i = f j

Tactic:
constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j

Premises used: CategoryTheory.constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j_1 : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j : I
refine : ∀ (j₁ j₂ : I) (g : j₁ ⟶ j₂), f j₁ = f j₂
⊢ f i = f j

Tactic:
refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j

Premises used: CategoryTheory.constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j_1 : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f j₁ ≫ f_1.hom = f j₂ ≫ f_1.hom

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j_1 : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
refine : f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
⊢ f j₁ = f j₂

Tactic:
refine (hf j₂).hom_ext ?_ (by simp [f])

Premises used: CategoryTheory.IsPullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j_1 : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
rw : f j₁ ≫ cF.π.app j₂ = s.π.app j₂
rw₁ : f j₁ ≫ cF.π.app j₁ ≫ F.map g = s.π.app j₂
rw₂ : s.π.app j₁ ≫ F.map g = s.π.app j₂
rw₃ rw₄ : s.π.app j₂ = s.π.app j₂
⊢ f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂

Tactic:
rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.IsPullback.lift_fst, CategoryTheory.IsPullback.lift_fst_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
⊢ ∀ (i j : I), f i = f j

Tactic:
have (i j : _) : f i = f j := by
      refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
      refine (hf j₂).hom_ext ?_ (by simp [f])
      rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
change : f (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j
⊢ IsPullback.lift ⋯ (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ cF.π.app j = s.π.app j

Tactic:
change f _ ≫ _ = _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
rw : f j ≫ cF.π.app j = s.π.app j
⊢ f (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j

Tactic:
rw [this _ j]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f_1 : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f_1.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : (i : I) → s.pt ⟶ cF.pt := fun (i : I) ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f j ≫ cF.π.app j = s.π.app j

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
g : s.pt ⟶ cF.pt
hg : ∀ (j : I), g ≫ cF.π.app j = s.π.app j
⊢ Eq (α := s.pt ⟶ F.obj (Classical.arbitrary I))
    (g ≫ cF.π.app (Classical.arbitrary I) : s.pt ⟶ F.obj (Classical.arbitrary I))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I))
        (IsPullback.lift ⋯ (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ :
          s.pt ⟶ Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I))
        (cF.π.app (Classical.arbitrary I) :
          Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I) ⟶
            F.obj (Classical.arbitrary I)) :
      s.pt ⟶ F.obj (Classical.arbitrary I))

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
g : s.pt ⟶ cF.pt
hg : ∀ (j : I), g ≫ cF.π.app j = s.π.app j
⊢ ∀ (j : I),
    (g ≫ f.hom) ≫ cG.π.app j =
      (IsPullback.lift ⋯ (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ f.hom) ≫
        cG.π.app j

Tactic:
simp [reassoc_of% hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
⊢ Eq (α := F.obj (Classical.arbitrary I) ⟶ s.pt)
    (cF.ι.app (Classical.arbitrary I) ≫ hcF.desc ((Cocone.precompose α).obj s) : F.obj (Classical.arbitrary I) ⟶ s.pt)
    (α.app (Classical.arbitrary I) ≫ s.ι.app (Classical.arbitrary I) : F.obj (Classical.arbitrary I) ⟶ s.pt)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j i : I
⊢ cF.ι.app i ≫ hcF.desc ((Cocone.precompose α).obj s) = α.app i ≫ s.ι.app i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j_1 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j : I
⊢ f i = f j

Tactic:
constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j

Premises used: CategoryTheory.constant_of_preserves_morphisms