awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∃! χ : a' ⟶ a, p.IsHomLift h χ ∧ χ ≫ φ = τ
have h₂ : (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) sorry (τ ≫ ψ)) ∧
  ∀ (y : a' ⟶ a),
    (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) sorry (τ ≫ ψ)
Tactic: use map p (f ≫ g) (φ ≫ ψ) (f' := h ≫ f ≫ g) rfl (τ ≫ ψ)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
have h₂ : map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) sorry (τ ≫ ψ) ≫ φ = τ
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
h₂ : map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ) ≫ φ = τ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
have h₃ : ∀ (y : a' ⟶ a),
  (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) sorry (τ ≫ ψ)
Tactic: refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) π' → π' = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
have h₂ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : π' ≫ φ = τ), π' = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) sorry (τ ≫ ψ)
Tactic: ⟨hπ'₁, hπ'₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
have h₂ : π' ≫ φ ≫ ψ = τ ≫ ψ
Tactic: apply map_uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ.hom = τ
have h : (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) (τ ≫ φ.inv) ∧
  ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) y → y = τ ≫ φ.inv
Tactic: use τ ≫ φ.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) (τ ≫ φ.inv) ∧
    ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) y → y = τ ≫ φ.inv
have h : (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) (τ ≫ φ.inv)
Tactic: refine ⟨?_, by cat_disch⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian f φ
inst_3 : IsIso f
⊢ IsIso φ
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsStronglyCartesian (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.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
⊢ IsIso φ
have h : φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
Tactic: use φ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
have inv_hom : φ' ≫ φ = 𝟙 b
Tactic: have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
have h : φ ≫ φ' = 𝟙 a
Tactic: refine ⟨?_, inv_hom⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
have rw : p.IsHomLift (p.map φ ≫ CategoryTheory.inv (p.map φ)) (φ ≫ φ')
Tactic: rw [← IsIso.hom_inv_id (p.map φ)]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a
have h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
Tactic: have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') := by
    rw [← IsIso.hom_inv_id (p.map φ)]
    apply IsHomLift.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (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.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ φ ≫ φ' = 𝟙 a
have h : (φ ≫ φ') ≫ φ = 𝟙 a ≫ φ
Tactic: apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Cartesian (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian f' φ'
⊢ p.IsHomLift g.inv (domainIsoOfBaseIso p h φ φ').inv
have this : p.IsHomLift (R := R) (S := S) ((fun (x : R' ⟶ S) ↦ g.inv ≫ x) (g.hom ≫ f)) φ
Tactic: haveI : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ := by
    simpa using IsCartesian.toIsHomLift
-- 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.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift (𝟙 S) ψ
inst_4 : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'
have rw : IsCocartesian.map p f φ (φ ≫ ψ) = ψ'
Tactic: rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift (𝟙 S) ψ
inst_4 : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
rw : IsCocartesian.map p f φ (φ ≫ ψ) = ψ'
⊢ ψ = ψ'
have rw₁ : IsCocartesian.map p f φ (φ ≫ ψ) = IsCocartesian.map p f φ (φ ≫ ψ)
Tactic: rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
⊢ IsCocartesian.map p f φ φ = 𝟙 b
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsCocartesian (p.map φ) φ], IsCocartesian.map p (p.map φ) φ φ = 𝟙 b
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
⊢ IsCocartesian.map p (p.map φ) φ φ = 𝟙 b_1
have symm : 𝟙 b_1 = IsCocartesian.map p (p.map φ) φ φ
Tactic: 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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
⊢ 𝟙 b_1 = IsCocartesian.map p (p.map φ) φ φ
have hψ : φ ≫ 𝟙 b_1 = φ
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.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ φ' ≫ IsCocartesian.map p f φ' φ = 𝟙 b
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCocartesian (p.map φ) φ] [inst_5 : p.IsCocartesian (p.map φ) φ'],
  IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = 𝟙 b
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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
inst_3 : p.IsCocartesian (p.map φ) φ'
⊢ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = 𝟙 b_1
have h : φ ≫ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = φ ≫ 𝟙 b_1
Tactic: apply IsCocartesian.ext p (p.map φ) φ
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ' φ ≫ IsCocartesian.map p f φ φ' = 𝟙 b'
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCocartesian (p.map φ') φ] [inst_5 : p.IsCocartesian (p.map φ') φ'],
  IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = 𝟙 b'
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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ') φ
inst_3 : p.IsCocartesian (p.map φ') φ'
⊢ IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = 𝟙 b'
have h : φ' ≫ IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = φ' ≫ 𝟙 b'
Tactic: apply IsCocartesian.ext p (p.map φ') φ'
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
⊢ ∃! χ : b' ⟶ c, p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ
have h : (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) (φ'.inv ≫ IsCocartesian.map p f φ ψ) ∧
  ∀ (y : b' ⟶ c),
    (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ
Tactic: use φ'.inv ≫ IsCocartesian.map p f φ ψ
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
⊢ (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) (φ'.inv ≫ IsCocartesian.map p f φ ψ) ∧
    ∀ (y : b' ⟶ c),
      (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ
have h : ∀ (y : b' ⟶ c),
  (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ
Tactic: refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
⊢ τ = φ'.inv ≫ IsCocartesian.map p f φ ψ
have h : φ'.hom ≫ τ = IsCocartesian.map p f φ ψ
Tactic: rw [Iso.eq_inv_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₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
⊢ φ'.hom ≫ τ = IsCocartesian.map p f φ ψ
have h : φ ≫ φ'.hom ≫ τ = ψ
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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
⊢ ∃! χ : b ⟶ c, p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ
have h : (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) (IsCocartesian.map p f φ (φ'.inv ≫ ψ)) ∧
  ∀ (y : b ⟶ c),
    (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
Tactic: use IsCocartesian.map p f φ (φ'.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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
⊢ (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) (IsCocartesian.map p f φ (φ'.inv ≫ ψ)) ∧
    ∀ (y : b ⟶ c),
      (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
have h : ∀ (y : b ⟶ c),
  (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
Tactic: refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- 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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
τ : b ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ'.hom ≫ φ) ≫ τ = ψ
⊢ τ = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
have h : φ ≫ τ = φ'.inv ≫ ψ
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.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst_3 : p.IsHomLift f' φ'
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'
have subst_hom_lift : ∀ {R S_1 : 𝒮} {a_1 b_1 : 𝒳} (f : p.obj a ⟶ S) [p.IsStronglyCocartesian f φ] (g : S ⟶ p.obj b') (hf' : p.map φ' = f ≫ g)
  [p.IsHomLift (p.map φ') φ'], ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'
Tactic: subst_hom_lift p f' φ'
Cleared hypotheses: R, f, inst_2, S', g, f', hf', inst_3
-- 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₁} 𝒳 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst_2 : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst_3 : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'
have this : p.IsHomLift (f ≫ g) φ'
Tactic: have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift g ψ
inst_4 : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'
have rw : map p f φ (S' := S') (g := g) sorry (φ ≫ ψ) = ψ'
Tactic: rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift g ψ
inst_4 : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
rw : map p f φ (S' := S') (g := g) ⋯ (φ ≫ ψ) = ψ'
⊢ ψ = ψ'
have rw₁ : map p f φ (S' := S') (g := g) sorry (φ ≫ ψ) = map p f φ (S' := S') (g := g) sorry (φ ≫ ψ)
Tactic: rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 b
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsStronglyCocartesian (p.map φ) φ], map p (p.map φ) φ sorry φ = 𝟙 b
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 b_1
have symm : 𝟙 b_1 = map p (p.map φ) φ sorry φ
Tactic: 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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
⊢ 𝟙 b_1 = map p (p.map φ) φ ⋯ φ
have hψ : φ ≫ 𝟙 b_1 = φ
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.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst_3 : p.IsStronglyCocartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
⊢ f'' = f ≫ g ≫ g'
have rwa : f'' = (f ≫ g) ≫ g'
Tactic: rwa [← assoc, ← 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst_3 : p.IsStronglyCocartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
⊢ map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ (S' := S'') (g := g ≫ g') (f' := f'') ⋯ φ''
have hψ : φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''
Tactic: apply map_uniq p f φ
-- 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', p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ
have h₁ : (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) sorry (map p f φ sorry τ)) ∧
  ∀ (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: use map p g ψ (f' := g ≫ h) rfl <| map p f φ (assoc f g h) τ