case mp
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
constructor
no goals
case mp
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
exact split_imp_of_iso φ p p' hpp'
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
apply split_imp_of_iso φ.symm p' p
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
rw [← comp_id p, ← φ.hom_inv_id]
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
slice_rhs 2 3 => rw [hpp']
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = (𝟙 X' ≫ p') ≫ φ.inv
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
slice_rhs 1 2 => erw [φ.inv_hom_id]
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = p' ≫ φ.inv
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = (𝟙 X' ≫ p') ≫ φ.inv
simp only [id_comp]
no goals
case mpr
C : Type u_2
inst✝ : Category C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = p' ≫ φ.inv
rfl