Theorem: RiemannSphere.extChartAt_inf (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
⊢ extChartAt I ∞ = invEquiv.toPartialEquiv.trans coePartialEquiv.symm
Tactic:
apply PartialEquiv.ext
State after:
case h

⊢ ∀ (x : 𝕊), ↑(extChartAt I ∞) x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) x

case hsymm

⊢ ∀ (x : ℂ), ↑(extChartAt I ∞).symm x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm x

case hs

⊢ (extChartAt I ∞).source = (invEquiv.toPartialEquiv.trans coePartialEquiv.symm).source

State before:
case h

⊢ ∀ (x : 𝕊), ↑(extChartAt I ∞) x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) x
Tactic:
intro z
State after:
case h
z : 𝕊
⊢ ↑(extChartAt I ∞) z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) z

State before:
case h
z : 𝕊
⊢ ↑(extChartAt I ∞) z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) z
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialEquiv.coe_trans_symm, PartialHomeomorph.coe_coe_symm,
  Homeomorph.toPartialHomeomorph_symm_apply, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm,
  PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply]
State after:
no goals

State before:
case hsymm

⊢ ∀ (x : ℂ), ↑(extChartAt I ∞).symm x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm x
Tactic:
intro z
State after:
case hsymm
z : ℂ
⊢ ↑(extChartAt I ∞).symm z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm z

State before:
case hsymm
z : ℂ
⊢ ↑(extChartAt I ∞).symm z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm z
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  invEquiv, PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialEquiv.symm_symm, PartialEquiv.coe_trans,
  PartialHomeomorph.coe_coe, Homeomorph.toPartialHomeomorph_apply, Homeomorph.homeomorph_mk_coe,
  Equiv.coe_fn_mk, PartialEquiv.coe_trans_symm, Equiv.toPartialEquiv_symm_apply,
  Equiv.coe_fn_symm_mk]
State after:
no goals

State before:
case hs

⊢ (extChartAt I ∞).source = (invEquiv.toPartialEquiv.trans coePartialEquiv.symm).source
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl,
  PartialEquiv.symm_source, PartialEquiv.trans_target, Homeomorph.toPartialHomeomorph_target,
  PartialHomeomorph.coe_coe_symm, Homeomorph.toPartialHomeomorph_symm_apply,
  Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm, PartialEquiv.trans_source,
  Equiv.toPartialEquiv_source, Equiv.toPartialEquiv_apply]
State after:
no goals