awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual 𝕜 F
⊢ extendRCLike
      ((fun (f : Dual 𝕜 F) ↦
          (reLm ∘ₗ
              (↑ℝ :
                  {S : Type u_1} →
                    {M : Type u_2} →
                      {M₂ : Type u_1} →
                        [inst : Semiring ℝ] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module ℝ M] →
                                  [inst_9 : Module ℝ M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f :
            F →ₗ[ℝ] ℝ))
        f) =
    f
have h : ∀ (x : F),
  Eq.{u_1 + 1} (α := 𝕜)
    ((extendRCLike
            ((fun (f : Dual 𝕜 F) ↦
                (reLm ∘ₗ
                    (↑ℝ :
                        {S : Type u_1} →
                          {M : Type u_2} →
                            {M₂ : Type u_1} →
                              [inst : Semiring ℝ] →
                                [inst_5 : Semiring S] →
                                  [inst_6 : AddCommMonoid M] →
                                    [inst_7 : AddCommMonoid M₂] →
                                      [inst_8 : Module ℝ M] →
                                        [inst_9 : Module ℝ M₂] →
                                          [inst_10 : Module S M] →
                                            [inst_11 : Module S M₂] →
                                              [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                      f :
                  F →ₗ[ℝ] ℝ))
              f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual 𝕜 F
x : F
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((extendRCLike
            ((fun (f : Dual 𝕜 F) ↦
                (reLm ∘ₗ
                    (↑ℝ :
                        {S : Type u_1} →
                          {M : Type u_2} →
                            {M₂ : Type u_1} →
                              [inst : Semiring ℝ] →
                                [inst_5 : Semiring S] →
                                  [inst_6 : AddCommMonoid M] →
                                    [inst_7 : AddCommMonoid M₂] →
                                      [inst_8 : Module ℝ M] →
                                        [inst_9 : Module ℝ M₂] →
                                          [inst_10 : Module S M] →
                                            [inst_11 : Module S M₂] →
                                              [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                      f :
                  F →ₗ[ℝ] ℝ))
              f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)
have h : Eq (α := ℝ)
  ((re : (a : 𝕜) → ℝ)
      ((extendRCLike
              ((fun (f : Dual 𝕜 F) ↦
                  (reLm ∘ₗ
                      (↑ℝ :
                          {S : Type u_1} →
                            {M : Type u_2} →
                              {M₂ : Type u_1} →
                                [inst : Semiring ℝ] →
                                  [inst_5 : Semiring S] →
                                    [inst_6 : AddCommMonoid M] →
                                      [inst_7 : AddCommMonoid M₂] →
                                        [inst_8 : Module ℝ M] →
                                          [inst_9 : Module ℝ M₂] →
                                            [inst_10 : Module S M] →
                                              [inst_11 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                        f :
                    F →ₗ[ℝ] ℝ))
                f) :
            (a : F) → 𝕜)
          x :
        𝕜) :
    ℝ)
  ((re : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
g : StrongDual ℝ F
x : F
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)
    (-(g : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ)
have inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0),
  Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)
    (-(g : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ)
Tactic: obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
g : StrongDual ℝ F
x : F
inl :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0),
    Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)
      (-(g : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)
    (-(g : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ)
have inr : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)
    (-(g : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ)
Tactic: obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
x y : StrongDual ℝ F
⊢ (x + y).extendRCLike = HAdd.hAdd (α := StrongDual 𝕜 F) x.extendRCLike y.extendRCLike
have h : ∀ (x_1 : F),
  Eq.{u_1 + 1} (α := 𝕜) (((x + y).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HAdd.hAdd (α := StrongDual 𝕜 F) x.extendRCLike y.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
x y : StrongDual ℝ F
x_1 : F
⊢ Eq.{u_1 + 1} (α := 𝕜) (((x + y).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HAdd.hAdd (α := StrongDual 𝕜 F) x.extendRCLike y.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
have h : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((x : (a : F) → ℝ) x_1 : ℝ) : 𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((y : (a : F) → ℝ) x_1 : ℝ) : 𝕜) -
    I *
      HAdd.hAdd (α := 𝕜) (β := 𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((x : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1) : ℝ) : 𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((y : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1) : ℝ) : 𝕜) =
  (↑((x : (a : F) → ℝ) x_1) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((x : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1)) : 𝕜) +
    ((↑((y : (a : F) → ℝ) x_1) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((y : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x_1)) : 𝕜))
Tactic: simp [extendRCLike_apply]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
⊢ (m • x).extendRCLike = HSMul.hSMul (α := ℝ) (β := StrongDual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike
have h : ∀ (x_1 : F),
  Eq.{u_1 + 1} (α := 𝕜) (((m • x).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HSMul.hSMul (α := ℝ) (β := StrongDual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike : (a : F) → 𝕜)
        x_1 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (((m • x).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HSMul.hSMul (α := ℝ) (β := StrongDual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike : (a : F) → 𝕜)
        x_1 :
      𝕜)
have h : 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: simp [extendRCLike_apply, real_smul_eq_coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
⊢ (fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f.extendRCLike = f
have h : ∀ (x : F),
  Eq (α := ℝ)
    (((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f.extendRCLike :
          (a : F) → ℝ)
        x :
      ℝ)
    ((f : (a : F) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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
⊢ extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) = f
have 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 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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.{u_1 + 1} (α := 𝕜)
    ((extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)
have 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 : 𝕜) : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
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 : 𝕜) : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((extendRCLike ((fun (f : StrongDual 𝕜 F) ↦ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f : F →L[ℝ] ℝ)) f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)
have 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 : 𝕜) : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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 = HSub.hSub (α := 𝕜) (wInner (E := E) w f₁ g) (wInner (E := E) w f₂ g)
have simp_rw : wInner (E := E) w (f₁ + -f₂) g = HAdd.hAdd (α := 𝕜) (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]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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)
⊢ wInner (E := E) w (f₁ - f₂) g = HSub.hSub (α := 𝕜) (wInner (E := E) w f₁ g) (wInner (E := E) w f₂ g)
have 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)
Tactic: simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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₂) = HSub.hSub (α := 𝕜) (wInner (E := E) w f g₁) (wInner (E := E) w f g₂)
have simp_rw : wInner (E := E) w f (g₁ + -g₂) = HAdd.hAdd (α := 𝕜) (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]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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₂)
⊢ wInner (E := E) w f (g₁ - g₂) = HSub.hSub (α := 𝕜) (wInner (E := E) w f g₁) (wInner (E := E) w f g₂)
have 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₂)
Tactic: simp_rw [sub_eq_add_neg, wInner_add_right, wInner_neg_right]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)
have simp_rw : ∑ i : ι, w i • ⟪(c • f) i, g i⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)
have simp_rw₁ : ∑ x : ι, w x • ⟪c • f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)
have 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⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)
have simp_rw₃ : ∑ x : ι, w x • star c • ⟪f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) (star c) (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w (c • f) g = HSMul.hSMul (β := 𝕜) (star c) (wInner (E := E) w f g)
have simp_rw₄ : Eq.{u_3 + 1} (α := 𝕜) (∑ x : ι, w x • star c • ⟪f x, g x⟫_𝕜) (∑ x : ι, star c • w x • ⟪f x, g x⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
    smul_comm (w _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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
⊢ wInner (E := E) w f (c • g) = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
have simp_rw : ∑ i : ι, w i • ⟪f i, (c • g) i⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w f (c • g) = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
have simp_rw₁ : ∑ x : ι, w x • ⟪f x, c • g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
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⟫_𝕜)
⊢ wInner (E := E) w f (c • g) = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
have simp_rw₂ : ∑ x : ι, w x • c • ⟪f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]