-- Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
/-- In a category which admits strongly cartesian pullbacks, any cartesian morphism is
strongly cartesian. This is a helper-lemma for the fact that admitting strongly cartesian pullbacks
implies being fibered. -/
lemma isStronglyCartesian_of_exists_isCartesian (p : 𝒳 ⥤ 𝒮) (h : ∀ (a : 𝒳) (R : 𝒮)
    (f : R ⟶ p.obj a), ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) {R S : 𝒮} (f : R ⟶ S)
      {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ] : p.IsStronglyCartesian f φ

Proof state:
case universal_property'.map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ)

Result:
case universal_property'.map.intro.intro
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ p.IsStronglyCartesian f φ

Tactic:
constructor

Result:
case universal_property'
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [inst : p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case universal_property'
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
φ' : c ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f φ

Result:
case universal_property'.map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
c : 𝒳
φ' : c ⟶ b✝
R S : 𝒮
a b : 𝒳
g : p.obj c ⟶ p.obj a✝
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case universal_property'.map.intro.intro
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
let τ' := IsStronglyCartesian.map p (p.map φ) ψ (f':= g ≫ p.map φ) rfl φ'

Result:
case universal_property'.map.intro.intro
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : 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 φ) ψ ⋯ φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : 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 φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π ≫ Φ.inv = τ'

Tactic:
apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'

Result:
case h.refine_2.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : 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 φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ (π ≫ Φ.inv) ≫ ψ = φ'

Proof state:
case universal_property'.map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
c : 𝒳
φ' : c ⟶ b✝
R S : 𝒮
a b : 𝒳
g : p.obj c ⟶ p.obj a✝
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
clear a b R S

Result:
case universal_property'.map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : 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 φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ' ≫ Φ.hom

Tactic:
rw [← Iso.comp_inv_eq]

Result:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : 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 φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π ≫ Φ.inv = τ'