awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
refine : ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ 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)

Premises used: Iff.mpr, ContDiff.inv, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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)

Tactic:
(contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'

Premises used: Real, contDiff_const, contDiff_norm_sq, LT.lt.ne', ContDiff.add, ContDiff.sqrt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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)

Tactic:
exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'

Premises used: Real, contDiff_const, contDiff_norm_sq, LT.lt.ne', ContDiff.add, ContDiff.sqrt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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 : ContDiffAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) y
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) (ball 0 1) y

Tactic:
apply ContDiffAt.contDiffWithinAt

Premises used: ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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 : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹) y
⊢ ContDiffAt ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm univUnitBall) : E → E) y

Tactic:
suffices ContDiffAt ℝ n (fun y : E => (√(1 - ‖y‖ ^ 2 : ℝ))⁻¹) y from this.smul contDiffAt_id
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (hy : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2), 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

Premises used: sub_pos, one_pow, sq_lt_sq, abs_norm, abs_one, mem_ball_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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

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
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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

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

Premises used: Iff.mpr, ContDiffAt.inv, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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
h₁ : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ √(1 - HPow.hPow (β := ℕ) ‖y‖ 2)) y
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹) y

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

Premises used: Iff.mpr, ContDiffAt.inv, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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

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

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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
h₁ : ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ 1 - HPow.hPow (β := ℕ) ‖y‖ 2) y
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) ((fun (y : ℝ) ↦ √y) ∘ fun (y : E) ↦ 1 - HPow.hPow (β := ℕ) ‖y‖ 2) y

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

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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

Tactic:
contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt

Premises used: Real, contDiff_norm_sq, contDiffAt_const, ContDiffAt.sub, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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

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

Premises used: Real, contDiff_norm_sq, contDiffAt_const, ContDiffAt.sub, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContDiff ℝ (F := E) (↑n : WithTop ℕ∞) fun (x : E) ↦ (↑((unitBall : (a : E) → (↑(ball 0 1) : Type u_1)) x) : E)

Tactic:
OpenPartialHomeomorph.contDiff_univUnitBall

Premises used: OpenPartialHomeomorph.contDiff_univUnitBall, OpenPartialHomeomorph.toFun'
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
hr : 0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(unitBallBall c r hr) : E → E)

Tactic:
(contDiff_id.const_smul r).add contDiff_const

Premises used: contDiff_id, contDiff_const, OpenPartialHomeomorph.toFun', ContDiff.add, ContDiff.const_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
hr : 0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm (unitBallBall c r hr)) : E → E)

Tactic:
(contDiff_id.sub contDiff_const).const_smul r⁻¹

Premises used: ContDiff.sub, contDiff_id, contDiff_const, OpenPartialHomeomorph.toFun', Inv.inv, ContDiff.const_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
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) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
      E → E)
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(univBall c r) : E → E)

Tactic:
unfold univBall

Premises used: OpenPartialHomeomorph.univBall
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
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)
neg :
  ∀ (h : ¬0 < r),
    ContDiff ℝ (↑n : WithTop ℕ∞)
      (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → E)

Tactic:
(contDiff_unitBallBall h).comp contDiff_univUnitBall

Premises used: OpenPartialHomeomorph.contDiff_univUnitBall, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.contDiff_unitBallBall, ContDiff.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → E)

Tactic:
exact (contDiff_unitBallBall h).comp contDiff_univUnitBall

Premises used: OpenPartialHomeomorph.contDiff_univUnitBall, OpenPartialHomeomorph.contDiff_unitBallBall, ContDiff.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞)
    (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → E)

Tactic:
contDiff_id.add contDiff_const

Premises used: contDiff_id, contDiff_const, OpenPartialHomeomorph.toFun', ContDiff.add
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ (↑n : WithTop ℕ∞)
    (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → E)

Tactic:
exact contDiff_id.add contDiff_const

Premises used: contDiff_id, contDiff_const, ContDiff.add
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
unfold :
  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)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (↑(OpenPartialHomeomorph.symm (univBall c r)) : E → E) (ball c r)

Tactic:
unfold univBall

Premises used: OpenPartialHomeomorph.univBall
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
pos :
  ∀ (h : 0 < r),
    ContDiffOn ℝ (↑n : WithTop ℕ∞)
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)) : E → E)
      (ball c r)
neg :
  ∀ (h : ¬0 < r),
    ContDiffOn ℝ (↑n : WithTop ℕ∞)
      (↑(OpenPartialHomeomorph.symm
            (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
        E → E)
      (ball c 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)) : E → E)
    (ball c r)

Tactic:
contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_

Premises used: OpenPartialHomeomorph.contDiff_unitBallBall_symm, ContDiff.contDiffOn, ContDiffOn.comp, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.contDiffOn_univUnitBall_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
pos : Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (ball c r) (ball 0 1)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)) : E → E)
    (ball c r)

Tactic:
refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_

Premises used: OpenPartialHomeomorph.contDiff_unitBallBall_symm, ContDiff.contDiffOn, ContDiffOn.comp, OpenPartialHomeomorph.contDiffOn_univUnitBall_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
pos :
  Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (toPartialEquiv (unitBallBall c r h)).target
    (toPartialEquiv (unitBallBall c r h)).source
⊢ Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (ball c r) (ball 0 1)

Tactic:
rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]

Premises used: OpenPartialHomeomorph.unitBallBall_target, OpenPartialHomeomorph.unitBallBall_source
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (toPartialEquiv (unitBallBall c r h)).target
    (toPartialEquiv (unitBallBall c r h)).source

Tactic:
apply OpenPartialHomeomorph.symm_mapsTo

Premises used: OpenPartialHomeomorph.symm_mapsTo
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm
          (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
      E → E)
    (ball c r)

Tactic:
contDiffOn_id.sub contDiffOn_const

Premises used: OpenPartialHomeomorph.toFun', ContDiffOn.sub, contDiffOn_const, contDiffOn_id
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm
          (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
      E → E)
    (ball c r)

Tactic:
exact contDiffOn_id.sub contDiffOn_const

Premises used: ContDiffOn.sub, contDiffOn_const, contDiffOn_id
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
e_f :
  ∀ (m : Fin (Module.finrank ℝ E)),
    Eq (α := E ⊗[ℝ] E)
      ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)
      (∑ n : Fin (Module.finrank ℝ E),
          HSMul.hSMul (β := E ⊗[ℝ] E)
            (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
              ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
            ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E) :
        E ⊗[ℝ] E)
⊢ Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))

Tactic:
congr 1 with m
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
e_f :
  (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m =
    HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E) (if m = m then 1 else 0)
      ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)
rw :
  ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E) =
        0
⊢ Eq (α := E ⊗[ℝ] E)
    ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)
    (∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E) :
      E ⊗[ℝ] E)

Tactic:
rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]

Premises used: OrthonormalBasis.orthonormal, Iff.mp, orthonormal_iff_ite, Fintype.sum_eq_single
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m =
    HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E) (if m = m then 1 else 0)
      ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)

Tactic:
simp only [↓reduceIte, one_smul]

Premises used: one_smul, reduceIte
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
simp :
  ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      m = x →
        Eq (α := E ⊗[ℝ] E)
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E)
          (0 : E ⊗[ℝ] E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E) =
        0

Tactic:
simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]

Premises used: one_smul, zero_smul, ite_eq_right_iff, OrthonormalBasis.orthonormal, Iff.mp, ite_smul, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      m = x →
        Eq (α := E ⊗[ℝ] E)
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E)
          (0 : E ⊗[ℝ] E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      m = x →
        Eq (α := E ⊗[ℝ] E)
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E)
          (0 : E ⊗[ℝ] E)

Tactic:
tauto
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner.{0, u_1} ℝ (E := E) ((v : (a : ι) → E) i : E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))

Tactic:
simp_rw [OrthonormalBasis.sum_inner_mul_inner v]

Premises used: OrthonormalBasis.sum_inner_mul_inner
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner.{0, u_1} ℝ (E := E) ((v : (a : ι) → E) i : E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))

Tactic:
simp only [real_inner_comm (w _)]

Premises used: DFunLike.coe, real_inner_comm