awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x + y) : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
rw₁ :
  z * HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
⊢ z * star (x + y) = z * star x + z * star y
have rw₂ : HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) =
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
Tactic: rw [star_def, map_add, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
⊢ y * star (z • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (y * star x)
have rw : HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z • x) : 𝕜) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rw [star_def, smul_eq_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z • x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ y * star (z • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (y * star x)
have rw₁ : HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z * x) : 𝕜) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rw [star_def, smul_eq_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z • x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z * x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ y * star (z • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (y * star x)
have rw₂ : y * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rw [star_def, smul_eq_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z • x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z * x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₂ :
  y * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ y * star (z • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (y * star x)
have rw₃ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rw [star_def, smul_eq_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ⟪r • x, y⟫_ℝ = HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪x, y⟫_ℝ
have this₁ : r • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x
Tactic: have : r • x = (r : 𝕜) • x := rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
⊢ (re : (a : 𝕜) → ℝ) (z * star (x + y)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) (z * star x) : ℝ) ((re : (a : 𝕜) → ℝ) (z * star y) : ℝ)
have simp : HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ)
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ)) -
    HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ)
      (HAdd.hAdd (α := ℝ) (β := ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ)) =
  HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) +
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ))
Tactic: simp only [star_def, map_add, mul_re, conj_re, conj_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
r : ℝ
⊢ (re : (a : 𝕜) → ℝ) (y * star (r • x)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ((re : (a : 𝕜) → ℝ) (y * star x) : ℝ)
have simp : HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) (HMul.hMul (β := ℝ) r ((re : (a : 𝕜) → ℝ) x : ℝ)) -
    HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-HMul.hMul (β := ℝ) r ((im : (a : 𝕜) → ℝ) x : ℝ)) =
  r *
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ))
Tactic: simp only [star_def, mul_re, conj_re, conj_im, conj_trivial, smul_re, smul_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
x y : ℝ
⊢ inner ℝ x y = x * y
have rw : inner ℝ x y = y * x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ (fderiv ℝ (fun (t : G) ↦ ⟪f t, g t⟫) x : (a : G) → 𝕜) y =
    ⟪f x, (fderiv ℝ g x : (a : G) → E) y⟫ + ⟪(fderiv ℝ f x : (a : G) → E) y, g x⟫
have rw : (fderivInnerCLM 𝕜 (f x, g x) ∘SL ContinuousLinearMap.prod (fderiv ℝ f x) (fderiv ℝ g x) : (a : G) → 𝕜) y =
  ⟪f x, (fderiv ℝ g x : (a : G) → E) y⟫ + ⟪(fderiv ℝ f x : (a : G) → E) y, g x⟫
Tactic: rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
n : WithTop ℕ∞
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
have h : ∀ (x : E),
  HPow.hPow (β := ℕ) ‖x‖ 2 =
    Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑reCLM : (a : 𝕜) → ℝ) (fun (x : E) ↦ ⟪id x, id x⟫) x
Tactic: convert! (reCLM : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
have this : HPow.hPow (β := ℕ) ‖id x‖ 2 ≠ 0
Tactic: have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : G) ↦ Dist.dist (f y) (g y)) x
have simp : ContDiffAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y - g y‖) x
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ Dist.dist (f y) (g y)) s x
have simp : ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y - g y‖) s x
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x
have simp : HasStrictFDerivAt (fun (x : F) ↦ (re : (a : ℝ) → ℝ) ⟪x, x⟫)
  (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x
Tactic: simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun (x : F) ↦ (re : (a : ℝ) → ℝ) ⟪x, x⟫)
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x
have h : instAddCommGroup = Ring.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) =
      fderivInnerCLM ℝ (id x, id x) ∘SL
        ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)
Tactic: convert! (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) =
    fderivInnerCLM ℝ (id x, id x) ∘SL ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)
have h : ∀ (y : F),
  Eq (α := ℝ)
    ((HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ)
    ((fderivInnerCLM ℝ (id x, id x) ∘SL
            ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F) :
          (a : F) → ℝ)
        y :
      ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
⊢ (fderiv ℝ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) =
    HSMul.hSMul (α := ℕ) (β := (a : F) → F →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : F) → F →L[ℝ] ℝ)
have h : ∀ (x : F),
  fderiv ℝ (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) x =
    HSMul.hSMul (α := ℕ) (β := (a : F) → F →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : F) → F →L[ℝ] ℝ) x
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ Dist.dist (f y) (g y)) x
have simp : DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) x
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ Dist.dist (f y) (g y)) s x
have simp : DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) s x
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContDiff.{0, u_1, u_1} ℝ (E := E) (↑n : WithTop ℕ∞) (↑univUnitBall : E → E)
have suffices : ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
Tactic: suffices ContDiff ℝ n fun x : E => (√(1 + ‖x‖ ^ 2 : ℝ))⁻¹ from this.smul contDiff_id
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (hypothesis)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
have h : ∀ (x : E), 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
have refine : ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: refine ContDiff.inv ?_ fun x => Real.sqrt_ne_zero'.mpr (h x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) (ball 0 1) y
have h : ContDiffAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) y
Tactic: apply ContDiffAt.contDiffWithinAt
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ ContDiffAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) y
have h : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹) y
Tactic: suffices ContDiffAt ℝ n (fun y : E => (√(1 - ‖y‖ ^ 2 : ℝ))⁻¹) y from this.smul contDiffAt_id
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa₁ : ∀ (hy : ‖y‖ < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₁ : ∀ (hy : ‖y‖ < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa₂ : ∀ (hy : |‖y‖| < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₁ : ∀ (hy : ‖y‖ < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₂ : ∀ (hy : |‖y‖| < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa₃ : ∀ (hy : HPow.hPow (β := ℕ) ‖y‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 1 2), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₁ : ∀ (hy : ‖y‖ < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₂ : ∀ (hy : |‖y‖| < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₃ : ∀ (hy : HPow.hPow (β := ℕ) ‖y‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 1 2), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa₄ : ∀ (hy : HPow.hPow (β := ℕ) ‖y‖ 2 < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
rwa : ∀ (hy : ‖y‖ < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₁ : ∀ (hy : ‖y‖ < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₂ : ∀ (hy : |‖y‖| < |1|), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₃ : ∀ (hy : HPow.hPow (β := ℕ) ‖y‖ 2 < HPow.hPow (α := ℝ) (β := ℕ) 1 2), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
rwa₄ : ∀ (hy : HPow.hPow (β := ℕ) ‖y‖ 2 < 1), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have rwa₅ : ∀ (hy : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2), 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (hypothesis)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹) y
have h : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
h : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹) y
have h₁ : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ √(1 - HPow.hPow (β := ℕ) ‖y‖ 2)) y
Tactic: refine ContDiffAt.inv ?_ (Real.sqrt_ne_zero'.mpr h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
h : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) ((fun (y : ℝ) ↦ √y) ∘ fun (y : E) ↦ 1 - HPow.hPow (β := ℕ) ‖y‖ 2) y
have h₁ : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ 1 - HPow.hPow (β := ℕ) ‖y‖ 2) y
Tactic: refine (contDiffAt_sqrt h.ne').comp y ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(univBall c r) : E → E)
have unfold : ContDiff.{0, u_1, u_1} ℝ (E := E) (F := E) (↑n : WithTop ℕ∞)
  (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry
      else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
    E → E)
Tactic: unfold univBall
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff.{0, u_1, u_1} ℝ (E := E) (F := E) (↑n : WithTop ℕ∞)
    (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
      E → E)
have pos : ∀ (h : 0 < r),
  ContDiff ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry) : E → E)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
pos :
  ∀ (h : 0 < r),
    ContDiff ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → E)
⊢ ContDiff.{0, u_1, u_1} ℝ (E := E) (F := E) (↑n : WithTop ℕ∞)
    (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
      E → E)
have neg : ∀ (h : ¬0 < r),
  ContDiff ℝ (↑n : WithTop ℕ∞)
    (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → E)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm (univBall c r)) : E → E) (ball c r)
have unfold : ContDiffOn ℝ (F := E) (↑n : WithTop ℕ∞)
  (↑(OpenPartialHomeomorph.symm
        (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
    E → E)
  (ball c r)
Tactic: unfold univBall
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ (F := E) (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm
          (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
          else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
      E → E)
    (ball c r)
have pos : ∀ (h : 0 < r),
  ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry)) : E → E)
    (ball c r)
Tactic: split_ifs with h