Theorem: measurable_symm_equiv_inverse (Ray/Hartogs/FubiniBall.lean)

State before:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (Complex.equivRealProd z) = z
Tactic:
simp only [Complex.equivRealProd_apply]
State after:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (z.re, z.im) = z

State before:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (z.re, z.im) = z
Tactic:
rw [Complex.measurableEquivRealProd, Homeomorph.toMeasurableEquiv_symm_coe]
State after:
z : ℂ
⊢ Complex.equivRealProdCLM.toHomeomorph.symm (z.re, z.im) = z

State before:
z : ℂ
⊢ Complex.equivRealProdCLM.toHomeomorph.symm (z.re, z.im) = z
Tactic:
simp only [ContinuousLinearEquiv.symm_toHomeomorph, ContinuousLinearEquiv.coe_toHomeomorph]
State after:
z : ℂ
⊢ Complex.equivRealProdCLM.symm (z.re, z.im) = z

State before:
z : ℂ
⊢ Complex.equivRealProdCLM.symm (z.re, z.im) = z
Tactic:
apply Complex.ext
State after:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).re = z.re

case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).im = z.im

State before:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).re = z.re
Tactic:
simp only [Complex.equivRealProdCLM_symm_apply_re]
State after:
no goals

State before:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).im = z.im
Tactic:
simp only [Complex.equivRealProdCLM_symm_apply_im]
State after:
no goals