awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.BoundedContinuous (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg :
  Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
hg_apply : ∀ (a : E), Eq.{u_1 + 1} (α := 𝕜) ((x : (a : E) → 𝕜) a : 𝕜) ((↑((g : (a : E) → ℝ) a) : 𝕜) : 𝕜)
h_comp_eq :
  (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
      (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) =
    x
⊢ Membership.mem (α := E →ᵇ 𝕜) A
      ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
          (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) :
        E →ᵇ 𝕜) ∧
    (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) = g
have h : (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) : C(E, ℝ)) = g
Tactic: refine ⟨by rwa [h_comp_eq], ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.BoundedContinuous (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg :
  Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
hg_apply : ∀ (a : E), Eq.{u_1 + 1} (α := 𝕜) ((x : (a : E) → 𝕜) a : 𝕜) ((↑((g : (a : E) → ℝ) a) : 𝕜) : 𝕜)
h_comp_eq :
  (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
      (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) =
    x
⊢ (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) = g
have h : ∀ (a : E),
  Eq (α := ℝ)
    (((↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) : C(E, ℝ)) : (a : E) → ℝ)
        a :
      ℝ)
    ((g : (a : E) → ℝ) a : ℝ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
⊢ IsSelfAdjoint (R := C(X, 𝕜)) (realToRCLike 𝕜 f)
have h : ∀ (a : X),
  Eq.{u_2 + 1} (α := 𝕜) ((star (realToRCLike 𝕜 f) : (a : X) → 𝕜) a : 𝕜) ((realToRCLike 𝕜 f : (a : X) → 𝕜) a : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
⊢ spectrum ℝ (A := C(X, 𝕜)) (realToRCLike 𝕜 f) = spectrum ℝ f
have h : ∀ (x : ℝ), x ∈ spectrum ℝ (A := C(X, 𝕜)) (realToRCLike 𝕜 f) ↔ x ∈ spectrum ℝ f
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f g : C(X, ℝ)
hfg : Eq (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g)
⊢ f = g
have h : ∀ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
⊢ rclikeToReal (realToRCLike 𝕜 f) = f
have h : ∀ (a : X), Eq (α := ℝ) ((rclikeToReal (realToRCLike 𝕜 f) : (a : X) → ℝ) a : ℝ) ((f : (a : X) → ℝ) a : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
⊢ realToRCLike 𝕜 f.rclikeToReal = f
have h : ∀ (a : X), Eq.{u_2 + 1} (α := 𝕜) ((realToRCLike 𝕜 f.rclikeToReal : (a : X) → 𝕜) a : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
⊢ Eq.{u_2 + 1} (α := 𝕜) ((realToRCLike 𝕜 f.rclikeToReal : (a : X) → 𝕜) a : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
have h : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
Tactic: simp only [realToRCLike_apply, rclikeToReal_apply, ← RCLike.conj_eq_iff_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
| ((f : (a : X) → 𝕜) a : 𝕜)
have rw : ((star f : (a : X) → 𝕜) a : 𝕜)
Tactic: rw [← hf.star_eq]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.ContinuousMap (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
have h : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((star f : (a : X) → 𝕜) a : 𝕜)
Tactic: conv_rhs => rw [← hf.star_eq]
-- 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
fr : Dual ℝ F
fc : F → 𝕜 :=
  fun (x : F) ↦
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)
x y : F
⊢ fc (x + y) = fc x + fc y
have simp : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((fr : (a : F) → ℝ) x : ℝ) : 𝕜)
      ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((fr : (a : F) → ℝ) y : ℝ) : 𝕜) -
    (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) : ℝ) : 𝕜) +
      HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
        ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y) : ℝ) : 𝕜)) =
  (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜) +
    ((↑((fr : (a : F) → ℝ) y) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)) : 𝕜))
Tactic: simp only [fc, smul_add, map_add, mul_add]
-- 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
fr : Dual ℝ F
fc : F → 𝕜 :=
  fun (x : F) ↦
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A :
  ∀ (c : ℝ) (x : F),
    (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x)) : 𝕜) =
      HMul.hMul (α := 𝕜) (↑c : 𝕜) (↑((fr : (a : F) → ℝ) x) : 𝕜)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x) = (↑c : 𝕜) * fc x
x : F
⊢ fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
have inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
Tactic: obtain (h | h) := @I_mul_I_ax 𝕜 _
-- 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
fr : Dual ℝ F
fc : F → 𝕜 :=
  fun (x : F) ↦
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A :
  ∀ (c : ℝ) (x : F),
    (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x)) : 𝕜) =
      HMul.hMul (α := 𝕜) (↑c : 𝕜) (↑((fr : (a : F) → ℝ) x) : 𝕜)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x) = (↑c : 𝕜) * fc x
x : F
inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
⊢ fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
have inr : ∀ (h : HMul.hMul (α := 𝕜) I I = -1), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
Tactic: obtain (h | h) := @I_mul_I_ax 𝕜 _
-- 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
fr : Dual ℝ F
fc : F → 𝕜 :=
  fun (x : F) ↦
    (↑((fr : (a : F) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜)
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A :
  ∀ (c : ℝ) (x : F),
    (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x)) : 𝕜) =
      HMul.hMul (α := 𝕜) (↑c : 𝕜) (↑((fr : (a : F) → ℝ) x) : 𝕜)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x) = (↑c : 𝕜) * fc x
smul_I : ∀ (x : F), fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x
c : 𝕜
x : F
⊢ fc (c • x) = c • fc x
have rw : fc (((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • x) =
  ((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • fc x
Tactic: rw [← re_add_im c]
-- 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
g : Dual ℝ 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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
g : Dual ℝ 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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
x : F
⊢ 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 : 𝕜))
have 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)
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]
-- 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
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)
⊢ 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 : 𝕜))
have 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) : 𝕜)
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]
-- 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
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) : 𝕜)
⊢ 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 : 𝕜))
have 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
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]
-- 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
fr : Dual ℝ F
x : F
⊢ 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) :
      ℝ)
have 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) :
    ℝ)
Tactic: rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]
-- 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
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) :
      ℝ)
⊢ 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) :
      ℝ)
have 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) :
    ℝ)
Tactic: rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]
-- 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
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) :
      ℝ)
⊢ 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) :
      ℝ)
have 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) :
    ℝ)
Tactic: rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]
-- 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
x y : Dual ℝ F
⊢ (x + y).extendRCLike = HAdd.hAdd (α := Dual 𝕜 F) x.extendRCLike y.extendRCLike
have 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 : 𝕜)
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
x y : Dual ℝ F
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 : 𝕜)
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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
m : ℝ
x : Dual ℝ F
⊢ (m • x).extendRCLike = HSMul.hSMul (α := ℝ) (β := Dual 𝕜 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 (α := ℝ) (β := Dual 𝕜 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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
m : ℝ
x : Dual ℝ F
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 : 𝕜)
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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual ℝ F
⊢ (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
have 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 : ℝ)
Tactic: ext