-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- A strongly cocartesian arrow lying over an isomorphism is an isomorphism. -/
lemma isIso_of_base_isIso (φ : a ⟶ b) [IsStronglyCocartesian p f φ] [IsIso f] : IsIso φ

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ' ≫ φ = 𝟙 b

Tactic:
apply IsStronglyCocartesian.ext p (p.map φ) φ (𝟙 (p.obj b))

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ ≫ φ' ≫ φ = φ ≫ 𝟙 b

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : IsIso f
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)

Tactic:
apply IsHomLift.comp

Result:
no goals

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ' ≫ φ = 𝟙 b

Tactic:
have h₁ : IsHomLift p (𝟙 (p.obj b)) (φ' ≫ φ) := by
  rw [← IsIso.inv_hom_id (p.map φ)]
  apply IsHomLift.comp

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ' ≫ φ = 𝟙 b

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
refine ⟨inv_hom, ?_⟩

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ' ≫ φ = 𝟙 b

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ

Tactic:
clear a b R S

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ

Tactic:
let φ' := map p (p.map φ) φ (IsIso.hom_inv_id (p.map φ)).symm (𝟙 a)

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
⊢ IsIso φ

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
⊢ IsIso φ

Tactic:
use φ'

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ ≫ φ' ≫ φ = φ ≫ 𝟙 b

Tactic:
simp only [← assoc, inv_hom, comp_id, id_comp]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)

Tactic:
rw [← IsIso.inv_hom_id (p.map φ)]

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
have inv_hom : φ ≫ φ' = 𝟙 a := fac p (p.map φ) φ _ (𝟙 a)

Result:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b