awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(closedBall 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2)
    (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(closedBall 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
inst_6 : NormedAlgebra 𝕜 𝕜'
⊢ SMulCommClass.{u_1, u_2, u_2} (↑(sphere 0 1) : Type u_1) (↑(ball 0 1) : Type u_2) (↑(ball 0 1) : Type u_2)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : SMulCommClass 𝕜 𝕜' E
⊢ SMulCommClass.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(sphere 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : (↑(sphere 0 r) : Type u_3)
this : IsAddTorsionFree E
h : x = -x
rw : (↑(-x) : E)
| (↑x : E)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : (↑(sphere 0 r) : Type u_3)
this : IsAddTorsionFree E
h : x = -x
conv_lhs : (↑(-x) : E) = -(↑x : E)
⊢ (↑x : E) = -(↑x : E)

Tactic:
conv_lhs => rw [h]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : (↑(sphere 0 r) : Type u_3)
this : IsAddTorsionFree E
h : x = -x
⊢ (↑(-x) : E) = -(↑x : E)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
x : (↑(sphere 0 1) : Type u_3)
⊢ x ≠ -x

Tactic:
ne_neg_of_mem_sphere 𝕜 one_ne_zero x

Premises used: one_ne_zero, ne_neg_of_mem_sphere
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
have : 0 < 1 + ‖x‖ ^ 2 := by positivity
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
this : 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
rw : HPow.hPow (β := ℕ) ‖x‖ 2 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ Membership.mem (γ := Set E) (ball 0 1) ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x)

Tactic:
rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
      div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq,
      abs_norm, Real.sq_sqrt this.le]

Premises used: Iff.mpr, norm_smul, abs_inv, LT.lt.le, Real.sq_sqrt, abs_pos, sq_lt_sq, div_lt_one, abs_norm, div_eq_inv_mul, Real.norm_eq_abs, Real.sqrt_ne_zero', mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
this : 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
lt_one_add _

Premises used: lt_one_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
this : 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
exact lt_one_add _

Premises used: lt_one_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
match_scalars :
  (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ *
      ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ * 1) =
    1
⊢ (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ • (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x =
    x

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
simp :
  (√(1 - HPow.hPow (β := ℕ) (|√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)|⁻¹ * ‖x‖) 2))⁻¹ * (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ = 1
⊢ (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ *
      ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ * 1) =
    1

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
field_simp :
  1 /
      √((HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2 - HPow.hPow (β := ℕ) ‖x‖ 2) /
          HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2) =
    √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ (√(1 - HPow.hPow (β := ℕ) (|√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)|⁻¹ * ‖x‖) 2))⁻¹ * (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ = 1

Tactic:
field_simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ 1 /
      √((HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2 - HPow.hPow (β := ℕ) ‖x‖ 2) /
          HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2) =
    √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
simp [sq_abs, Real.sq_sqrt (zero_lt_one_add_norm_sq x).le]

Premises used: LT.lt.le, Real.sq_sqrt, sq_abs, zero_lt_one_add_norm_sq
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
nlinarith :
  1 - HPow.hPow (β := ℕ) ‖y‖ 2 ≤ 0 → 1 - HPow.hPow (β := ℕ) ‖y‖ 2 - 0 + (‖y‖ - 1) + (0 - (0 - ‖y‖) * (‖y‖ - 1)) = 0
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]

Premises used: Iff.mp, norm_nonneg, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
match_scalars :
  (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ *
      ((√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ * 1) =
    1
⊢ (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ • (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y =
    y

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
simp :
  (√(1 + HPow.hPow (β := ℕ) (|√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)|⁻¹ * ‖y‖) 2))⁻¹ * (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ = 1
⊢ (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ *
      ((√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ * 1) =
    1

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
field_simp :
  1 =
    √((HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2 + HPow.hPow (β := ℕ) ‖y‖ 2) /
          HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2) *
      √(1 - HPow.hPow (β := ℕ) ‖y‖ 2)
⊢ (√(1 + HPow.hPow (β := ℕ) (|√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)|⁻¹ * ‖y‖) 2))⁻¹ * (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ = 1

Tactic:
field_simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 1 =
    √((HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2 + HPow.hPow (β := ℕ) ‖y‖ 2) /
          HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2) *
      √(1 - HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
simp [field, sq_abs, Real.sq_sqrt this.le]

Premises used: LT.lt.le, Real.sq_sqrt, sq_abs
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
funProp : ∀ (x : E), Membership.mem (γ := Set E) univ x → √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
funProp₁ : ∀ (x : ℝ), x ≠ 0
funProp₂ : ∀ (x : E), √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
suffices : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ

Tactic:
suffices Continuous fun (x : E) => (√(1 + ‖x‖ ^ 2))⁻¹ by fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Continuous (Y := ℝ) fun (x : E) ↦ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹

Tactic:
exact Continuous.inv₀ (by fun_prop) fun x => Real.sqrt_ne_zero'.mpr (by positivity)

Premises used: Iff.mpr, Continuous.inv₀, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rw : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0

Tactic:
rw [Real.sqrt_ne_zero']

Premises used: Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ ∀ (y : E), Membership.mem (γ := Set E) (ball 0 1) y → √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0

Tactic:
have : ∀ y ∈ ball (0 : E) 1, √(1 - ‖(y : E)‖ ^ 2) ≠ 0 := fun y hy ↦ by
      rw [Real.sqrt_ne_zero']
      nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : ∀ (y : E), Membership.mem (γ := Set E) (ball 0 1) y → √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0
⊢ ContinuousOn (Y := E) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y) (ball 0 1)

Tactic:
ContinuousOn.smul (ContinuousOn.inv₀
      (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this) continuousOn_id

Premises used: Continuous.continuousOn, ContinuousOn.sub, continuousOn_const, ContinuousOn.sqrt, ContinuousOn.smul, ContinuousOn.inv₀, continuousOn_id, continuous_norm, ContinuousOn.pow
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : ∀ (y : E), Membership.mem (γ := Set E) (ball 0 1) y → √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0
⊢ ContinuousOn (Y := E) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y) (ball 0 1)

Tactic:
exact ContinuousOn.smul (ContinuousOn.inv₀
      (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this) continuousOn_id

Premises used: Continuous.continuousOn, ContinuousOn.sub, continuousOn_const, ContinuousOn.sqrt, ContinuousOn.smul, ContinuousOn.inv₀, continuousOn_id, continuous_norm, ContinuousOn.pow
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Eq.{u_1 + 1} (α := E) ((↑univUnitBall : E → E) 0) 0

Tactic:
simp [OpenPartialHomeomorph.univUnitBall_apply]

Premises used: OpenPartialHomeomorph.univUnitBall_apply
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Eq.{u_1 + 1} (α := E) ((↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) 0) 0

Tactic:
simp [OpenPartialHomeomorph.univUnitBall_symm_apply]

Premises used: OpenPartialHomeomorph.univUnitBall_symm_apply
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Eq.{u_1 + 1} (α := E) (↑((unitBall : (a : E) → (↑(ball 0 1) : Type u_1)) 0) : E) 0

Tactic:
OpenPartialHomeomorph.univUnitBall_apply_zero

Premises used: OpenPartialHomeomorph.univUnitBall_apply_zero, OpenPartialHomeomorph.toFun'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
change :
  image.{u_1, u_2} (α := E) (Function.comp (β := E) (⇑(IsometryEquiv.vaddConst c) : (a : E) → P) fun (x : E) ↦ r • x)
      (ball 0 1) =
    ball c r
⊢ image.{u_1, u_2} (α := E)
      (⇑(Homeomorph.trans (Homeomorph.smulOfNeZero r ⋯) (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
        (a : E) → P)
      (ball 0 1) =
    ball c r

Tactic:
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r

Premises used: Metric.ball, IsometryEquiv.vaddConst, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
rw : ball ((IsometryEquiv.vaddConst c : (a : E) → P) 0) ‖r‖ = ball c r
⊢ image.{u_1, u_2} (α := E) (Function.comp (β := E) (⇑(IsometryEquiv.vaddConst c) : (a : E) → P) fun (x : E) ↦ r • x)
      (ball 0 1) =
    ball c r

Tactic:
rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]

Premises used: Set.image_smul, LT.lt.ne', smul_unitBall, Set.image_comp, IsometryEquiv.image_ball
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball ((IsometryEquiv.vaddConst c : (a : E) → P) 0) ‖r‖ = ball c r

Tactic:
simp [abs_of_pos hr]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (h : 0 < r), (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)).source = univ
neg :
  ¬0 < r →
    (toPartialEquiv
          (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).source =
      univ
⊢ Eq.{u_1 + 1} (α := Set E)
    (PartialEquiv.source.{u_1, u_2} (β := P)
      (toPartialEquiv
        (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    univ

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
h : 0 < r
⊢ (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)).source = univ

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
h : ¬0 < r
⊢ (toPartialEquiv
        (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).source =
    univ

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
rw : (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r hr) ⋯)).target = ball c r
⊢ (toPartialEquiv (univBall c r)).target = ball c r

Tactic:
rw [univBall, dif_pos hr]

Premises used: OpenPartialHomeomorph.univBall, dif_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r hr) ⋯)).target = ball c r

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (hr : 0 < r), ball c r ⊆ (toPartialEquiv (univBall c r)).target
neg : ∀ (hr : ¬0 < r), ball c r ⊆ (toPartialEquiv (univBall c r)).target
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target

Tactic:
by_cases hr : 0 < r
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
pos pos₁ : ball c r ⊆ ball c r
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target

Tactic:
rw [univBall_target c hr]

Premises used: OpenPartialHomeomorph.univBall_target
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
neg :
  ball c r ⊆
    (toPartialEquiv
        (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).target
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target

Tactic:
rw [univBall, dif_neg hr]

Premises used: OpenPartialHomeomorph.univBall, dif_neg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆
    (toPartialEquiv
        (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).target

Tactic:
subset_univ _

Premises used: Set.subset_univ, Set.univ, setOf
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆
    (toPartialEquiv
        (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).target

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (h : 0 < r), (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → P) 0 = c
neg :
  ¬0 < r →
    (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → P) 0 = c
⊢ (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
          else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
        E → P)
      0 =
    c

Tactic:
split_ifs