awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.BoundedContinuous
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
h : (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) = g
⊢ 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

Tactic:
refine ⟨by rwa [h_comp_eq], ?_⟩
-- Module: Mathlib.Analysis.RCLike.BoundedContinuous
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
h :
  ∀ (a : E),
    Eq (α := ℝ)
      (((↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) : (a : E) → ℝ)
          a :
        ℝ)
      ((g : (a : E) → ℝ) a : ℝ)
⊢ (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) = g

Tactic:
ext a
-- Module: Mathlib.Analysis.RCLike.BoundedContinuous
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
a : E
⊢ Eq (α := ℝ)
    (((↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) : C(E, ℝ)) : (a : E) → ℝ)
        a :
      ℝ)
    ((g : (a : E) → ℝ) a : ℝ)

Tactic:
simp [hg_apply]
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := 𝕜) ((star (realToRCLike 𝕜 f) : (a : X) → 𝕜) a : 𝕜) ((realToRCLike 𝕜 f : (a : X) → 𝕜) a : 𝕜)
⊢ IsSelfAdjoint (R := C(X, 𝕜)) (realToRCLike 𝕜 f)

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
a : X
⊢ Eq.{u_2 + 1} (α := 𝕜) ((star (realToRCLike 𝕜 f) : (a : X) → 𝕜) a : 𝕜) ((realToRCLike 𝕜 f : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
h : ∀ (x : ℝ), x ∈ spectrum ℝ (A := C(X, 𝕜)) (realToRCLike 𝕜 f) ↔ x ∈ spectrum ℝ f
⊢ spectrum ℝ (A := C(X, 𝕜)) (realToRCLike 𝕜 f) = spectrum ℝ f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
x : ℝ
⊢ x ∈ spectrum ℝ (A := C(X, 𝕜)) (realToRCLike 𝕜 f) ↔ x ∈ spectrum ℝ f

Tactic:
simp [spectrum.mem_iff, isUnit_iff_forall_isUnit, RCLike.ext_iff (K := 𝕜), Algebra.smul_def]

Premises used: RCLike.ext_iff, ContinuousMap.isUnit_iff_forall_isUnit, spectrum.mem_iff, Algebra.smul_def
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
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)
h : ∀ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
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)
x : X
⊢ Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)

Tactic:
simpa using congr($hfg x)
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ ∀ {a b : C(X, ℝ)},
    LE.le (α := C(X, 𝕜)) (({ toFun := realToRCLike 𝕜, inj' := ⋯ } : (a : C(X, ℝ)) → C(X, 𝕜)) a : C(X, 𝕜))
        (({ toFun := realToRCLike 𝕜, inj' := ⋯ } : (a : C(X, ℝ)) → C(X, 𝕜)) b : C(X, 𝕜)) ↔
      a ≤ b

Tactic:
simp [le_def]

Premises used: ContinuousMap.le_def
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ Monotone (α := C(X, ℝ)) (β := C(X, 𝕜)) (realToRCLike 𝕜)

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.monotone

Premises used: OrderEmbedding.monotone, ContinuousMap.realToRCLike, ContinuousMap.realToRCLikeOrderEmbedding
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ StrictMono (α := C(X, ℝ)) (β := C(X, 𝕜)) (realToRCLike 𝕜)

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.strictMono

Premises used: OrderEmbedding.strictMono, ContinuousMap.realToRCLike, ContinuousMap.realToRCLikeOrderEmbedding
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ Function.Injective (α := C(X, ℝ)) (β := C(X, 𝕜)) (realToRCLike 𝕜)

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.injective

Premises used: RelEmbedding.injective, ContinuousMap.realToRCLike, ContinuousMap.realToRCLikeOrderEmbedding
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f g : C(X, ℝ)
⊢ Eq (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g) ↔ f = g

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.eq_iff_eq

Premises used: ContinuousMap.realToRCLike, ContinuousMap.realToRCLikeOrderEmbedding, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f g : C(X, ℝ)
⊢ LE.le (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g) ↔ f ≤ g

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.le_iff_le

Premises used: ContinuousMap.realToRCLikeOrderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f g : C(X, ℝ)
⊢ LT.lt (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g) ↔ f < g

Tactic:
realToRCLikeOrderEmbedding X 𝕜 |>.lt_iff_lt

Premises used: ContinuousMap.realToRCLikeOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
inst_2 : CompactSpace X
f g : C(X, ℝ)
⊢ dist (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g) = dist f g

Tactic:
simp [dist_eq_norm, norm_eq_iSup_norm, ← map_sub]

Premises used: dist_eq_norm, map_sub, ContinuousMap.norm_eq_iSup_norm
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ Continuous (X := C(X, ℝ)) (Y := C(X, 𝕜)) (realToRCLike 𝕜)

Tactic:
continuous_postcomp { toFun x := RCLike.ofReal x }

Premises used: ContinuousMap.continuous_postcomp, ContinuousMap.mk, ContinuousMap.comp, RCLike.ofReal, ContinuousMap.realToRCLike
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
⊢ Eq (α := C(X, 𝕜)) ((realToRCLikeStarAlgHom X 𝕜 : (a : C(X, ℝ)) → C(X, 𝕜)) f : C(X, 𝕜)) (realToRCLike 𝕜 f : C(X, 𝕜))

Tactic:
rfl

Premises used: ContinuousMap.comp, ContinuousMap.realToRCLike, rfl
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
⊢ Eq (α := C(X, 𝕜)) (realToRCLike 𝕜 (star f)) (star (realToRCLike 𝕜 f))

Tactic:
map_star (realToRCLikeStarAlgHom X 𝕜) f

Premises used: ContinuousMap.realToRCLikeStarAlgHom, ContinuousMap.comp, StarHomClass.map_star, ContinuousMap.realToRCLike
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f g : C(X, ℝ)
⊢ realToRCLike 𝕜 (f * g) = HMul.hMul (α := C(X, 𝕜)) (realToRCLike 𝕜 f) (realToRCLike 𝕜 g)

Tactic:
map_mul (realToRCLikeStarAlgHom X 𝕜) f g

Premises used: ContinuousMap.realToRCLikeStarAlgHom, ContinuousMap.comp, ContinuousMap.realToRCLike, map_mul
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
a b : C(X, 𝕜)
⊢ a ≤ b → a.rclikeToReal ≤ b.rclikeToReal

Tactic:
simp_all [le_def, RCLike.le_iff_re_im (K := 𝕜)]

Premises used: ContinuousMap.le_def, RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
⊢ Continuous (X := C(X, 𝕜)) rclikeToReal

Tactic:
continuous_postcomp { toFun x := RCLike.re x }

Premises used: ContinuousMap.continuous_postcomp, ContinuousMap.mk, ContinuousMap.comp, RCLike.re, DFunLike.coe, ContinuousMap.rclikeToReal
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
h : ∀ (a : X), Eq (α := ℝ) ((rclikeToReal (realToRCLike 𝕜 f) : (a : X) → ℝ) a : ℝ) ((f : (a : X) → ℝ) a : ℝ)
⊢ rclikeToReal (realToRCLike 𝕜 f) = f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, ℝ)
a : X
⊢ Eq (α := ℝ) ((rclikeToReal (realToRCLike 𝕜 f) : (a : X) → ℝ) a : ℝ) ((f : (a : X) → ℝ) a : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
h : ∀ (a : X), Eq.{u_2 + 1} (α := 𝕜) ((realToRCLike 𝕜 f.rclikeToReal : (a : X) → 𝕜) a : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
⊢ realToRCLike 𝕜 f.rclikeToReal = f

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
h : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((realToRCLike 𝕜 f.rclikeToReal : (a : X) → 𝕜) a : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp only [realToRCLike_apply, rclikeToReal_apply, ← RCLike.conj_eq_iff_re]

Premises used: RCLike.conj_eq_iff_re, ContinuousMap.realToRCLike_apply, ContinuousMap.rclikeToReal_apply
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
rw : ((star f : (a : X) → 𝕜) a : 𝕜)
| ((f : (a : X) → 𝕜) a : 𝕜)

Tactic:
rw [← hf.star_eq]

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a : X
h : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((star f : (a : X) → 𝕜) a : 𝕜)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)

Tactic:
conv_rhs => rw [← hf.star_eq]

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
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 : 𝕜) : 𝕜) ((star f : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.ContinuousMap
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : RCLike 𝕜
x : C(X, 𝕜)
h_1 : Membership.mem (γ := Set C(X, 𝕜)) (Set.range (realToRCLike 𝕜)) x
w : C(X, ℝ)
h : realToRCLike 𝕜 w = x
⊢ Membership.mem (γ := Set C(X, 𝕜)) {f : C(X, 𝕜) | IsSelfAdjoint f} x

Tactic:
simp [← h]
-- 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
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
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)) : 𝕜))
⊢ fc (x + y) = fc x + fc y

Tactic:
simp only [fc, smul_add, map_add, mul_add]

Premises used: map_add, mul_add, smul_add
-- 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
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
⊢ 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:
abel
-- 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
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
c : ℝ
x : F
⊢ (↑((fr : (a : F) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x)) : 𝕜) =
    HMul.hMul (α := 𝕜) (↑c : 𝕜) (↑((fr : (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
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) : 𝕜)
c : ℝ
x : F
⊢ fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑c : 𝕜) x) = (↑c : 𝕜) * fc x

Tactic:
simp only [fc, A, smul_comm I, mul_comm I, mul_sub, mul_assoc]

Premises used: mul_sub, mul_assoc, RCLike.I, mul_comm, SMulCommClass.smul_comm
-- 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
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
inr : ∀ (h : HMul.hMul (α := 𝕜) I I = -1), 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

Tactic:
obtain (h | h) := @I_mul_I_ax 𝕜 _

Premises used: RCLike.I_mul_I_ax
-- 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
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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x

Tactic:
simp [fc, h]
-- 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
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
h : HMul.hMul (α := 𝕜) I I = -1
⊢ fc (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) = I * fc x

Tactic:
simp [fc, mul_sub, ← mul_assoc, smul_smul, h, add_comm]

Premises used: mul_sub, mul_assoc, smul_smul, add_comm
-- 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
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
rw :
  fc (((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • x) =
    ((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • fc x
⊢ fc (c • x) = c • fc x

Tactic:
rw [← re_add_im c]

Premises used: RCLike.re_add_im
-- 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
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 (((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • x) =
    ((↑((re : (a : 𝕜) → ℝ) c) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) c) : 𝕜) I) • fc x

Tactic:
simp only [add_smul, ← smul_smul, add, smul_ℝ, smul_I, ← mul_assoc, smul_eq_mul, add_mul]

Premises used: add_mul, mul_assoc, smul_smul, add_smul, smul_eq_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
fr : Dual ℝ 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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
x : F
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ) ((fr : (a : F) → ℝ) x : ℝ)

Tactic:
simp only [extendRCLike_apply, map_sub, zero_mul, mul_zero, sub_zero, rclike_simps]

Premises used: map_sub, sub_zero, MulZeroClass.zero_mul, Module.Dual.extendRCLike_apply, MulZeroClass.mul_zero
-- 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
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) : ℝ)
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 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
g : Dual ℝ 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: 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
g : Dual ℝ 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: Module.Dual.extendRCLike_apply