awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α β : F ⟶ G
h : α.toNatTrans = β.toNatTrans
⊢ α = β

Tactic:
BasedNatTrans.ext α β h

Premises used: CategoryTheory.BasedNatTrans.ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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 α)
out : ∃ (inv : G ⟶ F), α ≫ inv = 𝟙 F ∧ inv ≫ α = 𝟙 G
⊢ IsIso α

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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 α)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((inv ((forgetful 𝒳 𝒴).map α)).app a)

Tactic:
simp [lift_id_inv_isIso]

Premises used: CategoryTheory.IsHomLift.lift_id_inv_isIso
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
h_1 : IsIso ((forgetful 𝒳 𝒴).map α)
h :
  (α ≫
        let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
        { toNatTrans := __NatTrans, isHomLift' := ⋯ }) =
      𝟙 F ∧
    (let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
        { toNatTrans := __NatTrans, isHomLift' := ⋯ }) ≫
        α =
      𝟙 G
⊢ ∃ (inv : G ⟶ F), α ≫ inv = 𝟙 F ∧ inv ≫ α = 𝟙 G

Tactic:
use {
      toNatTrans := inv ((forgetful 𝒳 𝒴).map α)
      isHomLift' := fun a ↦ by simp [lift_id_inv_isIso] }
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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 α)
⊢ (α ≫
        let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
        { toNatTrans := __NatTrans, isHomLift' := ⋯ }) =
      𝟙 F ∧
    (let __NatTrans := inv ((forgetful 𝒳 𝒴).map α);
        { toNatTrans := __NatTrans, isHomLift' := ⋯ }) ≫
        α =
      𝟙 G

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
inst_1 : IsIso α
rw : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ IsIso (C := Functor.{v₂, v₃, u₂, u₃} 𝒳.obj 𝒴.obj) (X := F.toFunctor) (Y := G.toFunctor) α.toNatTrans

Tactic:
rw [← forgetful_map]

Premises used: CategoryTheory.BasedNatTrans.forgetful_map
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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 ((forgetful 𝒳 𝒴).map α)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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)) (α.app a).hom

Tactic:
have : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom := (Iso.app_hom α a) ▸ isHomLift' a
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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
rw : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).inv
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)

Tactic:
rw [← Iso.app_inv]

Premises used: CategoryTheory.Iso.app_inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
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)) (α.app a).inv

Tactic:
apply IsHomLift.lift_id_inv

Premises used: CategoryTheory.IsHomLift.lift_id_inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
inst_1 : IsIso (C := Functor.{v₂, v₃, u₂, u₃} 𝒳.obj 𝒴.obj) (X := F.toFunctor) (Y := G.toFunctor) α.toNatTrans
⊢ IsIso ((forgetful 𝒳 𝒴).map α)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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.IsHomLift f φ'
⊢ p.IsHomLift (𝟙 R) (IsCartesian.map p f φ φ')

Tactic:
(Classical.choose_spec <| IsCartesian.universal_property (p := p) (f := f) (φ := φ) φ').1.1

Premises used: CategoryTheory.Functor.IsCartesian.map, CategoryTheory.Functor.IsCartesian.universal_property, Classical.choose_spec, And.left
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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.IsHomLift f φ'
⊢ IsCartesian.map p f φ φ' ≫ φ = φ'

Tactic:
(Classical.choose_spec <| IsCartesian.universal_property (p := p) (f := f) (φ := φ) φ').1.2

Premises used: CategoryTheory.Functor.IsCartesian.map, CategoryTheory.Functor.IsCartesian.universal_property, Classical.choose_spec, And.right, And.left
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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.IsHomLift f φ'
ψ : a' ⟶ a
inst_4 : p.IsHomLift (𝟙 R) ψ
hψ : ψ ≫ φ = φ'
⊢ ψ = IsCartesian.map p f φ φ'

Tactic:
(Classical.choose_spec <| IsCartesian.universal_property (p := p) (f := f) (φ := φ) φ').2
    ψ ⟨inferInstance, hψ⟩

Premises used: CategoryTheory.Functor.IsCartesian.map, inferInstance, CategoryTheory.Functor.IsCartesian.universal_property, Classical.choose_spec, And.right, And.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ (ψ ≫ φ) = ψ'
rw₁ rw₂ : IsCartesian.map p f φ (ψ ≫ φ) = IsCartesian.map p f φ (ψ ≫ φ)
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]

Premises used: CategoryTheory.Functor.IsCartesian.map_uniq, CategoryTheory.CategoryStruct.comp, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsCartesian (p.map φ) φ], IsCartesian.map p (p.map φ) φ φ = 𝟙 a
⊢ IsCartesian.map p f φ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ) φ
symm : 𝟙 a_1 = IsCartesian.map p (p.map φ) φ φ
⊢ IsCartesian.map p (p.map φ) φ φ = 𝟙 a_1

Tactic:
symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ) φ
hψ : 𝟙 a_1 ≫ φ = φ
⊢ 𝟙 a_1 = IsCartesian.map p (p.map φ) φ φ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ≫ φ = φ

Tactic:
simp only [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
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)
⊢ ∃! χ : c ⟶ a, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ

Tactic:
use IsCartesian.map p f φ (ψ ≫ φ'.inv)

Premises used: CategoryTheory.Functor.IsCartesian.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
⊢ IsCartesian.map p f φ (ψ ≫ φ'.inv) ≫ φ ≫ φ'.hom = ψ

Tactic:
simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.IsCartesian.fac_assoc
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
h :
  ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ ≫ φ'.hom = ψ) y → y = IsCartesian.map p f φ (ψ ≫ φ'.inv)
⊢ (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:
refine ⟨⟨inferInstance, by simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 = ψ
h : τ ≫ φ = ψ ≫ φ'.inv
⊢ τ = IsCartesian.map p f φ (ψ ≫ φ'.inv)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 = ψ
h : (τ ≫ φ) ≫ φ'.hom = ψ
⊢ τ ≫ φ = ψ ≫ φ'.inv

Tactic:
rw [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 = ψ
⊢ (τ ≫ φ) ≫ φ'.hom = ψ

Tactic:
simp only [assoc, hτ₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ'
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'
⊢ IsCartesian.map p f φ φ' ≫ IsCartesian.map p f φ' φ = 𝟙 a'

Tactic:
subst_hom_lift p f φ'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ') φ'
h : (IsCartesian.map p (p.map φ') φ φ' ≫ IsCartesian.map p (p.map φ') φ' φ) ≫ φ' = 𝟙 a' ≫ φ'
⊢ IsCartesian.map p (p.map φ') φ φ' ≫ IsCartesian.map p (p.map φ') φ' φ = 𝟙 a'

Tactic:
apply IsCartesian.ext p (p.map φ') φ'

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.IsCartesian.ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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' ≫ φ'

Tactic:
simp only [assoc, fac, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsCartesian.fac, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ'
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
⊢ IsCartesian.map p f φ' φ ≫ IsCartesian.map p f φ φ' = 𝟙 a

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ) φ'
h : (IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ') ≫ φ = 𝟙 a_1 ≫ φ
⊢ IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ' = 𝟙 a_1

Tactic:
apply IsCartesian.ext p (p.map φ) φ

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.IsCartesian.ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ≫ φ

Tactic:
simp only [assoc, fac, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsCartesian.fac, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ'
⊢ p.IsHomLift (𝟙 R) (domainUniqueUpToIso p f φ φ').hom

Tactic:
domainUniqueUpToIso_hom p f φ φ' ▸ IsCartesian.map_isHomLift p f φ φ'

Premises used: Eq.rec, CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom, CategoryTheory.Functor.IsCartesian.map_isHomLift, Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ'
⊢ p.IsHomLift (𝟙 R) (domainUniqueUpToIso p f φ φ').inv

Tactic:
domainUniqueUpToIso_inv p f φ φ' ▸ IsCartesian.map_isHomLift p f φ' φ

Premises used: Eq.rec, CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv, CategoryTheory.Functor.IsCartesian.map_isHomLift, Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
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
⊢ ∃! χ : c ⟶ a', p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ

Tactic:
use IsCartesian.map p f φ ψ ≫ φ'.inv

Premises used: CategoryTheory.Functor.IsCartesian.map, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
⊢ (IsCartesian.map p f φ ψ ≫ φ'.inv) ≫ φ'.hom ≫ φ = ψ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ψ
h :
  ∀ (y : c ⟶ a'), (fun (χ : c ⟶ a') ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) y → y = IsCartesian.map p f φ ψ ≫ φ'.inv
⊢ (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:
refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ≫ φ = ψ
h : τ ≫ φ'.hom = IsCartesian.map p f φ ψ
⊢ τ = IsCartesian.map p f φ ψ ≫ φ'.inv

Tactic:
rw [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 ≫ φ = ψ
h : (τ ≫ φ'.hom) ≫ φ = ψ
⊢ τ ≫ φ'.hom = IsCartesian.map p f φ ψ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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) ≫ φ = ψ

Tactic:
simp only [assoc, hτ₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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' φ'
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 χ ∧ χ ≫ φ = φ'
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f' φ'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ') φ'
⊢ p.IsHomLift (g ≫ f) φ'

Tactic:
have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ inferInstance)
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ') φ'
this : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
apply IsStronglyCartesian.universal_property' f

Premises used: CategoryTheory.Functor.IsStronglyCartesian.universal_property'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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 φ
a' : 𝒳
φ' : a' ⟶ b
inst_3 : p.IsHomLift f φ'
⊢ f = 𝟙 R ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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' φ'
⊢ p.IsHomLift g (map p f φ hf' φ')

Tactic:
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.1

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map, Classical.choose_spec, And.left, CategoryTheory.Functor.IsStronglyCartesian.universal_property
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
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' φ'
⊢ map p f φ hf' φ' ≫ φ = φ'

Tactic:
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.2

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map, Classical.choose_spec, And.right, And.left, CategoryTheory.Functor.IsStronglyCartesian.universal_property