awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
m : ℝ
x : StrongDual ℝ F
x_1 : F
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) m : 𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((x : (a : F) → ℝ) x_1 : ℝ) : 𝕜) -
      I *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) m : 𝕜)
          ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((x : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1) : ℝ) : 𝕜) =
    (↑m : 𝕜) *
      ((↑((x : (a : F) → ℝ) x_1) : 𝕜) -
        HMul.hMul (α := 𝕜) I (↑((x : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1)) : 𝕜))

Tactic:
ring
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual ℝ F
h :
  ∀ (x : F),
    Eq (α := ℝ)
      (((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f.extendRCLike :
            (a : F) → ℝ)
          x :
        ℝ)
      ((f : (a : F) → ℝ) x : ℝ)
⊢ (fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f.extendRCLike = f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual ℝ F
x : F
⊢ Eq (α := ℝ)
    (((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f.extendRCLike :
          (a : F) → ℝ)
        x :
      ℝ)
    ((f : (a : F) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
h :
  ∀ (x : F),
    Eq.{u_1 + 1} (α := 𝕜)
      ((extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
            (a : F) → 𝕜)
          x :
        𝕜)
      ((f : (a : F) → 𝕜) x : 𝕜)
⊢ extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) = f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
x : F
h :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ((extendRCLike
                ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
              (a : F) → 𝕜)
            x :
          𝕜) :
      ℝ)
    ((re : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)
h₁ :
  Eq (α := ℝ)
    ((im : (a : 𝕜) → ℝ)
        ((extendRCLike
                ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
              (a : F) → 𝕜)
            x :
          𝕜) :
      ℝ)
    ((im : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)

Tactic:
apply RCLike.ext

Premises used: RCLike.ext
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
x : F
⊢ Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ((extendRCLike
                ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
              (a : F) → 𝕜)
            x :
          𝕜) :
      ℝ)
    ((re : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)

Tactic:
simp [extendRCLike_apply]

Premises used: StrongDual.extendRCLike_apply
-- Module: Mathlib.Analysis.RCLike.Extend
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : TopologicalSpace F
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : ContinuousConstSMul 𝕜 F
inst_5 : Module ℝ F
inst_6 : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
x : F
⊢ Eq (α := ℝ)
    ((im : (a : 𝕜) → ℝ)
        ((extendRCLike
                ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
              (a : F) → 𝕜)
            x :
          𝕜) :
      ℝ)
    ((im : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)

Tactic:
simp [extendRCLike_apply]

Premises used: StrongDual.extendRCLike_apply
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
f g : (i : ι) → E i
⊢ wInner (E := E) cWeight f g = HSMul.hSMul (α := ℚ≥0) (β := 𝕜) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (wInner (E := E) 1 f g)

Tactic:
simp [wInner, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

Premises used: Real, RCLike.wInner, NNRat.cast_smul_eq_nnqsmul, Finset.smul_sum
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (wInner (E := E) w f g) : 𝕜) (wInner (E := E) w g f : 𝕜)

Tactic:
simp [wInner, map_sum, inner_conj_symm, rclike_simps]

Premises used: RCLike.wInner, map_sum, inner_conj_symm
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) w 0 g) 0

Tactic:
simp [wInner]

Premises used: RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) w f 0) 0

Tactic:
simp [wInner]

Premises used: RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ wInner (E := E) w (f₁ + f₂) g = HAdd.hAdd (α := 𝕜) (wInner (E := E) w f₁ g) (wInner (E := E) w f₂ g)

Tactic:
simp [wInner, inner_add_left, smul_add, sum_add_distrib]

Premises used: RCLike.wInner, Finset.sum_add_distrib, inner_add_left, smul_add
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
⊢ wInner (E := E) w f (g₁ + g₂) = HAdd.hAdd (α := 𝕜) (wInner (E := E) w f g₁) (wInner (E := E) w f g₂)

Tactic:
simp [wInner, inner_add_right, smul_add, sum_add_distrib]

Premises used: RCLike.wInner, Finset.sum_add_distrib, inner_add_right, smul_add
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) w (-f) g) (-wInner (E := E) w f g)

Tactic:
simp [wInner]

Premises used: RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) w f (-g)) (-wInner (E := E) w f g)

Tactic:
simp [wInner]

Premises used: RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
simp_rw : wInner (E := E) w (f₁ + -f₂) g = HAdd.hAdd (α := 𝕜) (wInner (E := E) w f₁ g) (-wInner (E := E) w f₂ g)
simp_rw₁ :
  HAdd.hAdd (α := 𝕜) (wInner (E := E) w f₁ g) (wInner (E := E) w (-f₂) g) =
    HAdd.hAdd (α := 𝕜) (wInner (E := E) w f₁ g) (-wInner (E := E) w f₂ g)
⊢ wInner (E := E) w (f₁ - f₂) g = HSub.hSub (α := 𝕜) (wInner (E := E) w f₁ g) (wInner (E := E) w f₂ g)

Tactic:
simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]

Premises used: sub_eq_add_neg, RCLike.wInner_neg_left, RCLike.wInner_add_left
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
simp_rw : wInner (E := E) w f (g₁ + -g₂) = HAdd.hAdd (α := 𝕜) (wInner (E := E) w f g₁) (-wInner (E := E) w f g₂)
simp_rw₁ :
  HAdd.hAdd (α := 𝕜) (wInner (E := E) w f g₁) (wInner (E := E) w f (-g₂)) =
    HAdd.hAdd (α := 𝕜) (wInner (E := E) w f g₁) (-wInner (E := E) w f g₂)
⊢ wInner (E := E) w f (g₁ - g₂) = HSub.hSub (α := 𝕜) (wInner (E := E) w f g₁) (wInner (E := E) w f g₂)

Tactic:
simp_rw [sub_eq_add_neg, wInner_add_right, wInner_neg_right]

Premises used: sub_eq_add_neg, RCLike.wInner_neg_right, RCLike.wInner_add_right
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
inst_4 : IsEmpty ι
w : ι → ℝ
f g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) w f g) 0

Tactic:
simp [Subsingleton.elim f 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
𝕝 : Type u_5
inst_4 : CommSemiring 𝕝
inst_5 : StarRing 𝕝
inst_6 : Algebra 𝕝 𝕜
inst_7 : StarModule 𝕝 𝕜
inst_8 : SMulCommClass ℝ 𝕝 𝕜
inst_9 : (i : ι) → Module.{u_5, u_4} 𝕝 (E i)
inst_10 : ∀ (i : ι), IsScalarTower.{u_5, u_3, u_4} 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
simp_rw : ∑ i : ι, w i • ⟪(c • f) i, g i⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₁ : ∑ x : ι, w x • ⟪c • f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₂ :
  ∑ x : ι, w x • HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) c : 𝕝) ⟪f x, g x⟫_𝕜 =
    HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₃ : ∑ x : ι, w x • star c • ⟪f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₄ : Eq.{u_3 + 1} (α := 𝕜) (∑ x : ι, w x • star c • ⟪f x, g x⟫_𝕜) (∑ x : ι, star c • w x • ⟪f x, g x⟫_𝕜)
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)

Tactic:
simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]

Premises used: RCLike.wInner, inner_smul_left_eq_star_smul, starRingEnd_apply, Finset.smul_sum, SMulCommClass.smul_comm, Pi.smul_apply
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
𝕝 : Type u_5
inst_4 : CommSemiring 𝕝
inst_5 : StarRing 𝕝
inst_6 : Algebra 𝕝 𝕜
inst_7 : StarModule 𝕝 𝕜
inst_8 : (i : ι) → Module.{u_5, u_4} 𝕝 (E i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_5, u_3, u_4} 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
simp_rw : ∑ i : ι, w i • ⟪f i, (c • g) i⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₁ : ∑ x : ι, w x • ⟪f x, c • g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₂ : ∑ x : ι, w x • c • ⟪f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₃ : Eq.{u_3 + 1} (α := 𝕜) (∑ x : ι, w x • c • ⟪f x, g x⟫_𝕜) (∑ x : ι, c • w x • ⟪f x, g x⟫_𝕜)
⊢ wInner (E := E) w f (c • g) = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)

Tactic:
simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]

Premises used: RCLike.wInner, Finset.smul_sum, inner_smul_right_eq_smul, SMulCommClass.smul_comm, Pi.smul_apply
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
rw : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) (star (star c)) (wInner (E := E) w f g)
rw₁ : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
rw₂ rw₃ : c * wInner (E := E) w f g = c * wInner (E := E) w f g
⊢ c * wInner (E := E) w f g = wInner (E := E) w (star c • f) g

Tactic:
rw [wInner_smul_left, star_star, smul_eq_mul]

Premises used: star_star, RCLike.wInner_smul_left, smul_eq_mul
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
f g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) 1 f g) (∑ i : ι, ⟪f i, g i⟫_𝕜)

Tactic:
simp [wInner]

Premises used: RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
f g : (i : ι) → E i
⊢ Eq.{u_3 + 1} (α := 𝕜) (wInner (E := E) cWeight f g) (𝔼 i : ι, ⟪f i, g i⟫_𝕜)

Tactic:
simp [wInner, expect, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

Premises used: Real, RCLike.wInner, Finset.expect, NNRat.cast_smul_eq_nnqsmul, Finset.smul_sum
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
w : ι → ℝ
a : 𝕜
f : ι → 𝕜
⊢ wInner (E := fun (a : ι) ↦ 𝕜) w (const ι a) f =
    HMul.hMul (α := 𝕜) (β := 𝕜) (∑ i : ι, w i • f i : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)

Tactic:
simp [wInner, const_apply, sum_mul]

Premises used: Function.const_apply, RCLike.wInner, Finset.sum_mul
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
w : ι → ℝ
f : ι → 𝕜
a : 𝕜
⊢ wInner (E := fun (i : ι) ↦ 𝕜) w f (const ι a) =
    a * ∑ i : ι, HSMul.hSMul (β := 𝕜) (w i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f i) : 𝕜)

Tactic:
simp [wInner, const_apply, mul_sum]

Premises used: Function.const_apply, Finset.mul_sum, RCLike.wInner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
a : 𝕜
f : ι → 𝕜
⊢ wInner (E := fun (a : ι) ↦ 𝕜) 1 (const ι a) f =
    HMul.hMul (α := 𝕜) (β := 𝕜) (∑ i : ι, f i : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)

Tactic:
simp [wInner_one_eq_sum, sum_mul]

Premises used: RCLike.wInner_one_eq_sum, Finset.sum_mul
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : ι → 𝕜
a : 𝕜
⊢ wInner (E := fun (i : ι) ↦ 𝕜) 1 f (const ι a) = a * ∑ i : ι, (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f i)

Tactic:
simp [wInner_one_eq_sum, mul_sum]

Premises used: Finset.mul_sum, RCLike.wInner_one_eq_sum
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
a : 𝕜
f : ι → 𝕜
⊢ Eq (α := 𝕜) (wInner (E := fun (a : ι) ↦ 𝕜) cWeight (const ι a) f)
    (𝔼 i : ι, HMul.hMul (β := 𝕜) (f i) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜))

Tactic:
simp [wInner_cWeight_eq_expect]

Premises used: RCLike.wInner_cWeight_eq_expect
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : ι → 𝕜
a : 𝕜
⊢ wInner (E := fun (i : ι) ↦ 𝕜) cWeight f (const ι a) = a * 𝔼 i : ι, (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f i)

Tactic:
simp [wInner_cWeight_eq_expect, mul_expect]

Premises used: RCLike.wInner_cWeight_eq_expect, Finset.mul_expect
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f g : ι → 𝕜
⊢ wInner (E := fun (i : ι) ↦ 𝕜) 1 f g = inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 f) (toLp 2 g)

Tactic:
simp [PiLp.inner_apply, wInner]

Premises used: RCLike.wInner, PiLp.inner_apply
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f g : PiLp.{u_1, u_3} 2 fun (_i : ι) ↦ 𝕜
⊢ ⟪f, g⟫_𝕜 = wInner (E := fun (_i : ι) ↦ 𝕜) 1 f.ofLp g.ofLp

Tactic:
simp [PiLp.inner_apply, wInner]

Premises used: RCLike.wInner, PiLp.inner_apply
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) 1 (f k₁) (f k₂)) 0
⊢ Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0

Tactic:
simp_rw [wInner_one_eq_inner] at hinner

Premises used: RCLike.wInner_one_eq_inner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
refine_2 : ∀ (this : LinearIndependent 𝕜 (M := WithLp 2 (ι → 𝕜)) fun (i : κ) ↦ toLp 2 (f i)), LinearIndependent 𝕜 f
refine_1 : ∀ (i : κ), Ne (α := WithLp 2 (ι → 𝕜)) (toLp 2 (f i)) 0
⊢ LinearIndependent 𝕜 f

Tactic:
have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
this : LinearIndependent 𝕜 (M := WithLp 2 (ι → 𝕜)) fun (i : κ) ↦ toLp 2 (f i)
⊢ LinearIndependent 𝕜 f

Tactic:
(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm.toLinearMap.linearIndependent_iff_of_injOn
    (toLp_injective 2).injOn |>.1 this

Premises used: LinearEquiv.symm, Function.Injective.injOn, LinearEquiv.toLinearMap, WithLp.toLp_injective, Iff.mp, LinearMap.linearIndependent_iff_of_injOn, OfNat.ofNat, WithLp.linearEquiv
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
⊢ ∀ (i : κ), Ne (α := WithLp 2 (ι → 𝕜)) (toLp 2 (f i)) 0

Tactic:
fun i ↦ (toLp_eq_zero 2).ne.2 (hf i)

Premises used: Iff.mpr, Iff.ne, WithLp.toLp_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
this : LinearIndependent 𝕜 (M := WithLp 2 (ι → 𝕜)) fun (i : κ) ↦ toLp 2 (f i)
⊢ LinearIndependent 𝕜 f

Tactic:
exacts [(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm.toLinearMap.linearIndependent_iff_of_injOn
    (toLp_injective 2).injOn |>.1 this, fun i ↦ (toLp_eq_zero 2).ne.2 (hf i)]

Premises used: Iff.mpr, LinearEquiv.symm, Function.Injective.injOn, LinearEquiv.toLinearMap, Iff.ne, WithLp.toLp_injective, Iff.mp, LinearMap.linearIndependent_iff_of_injOn, WithLp.toLp_eq_zero, OfNat.ofNat, WithLp.linearEquiv
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
inl : IsEmpty ι → LinearIndependent 𝕜 f
inr : Nonempty ι → LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 f

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : IsEmpty ι
⊢ IsEmpty κ

Tactic:
have : IsEmpty κ := ⟨fun k ↦ hf k <| Subsingleton.elim ..⟩
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : IsEmpty ι
this : IsEmpty κ
⊢ LinearIndependent 𝕜 f

Tactic:
linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : IsEmpty ι
this : IsEmpty κ
⊢ LinearIndependent 𝕜 f

Tactic:
exact linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : Nonempty ι
⊢ Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) 1 (f k₁) (f k₂)) 0

Tactic:
simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

Premises used: NNRat.cast_smul_eq_nnqsmul, RCLike.wInner_cWeight_eq_smul_wInner_one
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : Nonempty ι
⊢ LinearIndependent 𝕜 f

Tactic:
exact linearIndependent_of_ne_zero_of_wInner_one_eq_zero hf <| by
      simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

Premises used: RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
w : ι → ℝ
f g : ι → 𝕜
hw : 0 ≤ w
hf : 0 ≤ f
hg : 0 ≤ g
⊢ LE.le (α := 𝕜) 0 (wInner (E := fun (i : ι) ↦ 𝕜) w f g)

Tactic:
sum_nonneg fun _ _ ↦ smul_nonneg (hw _) <| mul_nonneg (hg _) (star_nonneg_iff.2 (hf _))

Premises used: Iff.mpr, smul_nonneg, mul_nonneg, RCLike.wInner, Finset.sum_nonneg, star_nonneg_iff
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
w : ι → ℝ
f g : ι → 𝕜
hw : 0 ≤ w
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ ‖w i • ⟪f i, g i⟫_𝕜‖ = w i • inner ℝ (E := (fun (i : ι) ↦ ℝ) i) ((fun (i : ι) ↦ ‖f i‖) i) ((fun (i : ι) ↦ ‖g i‖) i)

Tactic:
simp [Algebra.smul_def, norm_mul, abs_of_nonneg (hw i)]

Premises used: norm_mul, abs_of_nonneg, Algebra.smul_def
-- Module: Mathlib.Analysis.RCLike.Inner
Goal:
ι : Type u_1
inst : Fintype ι
w f g : ι → ℝ
hw : 0 ≤ w
⊢ LE.le (α := ℝ) |wInner (E := fun (i : ι) ↦ ℝ) w f g| (wInner (E := fun (i : ι) ↦ ℝ) w |f| |g|)

Tactic:
simpa using norm_wInner_le (𝕜 := ℝ) hw

Premises used: RCLike.norm_wInner_le