awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
refine_2₂ : φ ≫ h.p₂ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₂
⊢ φ ≫ h.p₂ = g₂
have refine_2₃ : φ ≫ 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_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₂
⊢ φ ≫ 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₂ = φ₂₃
⊢ φ ≫ h.p₃ = g₃
have refine_3 : φ ≫ 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_3 : φ ≫ h.p₃ = φ₂₃ ≫ h₂₃.p₂
⊢ φ ≫ h.p₃ = g₃
have refine_3₁ : φ ≫ 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_3 : φ ≫ h.p₃ = φ₂₃ ≫ h₂₃.p₂
refine_3₁ : φ ≫ h.p₃ = (φ ≫ h.chosenPullback.p₂) ≫ h₂₃.p₂
⊢ φ ≫ h.p₃ = g₃
have refine_3₂ : φ ≫ 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_3 : φ ≫ h.p₃ = φ₂₃ ≫ h₂₃.p₂
refine_3₁ : φ ≫ h.p₃ = (φ ≫ h.chosenPullback.p₂) ≫ h₂₃.p₂
refine_3₂ : φ ≫ h.p₃ = φ ≫ h.chosenPullback.p₂ ≫ h₂₃.p₂
⊢ φ ≫ h.p₃ = g₃
have refine_3₃ : φ ≫ 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_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₂
⊢ φ ≫ h.p₃ = g₃
have refine_3₄ : φ ≫ 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
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ = φ'
have h₀ : φ ≫ h.p₁₂ = φ' ≫ h.p₁₂
Tactic: apply h.isPullback₂.hom_ext
-- 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
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
h₀ : φ ≫ h.p₁₂ = φ' ≫ h.p₁₂
⊢ φ = φ'
have h₄ : φ ≫ h.p₂₃ = φ' ≫ h.p₂₃
Tactic: apply h.isPullback₂.hom_ext
-- 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₁₃
x : C
a : x ⟶ h₁₂.pullback
b : x ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₂ = a ∧ l ≫ h.p₁₃ = b
have 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
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₁)
-- 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₁₃
x : C
a : x ⟶ h₁₃.pullback
b : x ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ ∃ (l : x ⟶ h.pullback), l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b
have 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
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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
have refine : ∀ (j₁ j₂ : I) (g : j₁ ⟶ j₂), f j₁ = f j₂
Tactic: refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₂
have refine : f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
Tactic: refine (hf j₂).hom_ext ?_ (by simp [f])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
have rw : f j₁ ≫ cF.π.app j₂ = s.π.app j₂
Tactic: rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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₂
⊢ f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
have rw₁ : f j₁ ≫ cF.π.app j₁ ≫ F.map g = s.π.app j₂
Tactic: rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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₂
⊢ f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
have rw₂ : s.π.app j₁ ≫ F.map g = s.π.app j₂
Tactic: rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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₂
⊢ f j₁ ≫ cF.π.app j₂ = f j₂ ≫ cF.π.app j₂
have rw₃ : s.π.app j₂ = s.π.app j₂
Tactic: rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (hypothesis)
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)) ⋯
⊢ IsPullback.lift ⋯ (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ cF.π.app j = s.π.app j
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j
have rw : f j ≫ cF.π.app j = s.π.app j
Tactic: rw [this _ j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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
have refine : ∀ (j₁ j₂ : I) (g : j₁ ⟶ j₂), f j₁ = f j₂
Tactic: refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f j₁ = f j₂
have refine : cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
Tactic: refine (hf j₁).hom_ext (by simp [f]) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
have rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
Tactic: rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
have rw₁ : s.ι.app j₁ = (G.map g ≫ cG.ι.app j₂) ≫ f j₂
Tactic: rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
rw₁ : s.ι.app j₁ = (G.map g ≫ cG.ι.app j₂) ≫ f j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
have rw₂ : s.ι.app j₁ = G.map g ≫ cG.ι.app j₂ ≫ f j₂
Tactic: rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
rw₁ : s.ι.app j₁ = (G.map g ≫ cG.ι.app j₂) ≫ f j₂
rw₂ : s.ι.app j₁ = G.map g ≫ cG.ι.app j₂ ≫ f j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
have rw₃ : s.ι.app j₁ = G.map g ≫ s.ι.app j₂
Tactic: rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 j₁ j₂ : I
g : j₁ ⟶ j₂
rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
rw₁ : s.ι.app j₁ = (G.map g ≫ cG.ι.app j₂) ≫ f j₂
rw₂ : s.ι.app j₁ = G.map g ≫ cG.ι.app j₂ ≫ f j₂
rw₃ : s.ι.app j₁ = G.map g ≫ s.ι.app j₂
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
have rw₄ : s.ι.app j₁ = s.ι.app j₁
Tactic: rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected (goal)
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 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j
have rw : cG.ι.app j ≫ f j = s.ι.app j
Tactic: rw [this _ j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
X Y : WalkingCospan
⊢ Subsingleton (X ⟶ Y)
have allEq : ∀ (a b : X ⟶ Y), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
X Y : WalkingSpan
⊢ Subsingleton (X ⟶ Y)
have allEq : ∀ (a b : X ⟶ Y), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s ≅ t
have apply : ∀ (j : WalkingCospan), s.π.app j = i.hom ≫ t.π.app j
Tactic: apply Cone.ext i _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) none ⟶ F.obj none) (s.π.app none)
    (i.hom ≫ t.π.app none)
have h₁ : Functor.map (Functor.obj (Functor.const WalkingCospan) s.pt) inl ≫ s.π.app one = s.π.app left ≫ F.map inl
Tactic: have h₁ := s.π.naturality WalkingCospan.Hom.inl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : 𝟙 s.pt ≫ s.π.app one = s.π.app left ≫ F.map inl
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) none ⟶ F.obj none) (s.π.app none)
    (i.hom ≫ t.π.app none)
have h₂ : s.π.app one = s.π.app left ≫ F.map inl
Tactic: simp only [Category.id_comp] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) none ⟶ F.obj none) (s.π.app none)
    (i.hom ≫ t.π.app none)
have h₂ : Functor.map (Functor.obj (Functor.const WalkingCospan) t.pt) inl ≫ t.π.app one = t.π.app left ≫ F.map inl
Tactic: have h₂ := t.π.naturality WalkingCospan.Hom.inl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : 𝟙 t.pt ≫ t.π.app one = t.π.app left ≫ F.map inl
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) none ⟶ F.obj none) (s.π.app none)
    (i.hom ≫ t.π.app none)
have h₃ : t.π.app one = t.π.app left ≫ F.map inl
Tactic: simp only [Category.id_comp] at h₂
Cleared hypotheses: h₂