-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `φ` are strongly cocartesian, then so is `ψ`. -/
protected lemma of_comp [IsStronglyCocartesian p f φ] [IsStronglyCocartesian p (f ≫ g) (φ ≫ ψ)]
    [IsHomLift p g ψ] : IsStronglyCocartesian p g ψ where
  universal_property'

Proof state:
case h.refine_2.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ (φ ≫ ψ) ≫ π' = φ ≫ τ

Tactic:
simp [hπ'₂.symm]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ

Tactic:
use map p (f ≫ g) (φ ≫ ψ) (f' := f ≫ g ≫ h) (assoc f g h).symm (φ ≫ τ)

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Proof state:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ∀ (y : c ⟶ c'), (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
intro π' ⟨hπ'₁, hπ'₂⟩

Result:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Proof state:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ

Tactic:
apply IsStronglyCocartesian.ext p f φ (g ≫ h) <| by simp only [← assoc, fac]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)

Tactic:
simpa using IsHomLift.comp p f (g ≫ h) φ τ

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
⊢ ∀ {b' : 𝒳} (g_1 : T ⟶ p.obj b') (φ' : b ⟶ b') [inst : p.IsHomLift (g ≫ g_1) φ'], ∃! χ, p.IsHomLift g_1 χ ∧ ψ ≫ χ = φ'

Tactic:
intro c' h τ hτ

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ

Proof state:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
apply map_uniq

Result:
case h.refine_2.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ (φ ≫ ψ) ≫ π' = φ ≫ τ

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
refine ⟨⟨inferInstance, ?_⟩, ?_⟩

Result:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ

case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ∀ (y : c ⟶ c'), (fun χ => p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)