awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)) ∧
    ∀ (y : c ⟶ c'),
      (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y →
        y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
have h₁ : (φ ≫ ψ) ≫ map p g ψ (S' := p.obj c') (g := h) sorry (map p f φ sorry τ) = τ
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
h₁ : (φ ≫ ψ) ≫ map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ) = τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)) ∧
    ∀ (y : c ⟶ c'),
      (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y →
        y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
have h₂ : ∀ (y : c ⟶ c'),
  (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y → y = map p g ψ (S' := p.obj c') (g := h) sorry (map p f φ sorry τ)
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) π' → π' = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
have h₁ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : (φ ≫ ψ) ≫ π' = τ), π' = map p g ψ (S' := p.obj c') (g := h) sorry (map p f φ sorry τ)
Tactic: ⟨hπ'₁, hπ'₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : (φ ≫ ψ) ≫ π' = τ
⊢ π' = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
have h₁ : ψ ≫ π' = map p f φ sorry τ
Tactic: apply map_uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : (φ ≫ ψ) ≫ π' = τ
⊢ ψ ≫ π' = map p f φ ⋯ τ
have h₁ : φ ≫ ψ ≫ π' = τ
Tactic: apply map_uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∃! χ : c ⟶ c', p.IsHomLift h χ ∧ ψ ≫ χ = τ
have h₁ : (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) sorry (φ ≫ τ)) ∧
  ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) sorry (φ ≫ τ)
Tactic: use map p (f ≫ g) (φ ≫ ψ) (f' := f ≫ g ≫ h) (assoc f g h).symm (φ ≫ τ)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
have h₁ : ψ ≫ map p (f ≫ g) (φ ≫ ψ) sorry (φ ≫ τ) = τ
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
have h₂ : ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) sorry (φ ≫ τ)
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) π' → π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
have h₁ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : ψ ≫ π' = τ), π' = map p (f ≫ g) (φ ≫ ψ) sorry (φ ≫ τ)
Tactic: ⟨hπ'₁, hπ'₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
have h₁ : (φ ≫ ψ) ≫ π' = φ ≫ τ
Tactic: apply map_uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst_2 : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ.hom ≫ χ = τ
have h : (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ) ∧
  ∀ (y : b ⟶ b'), (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ
Tactic: use φ.inv ≫ τ
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst_2 : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ) ∧
    ∀ (y : b ⟶ b'), (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ
have h : (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ)
Tactic: refine ⟨?_, by cat_disch⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : IsIso f
⊢ IsIso φ
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsStronglyCocartesian (p.map φ) φ] [IsIso (p.map φ)], IsIso φ
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2, inst_3
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
⊢ IsIso φ
have h : φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
Tactic: use φ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
have inv_hom : φ ≫ φ' = 𝟙 a
Tactic: have inv_hom : φ ≫ φ' = 𝟙 a := fac p (p.map φ) φ _ (𝟙 a)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
have h : φ' ≫ φ = 𝟙 b
Tactic: refine ⟨inv_hom, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
have rw : p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)
Tactic: rw [← IsIso.inv_hom_id (p.map φ)]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ' ≫ φ = 𝟙 b
have h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
Tactic: have h₁ : IsHomLift p (𝟙 (p.obj b)) (φ' ≫ φ) := by
    rw [← IsIso.inv_hom_id (p.map φ)]
    apply IsHomLift.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ' ≫ φ = 𝟙 b
have h : φ ≫ φ' ≫ φ = φ ≫ 𝟙 b
Tactic: apply IsStronglyCocartesian.ext p (p.map φ) φ (𝟙 (p.obj b))
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cocartesian (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S S' : 𝒮
a b b' : 𝒳
f : R ⟶ S
f' : R ⟶ S'
g : S ≅ S'
h : f' = f ≫ g.hom
φ : a ⟶ b
φ' : a ⟶ b'
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian f' φ'
⊢ p.IsHomLift (R := R) (S := S) ((fun (x : R ⟶ S') ↦ x ≫ g.inv) (f ≫ g.hom)) φ
have simp : p.IsHomLift f φ
Tactic: simp only [assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fiber (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
X Y Z : p.Fiber S
φ : { φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳) // p.IsHomLift (𝟙 S) φ }
ψ : { φ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳) // p.IsHomLift (𝟙 S) φ }
⊢ p.IsHomLift (𝟙 S) ((↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳)) ≫ (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳)))
have this : p.IsHomLift (𝟙 S) (↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳))
Tactic: have := φ.2
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fiber (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
X Y Z : p.Fiber S
φ : { φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳) // p.IsHomLift (𝟙 S) φ }
ψ : { φ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳) // p.IsHomLift (𝟙 S) φ }
this : p.IsHomLift (𝟙 S) (↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳))
⊢ p.IsHomLift (𝟙 S) ((↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳)) ≫ (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳)))
have this₁ : p.IsHomLift (𝟙 S) (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳))
Tactic: have := ψ.2
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
a : 𝒳
R S : 𝒮
ha : p.obj a = S
f : R ⟶ S
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
have subst : ∀ (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
Tactic: subst ha
Cleared hypotheses: S, ha, f
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have h : (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ ≫ ψ) ∧
  ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
Tactic: use τ ≫ ψ
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ ≫ ψ) ∧
    ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
have h : ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
Tactic: refine ⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ ≫ ψ
have h : ∀ (hπ : p.IsHomLift g π) (hπ_comp : π ≫ φ = φ'), π = τ ≫ ψ
Tactic: ⟨hπ, hπ_comp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ ≫ ψ
have h : IsCartesian.map p g ψ π ≫ ψ = τ ≫ ψ
Tactic: rw [← fac p g ψ π]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ IsCartesian.map p g ψ π ≫ ψ = τ ≫ ψ
have h : IsCartesian.map p g ψ π = τ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ IsCartesian.map p g ψ π = τ
have h : IsCartesian.map p g ψ π ≫ ψ ≫ φ = φ'
Tactic: apply map_uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ IsCartesian.map p g ψ π ≫ ψ ≫ φ = φ'
have h : (IsCartesian.map p g ψ π ≫ ψ) ≫ φ = φ'
Tactic: rwa [← assoc, IsCartesian.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsCartesian f φ
⊢ p.IsStronglyCartesian f φ
have universal_property' : ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
φ' : c ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have universal_property' : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} (g : p.obj c ⟶ p.obj a) [p.IsCartesian (p.map φ) φ] [hφ' : p.IsHomLift (g ≫ p.map φ) φ'],
  ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2, g, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have universal_property' : ∀ (a' : 𝒳) (ψ : a' ⟶ b) (hψ : p.IsStronglyCartesian (p.map φ) ψ), ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Tactic: obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have h₁ : (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
  ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
Tactic: use τ' ≫ Φ.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
have h₁ : (τ' ≫ Φ.hom) ≫ φ = φ'
Tactic: refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
h₁ : (τ' ≫ Φ.hom) ≫ φ = φ'
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
have h₂ : ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
Tactic: refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ' ≫ Φ.hom
have h₁ : ∀ (hπ : p.IsHomLift g π) (hπ_comp : π ≫ φ = φ'), π = τ' ≫ Φ.hom
Tactic: ⟨hπ, hπ_comp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ' ≫ Φ.hom
have h₁ : π ≫ Φ.inv = τ'
Tactic: rw [← Iso.comp_inv_eq]