awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Extend
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
fr : Dual ℝ F
x : F
rw :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2 =
    (re : (a : 𝕜) → ℝ)
      (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) : 𝕜) 2)
rw₁ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2 =
    (re : (a : 𝕜) → ℝ) (↑(HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2) : 𝕜)
rw₂ rw₃ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) 2 =
    (re : (a : 𝕜) → ℝ)
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜)
        ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜))

Tactic:
rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.conj_mul, RCLike.ofReal_pow
-- Module: Mathlib.Analysis.RCLike.Extend
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
fr : Dual ℝ F
x : F
rw :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        (HSMul.hSMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜)
          ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) :
      ℝ)
    ((fr : (a : F) → ℝ)
        (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
      ℝ)
rw₁ :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ((fr.extendRCLike : (a : F) → 𝕜)
            (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
          𝕜) :
      ℝ)
    ((fr : (a : F) → ℝ)
        (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
      ℝ)
rw₂ rw₃ :
  Eq (α := ℝ)
    ((fr : (a : F) → ℝ)
        (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
      ℝ)
    ((fr : (a : F) → ℝ)
        (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
      ℝ)
⊢ Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜)
          ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜)) :
      ℝ)
    ((fr : (a : F) → ℝ)
        (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) :
      ℝ)

Tactic:
rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]

Premises used: Module.Dual.re_extendRCLike_apply, smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.RCLike.Extend
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
x y : Dual ℝ F
h :
  ∀ (x_1 : F),
    Eq.{u_1 + 1} (α := 𝕜) (((x + y).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
      ((HAdd.hAdd (α := Dual 𝕜 F) x.extendRCLike y.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
⊢ (x + y).extendRCLike = HAdd.hAdd (α := Dual 𝕜 F) x.extendRCLike y.extendRCLike

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
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
x y : Dual ℝ F
x_1 : F
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)) : 𝕜))
⊢ Eq.{u_1 + 1} (α := 𝕜) (((x + y).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HAdd.hAdd (α := Dual 𝕜 F) x.extendRCLike y.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)

Tactic:
simp [extendRCLike_apply]

Premises used: Module.Dual.extendRCLike_apply
-- Module: Mathlib.Analysis.RCLike.Extend
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
x y : Dual ℝ F
x_1 : F
⊢ 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:
ring
-- Module: Mathlib.Analysis.RCLike.Extend
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
m : ℝ
x : Dual ℝ F
h :
  ∀ (x_1 : F),
    Eq.{u_1 + 1} (α := 𝕜) (((m • x).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
      ((HSMul.hSMul (α := ℝ) (β := Dual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
⊢ (m • x).extendRCLike = HSMul.hSMul (α := ℝ) (β := Dual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
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
m : ℝ
x : Dual ℝ F
x_1 : F
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)) : 𝕜))
⊢ Eq.{u_1 + 1} (α := 𝕜) (((m • x).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HSMul.hSMul (α := ℝ) (β := Dual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)

Tactic:
simp [extendRCLike_apply, real_smul_eq_coe_mul]

Premises used: Module.Dual.extendRCLike_apply, RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Extend
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
m : ℝ
x : Dual ℝ 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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual ℝ F
h :
  ∀ (x : F),
    Eq (α := ℝ)
      (((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.extendRCLike :
            (a : F) → ℝ)
          x :
        ℝ)
      ((f : (a : F) → ℝ) x : ℝ)
⊢ (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.extendRCLike =
    f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
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 (α := ℝ)
    (((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.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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual 𝕜 F
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 : 𝕜)
⊢ 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

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Extend
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 (α := ℝ)
    ((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:
simp
-- Module: Mathlib.Analysis.RCLike.Extend
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 (α := ℝ)
    ((im : (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 :
          𝕜) :
      ℝ)
    ((im : (a : 𝕜) → ℝ) ((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
fr : StrongDual ℝ F
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : F) ↦
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)

Tactic:
fun_prop
-- 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
fr : StrongDual ℝ F
x : F
⊢ (fr.extendRCLike : (a : F) → 𝕜) x =
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)

Tactic:
rfl

Premises used: rfl
-- 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
g : StrongDual ℝ F
x : F
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((g.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ) ((g : (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
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) : ℝ)
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) : ℝ)
⊢ 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 := 𝕜)

Premises used: RCLike.I_eq_zero_or_im_I_eq_one
-- 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
g : StrongDual ℝ F
x : F
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:
simp [h, 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
g : StrongDual ℝ F
x : F
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:
simp [h, 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
x y : StrongDual ℝ F
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 : 𝕜)
⊢ (x + y).extendRCLike = HAdd.hAdd (α := StrongDual 𝕜 F) x.extendRCLike y.extendRCLike

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
x y : StrongDual ℝ F
x_1 : F
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)) : 𝕜))
⊢ Eq.{u_1 + 1} (α := 𝕜) (((x + y).extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)
    ((HAdd.hAdd (α := StrongDual 𝕜 F) x.extendRCLike y.extendRCLike : (a : F) → 𝕜) x_1 : 𝕜)

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
x y : StrongDual ℝ F
x_1 : F
⊢ 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:
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
m : ℝ
x : StrongDual ℝ F
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 :
        𝕜)
⊢ (m • x).extendRCLike = HSMul.hSMul (α := ℝ) (β := StrongDual 𝕜 F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.extendRCLike

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
m : ℝ
x : StrongDual ℝ F
x_1 : F
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)) : 𝕜))
⊢ 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:
simp [extendRCLike_apply, real_smul_eq_coe_mul]

Premises used: StrongDual.extendRCLike_apply, RCLike.real_smul_eq_coe_mul