-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem PartialHomeomorph.contDiffOn_univUnitBall_symm :
    ContDiffOn ℝ n univUnitBall.symm (ball (0 : E) 1) := fun y hy ↦ by
  apply ContDiffAt.contDiffWithinAt
  suffices ContDiffAt ℝ n (fun y : E => (√(1 - ‖y‖ ^ 2 : ℝ))⁻¹) y from this.smul contDiffAt_id
  have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (↑univUnitBall.symm) y

Tactic:
suffices ContDiffAt ℝ n (fun y : E => (√(1 - ‖y‖ ^ 2 : ℝ))⁻¹) y from this.smul contDiffAt_id

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y

Tactic:
refine ContDiffAt.inv ?_ (Real.sqrt_ne_zero'.mpr h)

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => √(1 - ‖y‖ ^ 2)) y

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => 1 - ‖y‖ ^ 2) y

Tactic:
exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt

Result:
no goals

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y

Tactic:
have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
  rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) ((fun y => √y) ∘ fun y => 1 - ‖y‖ ^ 2) y

Tactic:
refine (contDiffAt_sqrt h.ne').comp y ?_

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => 1 - ‖y‖ ^ 2) y

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2

Tactic:
rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy

Result:
no goals

Proof state:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y => √(1 - ‖y‖ ^ 2)) y

Tactic:
change ContDiffAt ℝ n ((fun y ↦ √(y)) ∘ fun y ↦ (1 - ‖y‖ ^ 2)) y

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) ((fun y => √y) ∘ fun y => 1 - ‖y‖ ^ 2) y

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffWithinAt ℝ (↑n) (↑univUnitBall.symm) (ball 0 1) y

Tactic:
apply ContDiffAt.contDiffWithinAt

Result:
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (↑univUnitBall.symm) y