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

State before:
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
z : 𝕊
⊢ g (OnePoint.rec i f z) = OnePoint.rec (g i) (g ∘ f) z
Tactic:
induction z using OnePoint.rec
State after:
case h₁
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
⊢ g (OnePoint.rec i f ∞) = OnePoint.rec (g i) (g ∘ f) ∞

case h₂
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
x✝ : ℂ
⊢ g (OnePoint.rec i f ↑x✝) = OnePoint.rec (g i) (g ∘ f) ↑x✝

State before:
case h₁
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
⊢ g (OnePoint.rec i f ∞) = OnePoint.rec (g i) (g ∘ f) ∞
Tactic:
simp only [rec_inf]
State after:
no goals

State before:
case h₂
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
x✝ : ℂ
⊢ g (OnePoint.rec i f ↑x✝) = OnePoint.rec (g i) (g ∘ f) ↑x✝
Tactic:
simp only [rec_coe, Function.comp]
State after:
no goals