awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
h : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ IsIso α
have out : ∃ (inv : G ⟶ F), α ≫ inv = 𝟙 F ∧ inv ≫ α = 𝟙 G
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
h : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ ∃ (inv : G ⟶ F), α ≫ inv = 𝟙 F ∧ inv ≫ α = 𝟙 G
have h : (α ≫
      let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
      { toNatTrans := __NatTrans, isHomLift' := sorry }) =
    𝟙 F ∧
  (let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
      { toNatTrans := __NatTrans, isHomLift' := sorry }) ≫
      α =
    𝟙 G
Tactic: use {
      toNatTrans := inv ((forgetful 𝒳 𝒴).map α)
      isHomLift' := fun a ↦ by simp [lift_id_inv_isIso] }
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
inst_1 : IsIso α
⊢ IsIso (C := Functor.{v₂, v₃, u₂, u₃} 𝒳.obj 𝒴.obj) (X := F.toFunctor) (Y := G.toFunctor) α.toNatTrans
have rw : IsIso ((forgetful 𝒳 𝒴).map α)
Tactic: rw [← forgetful_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (hypothesis)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)
have this : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom
Tactic: have : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom := (Iso.app_hom α a) ▸ isHomLift' a
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.BasedCategory (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
this : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)
have rw : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).inv
Tactic: rw [← Iso.app_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.IsCartesian f φ
a' : 𝒳
ψ ψ' : a' ⟶ a
inst_3 : p.IsHomLift (𝟙 R) ψ
inst_4 : p.IsHomLift (𝟙 R) ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'
have rw : IsCartesian.map p f φ (ψ ≫ φ) = ψ'
Tactic: rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]
-- 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.IsCartesian f φ
a' : 𝒳
ψ ψ' : a' ⟶ a
inst_3 : p.IsHomLift (𝟙 R) ψ
inst_4 : p.IsHomLift (𝟙 R) ψ'
h : ψ ≫ φ = ψ' ≫ φ
rw : IsCartesian.map p f φ (ψ ≫ φ) = ψ'
⊢ ψ = ψ'
have rw₁ : IsCartesian.map p f φ (ψ ≫ φ) = IsCartesian.map p f φ (ψ ≫ φ)
Tactic: rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]
-- 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.IsCartesian f φ
⊢ IsCartesian.map p f φ φ = 𝟙 a
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsCartesian (p.map φ) φ], IsCartesian.map p (p.map φ) φ φ = 𝟙 a
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCartesian (p.map φ) φ
⊢ IsCartesian.map p (p.map φ) φ φ = 𝟙 a_1
have symm : 𝟙 a_1 = IsCartesian.map p (p.map φ) φ φ
Tactic: symm
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCartesian (p.map φ) φ
⊢ 𝟙 a_1 = IsCartesian.map p (p.map φ) φ φ
have hψ : 𝟙 a_1 ≫ φ = φ
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.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
⊢ ∃! χ : c ⟶ a, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ
have h : (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) (IsCartesian.map p f φ (ψ ≫ φ'.inv)) ∧
  ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) y → y = IsCartesian.map p f φ (ψ ≫ φ'.inv)
Tactic: use IsCartesian.map p f φ (ψ ≫ φ'.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.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) (IsCartesian.map p f φ (ψ ≫ φ'.inv)) ∧
    ∀ (y : c ⟶ a),
      (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) y → y = IsCartesian.map p f φ (ψ ≫ φ'.inv)
have h : ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) y → y = IsCartesian.map p f φ (ψ ≫ φ'.inv)
Tactic: refine ⟨⟨inferInstance, by simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]⟩, ?_⟩
-- 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.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ τ = IsCartesian.map p f φ (ψ ≫ φ'.inv)
have h : τ ≫ φ = ψ ≫ φ'.inv
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.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ τ ≫ φ = ψ ≫ φ'.inv
have h : (τ ≫ φ) ≫ φ'.hom = ψ
Tactic: rw [Iso.eq_comp_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.IsCartesian f φ
a' : 𝒳
φ' : a' ⟶ b
inst_3 : p.IsCartesian f φ'
⊢ IsCartesian.map p f φ φ' ≫ IsCartesian.map p f φ' φ = 𝟙 a'
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCartesian (p.map φ') φ] [inst_5 : p.IsCartesian (p.map φ') φ'],
  IsCartesian.map p (p.map φ') φ φ' ≫ IsCartesian.map p (p.map φ') φ' φ = 𝟙 a'
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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
a' : 𝒳
φ' : a' ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCartesian (p.map φ') φ
inst_3 : p.IsCartesian (p.map φ') φ'
⊢ IsCartesian.map p (p.map φ') φ φ' ≫ IsCartesian.map p (p.map φ') φ' φ = 𝟙 a'
have h : (IsCartesian.map p (p.map φ') φ φ' ≫ IsCartesian.map p (p.map φ') φ' φ) ≫ φ' = 𝟙 a' ≫ φ'
Tactic: apply IsCartesian.ext p (p.map φ') φ'
-- 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.IsCartesian f φ
a' : 𝒳
φ' : a' ⟶ b
inst_3 : p.IsCartesian f φ'
⊢ IsCartesian.map p f φ' φ ≫ IsCartesian.map p f φ φ' = 𝟙 a
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCartesian (p.map φ) φ] [inst_5 : p.IsCartesian (p.map φ) φ'],
  IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ' = 𝟙 a
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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
a' : 𝒳
φ' : a' ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCartesian (p.map φ) φ
inst_3 : p.IsCartesian (p.map φ) φ'
⊢ IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ' = 𝟙 a_1
have h : (IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ') ≫ φ = 𝟙 a_1 ≫ φ
Tactic: apply IsCartesian.ext p (p.map φ) φ
-- 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.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
⊢ ∃! χ : c ⟶ a', p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ
have h : (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) (IsCartesian.map p f φ ψ ≫ φ'.inv) ∧
  ∀ (y : c ⟶ a'), (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) y → y = IsCartesian.map p f φ ψ ≫ φ'.inv
Tactic: use IsCartesian.map p f φ ψ ≫ φ'.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.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
⊢ (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) (IsCartesian.map p f φ ψ ≫ φ'.inv) ∧
    ∀ (y : c ⟶ a'),
      (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) y → y = IsCartesian.map p f φ ψ ≫ φ'.inv
have h : ∀ (y : c ⟶ a'), (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) y → y = IsCartesian.map p f φ ψ ≫ φ'.inv
Tactic: refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- 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.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ = IsCartesian.map p f φ ψ ≫ φ'.inv
have h : τ ≫ φ'.hom = IsCartesian.map p f φ ψ
Tactic: rw [Iso.eq_comp_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.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ ≫ φ'.hom = IsCartesian.map p f φ ψ
have h : (τ ≫ φ'.hom) ≫ φ = ψ
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.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
f' : R' ⟶ S
hf' : f' = g ≫ f
φ' : a' ⟶ b
inst_3 : p.IsHomLift f' φ'
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have subst_hom_lift : ∀ {R_1 S : 𝒮} {a_1 b_1 : 𝒳} (g : p.obj a' ⟶ R) (f : R ⟶ p.obj b) [p.IsStronglyCartesian f φ] (hf' : p.map φ' = g ≫ f)
  [p.IsHomLift (p.map φ') φ'], ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Tactic: subst_hom_lift p f' φ'
Cleared hypotheses: S, f, inst_2, R', g, f', hf', inst_3
-- 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 : 𝒮
a b : 𝒳
φ : a ⟶ b
a' : 𝒳
φ' : a' ⟶ b
g : p.obj a' ⟶ R
f : R ⟶ p.obj b
inst_2 : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst_3 : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
have this : p.IsHomLift (g ≫ f) φ'
Tactic: have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
ψ ψ' : a' ⟶ a
inst_3 : p.IsHomLift g ψ
inst_4 : p.IsHomLift g ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'
have rw : map p f φ (R' := R') (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.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 φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
ψ ψ' : a' ⟶ a
inst_3 : p.IsHomLift g ψ
inst_4 : p.IsHomLift g ψ'
h : ψ ≫ φ = ψ' ≫ φ
rw : map p f φ (R' := R') (g := g) ⋯ (ψ ≫ φ) = ψ'
⊢ ψ = ψ'
have rw₁ : map p f φ (R' := R') (g := g) sorry (ψ ≫ φ) = map p f φ (R' := R') (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.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 φ
⊢ map p f φ ⋯ φ = 𝟙 a
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsStronglyCartesian (p.map φ) φ], map p (p.map φ) φ sorry φ = 𝟙 a
Tactic: subst_hom_lift p f φ
Cleared hypotheses: R, S, f, inst_2
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 a_1
have symm : 𝟙 a_1 = map p (p.map φ) φ sorry φ
Tactic: symm
-- 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCartesian (p.map φ) φ
⊢ 𝟙 a_1 = map p (p.map φ) φ ⋯ φ
have hψ : 𝟙 a_1 ≫ φ = φ
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.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst_3 : p.IsStronglyCartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
⊢ f'' = (g' ≫ g) ≫ f
have rwa : f'' = g' ≫ g ≫ f
Tactic: rwa [assoc, ← 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst_3 : p.IsStronglyCartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
⊢ map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ (R' := R'') (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.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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ ∃! χ : a' ⟶ a, p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ
have h₁ : (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) (map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ sorry τ)) ∧
  ∀ (y : a' ⟶ a),
    (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ sorry τ)
Tactic: use map p f φ (f' := h ≫ f) rfl (map p g ψ (assoc h f g).symm τ)
-- 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)
have h₁ : map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
h₁ : map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)
have h₂ : ∀ (y : a' ⟶ a),
  (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ
have h₁ : (map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ sorry τ) ≫ φ) ≫ ψ = τ
Tactic: rw [← assoc, fac, fac]
-- 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
h₁ : (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ) ≫ ψ = τ
⊢ map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ
have h₂ : map p g ψ sorry τ ≫ ψ = τ
Tactic: rw [← assoc, fac, fac]
-- 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
h₁ : (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ) ≫ ψ = τ
h₂ : map p g ψ ⋯ τ ≫ ψ = τ
⊢ map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ
have h₃ : τ = τ
Tactic: rw [← assoc, fac, fac]
-- 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) π' → π' = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)
have h₁ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : π' ≫ φ ≫ ψ = τ), π' = map p f φ (R' := p.obj a') (g := h) sorry (map p g ψ 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 f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
⊢ π' = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)
have h₁ : π' ≫ φ = map p g ψ sorry τ
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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
⊢ π' ≫ φ = map p g ψ ⋯ τ
have h₁ : (π' ≫ φ) ≫ ψ = τ
Tactic: apply map_uniq
-- 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 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) τ
⊢ ∃! χ : a' ⟶ a, p.IsHomLift h χ ∧ χ ≫ φ = τ
have h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
Tactic: have h₁ : IsHomLift p (h ≫ f ≫ g) (τ ≫ ψ) := by simpa using IsHomLift.comp p (h ≫ f) _ τ ψ