awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
z w : 𝕜
⊢ z ≤ w ↔
    LE.le (α := ℝ)
        (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  re)
                  ⋯ :
                let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            z :
          ℝ)
        (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  re)
                  ⋯ :
                let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            w :
          ℝ) ∧
      Eq (α := ℝ)
        (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            z :
          ℝ)
        (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            w :
          ℝ)

Tactic:
h.le_iff_re_im

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ {z w : 𝕜},
    z ≤ w ↔
      LE.le (α := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) ∧
        Eq (α := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)

Tactic:
exact h.le_iff_re_im

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
hk : NormedField 𝕜
h : IsRCLikeNormedField 𝕜
choose : (p : RCLike 𝕜) → (hp : hk = DenselyNormedField.toNormedField) → RCLike 𝕜
⊢ RCLike 𝕜

Tactic:
choose p hp using h.out

Premises used: IsRCLikeNormedField.out
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
hk : NormedField 𝕜
h : IsRCLikeNormedField 𝕜
p : RCLike 𝕜
hp : hk = DenselyNormedField.toNormedField
⊢ RCLike 𝕜

Tactic:
exact p.copy_of_normedField hk hp

Premises used: RCLike.copy_of_normedField
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst_1 : RCLike 𝕜
inst_2 : SeminormedAddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : SeminormedAddCommGroup W
inst_5 : NormedSpace 𝕜 W
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] W
x : V
⊢ norm.{u_5} (E := W)
      ((HSMul.hSMul (α := 𝕜ˣ) ((Unitary.toUnits : (a : ↥(unitary 𝕜)) → 𝕜ˣ) α : 𝕜ˣ) e.toLinearEquiv : (a : V) → W) x :
        W) =
    ‖x‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
e : V ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
x : V
⊢ (α • e : (a : V) → W) x = HSMul.hSMul (β := W) (↑α : 𝕜) ((e : (a : V) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
e : V ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
x : W
⊢ ((α • e).symm : (a : W) → V) x = HSMul.hSMul (β := V) (↑α⁻¹ : 𝕜) ((e.symm : (a : W) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup W
inst_2 : NormedSpace 𝕜 W
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
h : ∀ (x : W), Eq.{u_6 + 1} (α := G) (((α • e).symm : (a : W) → G) x : G) ((α⁻¹ • e.symm : (a : W) → G) x : G)
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup W
inst_2 : NormedSpace 𝕜 W
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
x : W
⊢ Eq.{u_6 + 1} (α := G) (((α • e).symm : (a : W) → G) x : G) ((α⁻¹ • e.symm : (a : W) → G) x : G)

Tactic:
simp [symm_smul_apply]

Premises used: LinearIsometryEquiv.symm_smul_apply
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
e : V ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
⊢ (α • e).toLinearEquiv = HSMul.hSMul (α := 𝕜ˣ) ((Unitary.toUnits : (a : ↥(unitary 𝕜)) → 𝕜ˣ) α : 𝕜ˣ) e.toLinearEquiv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup W
inst_2 : NormedSpace 𝕜 W
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
⊢ (↑(α • e) : G ≃L[𝕜] W) = HSMul.hSMul (α := 𝕜ˣ) ((Unitary.toUnits : (a : ↥(unitary 𝕜)) → 𝕜ˣ) α : 𝕜ˣ) (↑e : G ≃L[𝕜] W)

Tactic:
rfl

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := W) (((α • e).trans f : (a : V) → W) x : W)
      ((HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f) : (a : V) → W) x : W)
⊢ (α • e).trans f = HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f)

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
x : V
⊢ Eq.{u_5 + 1} (α := W) (((α • e).trans f : (a : V) → W) x : W)
    ((HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f) : (a : V) → W) x : W)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := W) ((e.trans (α • f) : (a : V) → W) x : W)
      ((HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f) : (a : V) → W) x : W)
⊢ e.trans (α • f) = HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f)

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : SeminormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
x : V
⊢ Eq.{u_5 + 1} (α := W) ((e.trans (α • f) : (a : V) → W) x : W)
    ((HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f) : (a : V) → W) x : W)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.BoundedContinuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
h :
  ∀ (g : C(E, ℝ)),
    Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
        (Subalgebra.map (toContinuousMapₐ ℝ)
          (Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
            (Subalgebra.restrictScalars ℝ A.toSubalgebra)))
        g ↔
      Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
        (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
          (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))
        g
⊢ Subalgebra.map (toContinuousMapₐ ℝ)
      (Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
        (Subalgebra.restrictScalars ℝ A.toSubalgebra)) =
    Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A)))

Tactic:
ext g
-- 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, ℝ)
h :
  (∃ (x : E →ᵇ ℝ),
      Membership.mem (α := E →ᵇ 𝕜) A
          ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
        (↑x : C(E, ℝ)) = g) ↔
    ∃ x ∈ A,
      Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
        ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
⊢ Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
      (Subalgebra.map (toContinuousMapₐ ℝ)
        (Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
          (Subalgebra.restrictScalars ℝ A.toSubalgebra)))
      g ↔
    Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
      (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
        (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))
      g

Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_comap, Subalgebra.mem_restrictScalars,
    StarSubalgebra.mem_toSubalgebra, toContinuousMapₐ_apply, StarSubalgebra.mem_map]

Premises used: Subalgebra.mem_restrictScalars, StarSubalgebra.mem_toSubalgebra, Subalgebra.mem_map, Subalgebra.mem_comap, BoundedContinuousFunction.toContinuousMapₐ_apply, StarSubalgebra.mem_map
-- 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, ℝ)
h :
  (∃ (x : E →ᵇ ℝ),
      Membership.mem (α := E →ᵇ 𝕜) A
          ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
        (↑x : C(E, ℝ)) = g) →
    ∃ x ∈ A,
      Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
        ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
h₁ :
  (∃ x ∈ A,
      Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
        ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))) →
    ∃ (x : E →ᵇ ℝ),
      Membership.mem (α := E →ᵇ 𝕜) A
          ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
        (↑x : C(E, ℝ)) = g
⊢ (∃ (x : E →ᵇ ℝ),
      Membership.mem (α := E →ᵇ 𝕜) A
          ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
        (↑x : C(E, ℝ)) = g) ↔
    ∃ x ∈ A,
      Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
        ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))

Tactic:
constructor
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
right :
  Eq (α := C(E, 𝕜))
    ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
      C(E, 𝕜))
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
⊢ ∃ x ∈ A,
    Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
      ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))

Tactic:
use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA

Premises used: Real, RCLike.ofRealAm, RCLike.lipschitzWith_ofReal, BoundedContinuousFunction.AlgHom.compLeftContinuousBounded, DFunLike.coe
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
right :
  ∀ (a : E),
    Eq.{u_1 + 1} (α := 𝕜)
      ((((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
                ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
              C(E, 𝕜)) :
            (a : E) → 𝕜)
          a :
        𝕜)
      ((((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)
⊢ Eq (α := C(E, 𝕜))
    ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
      C(E, 𝕜))
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))

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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
a : E
right : Eq (α := ℝ) ((x : (a : E) → ℝ) a : ℝ) ((g : (a : E) → ℝ) a : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
              ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
            C(E, 𝕜)) :
          (a : E) → 𝕜)
        a :
      𝕜)
    ((((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)

Tactic:
simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuousBounded_apply_apply,
      ofRealAm_coe, AlgHom.compLeftContinuous_apply_apply, algebraMap.coe_inj]

Premises used: algebraMap.coe_inj, BoundedContinuousFunction.AlgHom.compLeftContinuousBounded_apply_apply, BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuous_apply_apply, RCLike.ofRealAm_coe
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
a : E
⊢ Eq (α := ℝ) ((x : (a : E) → ℝ) a : ℝ) ((g : (a : E) → ℝ) a : ℝ)

Tactic:
DFunLike.congr_fun hxg a

Premises used: DFunLike.congr_fun
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
a : E
⊢ Eq (α := ℝ) ((x : (a : E) → ℝ) a : ℝ) ((g : (a : E) → ℝ) a : ℝ)

Tactic:
exact DFunLike.congr_fun hxg a

Premises used: DFunLike.congr_fun
-- 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, 𝕜))
⊢ ∀ (a : E),
    Eq.{u_1 + 1} (α := 𝕜) ((((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)
      ((((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)

Tactic:
have hg_apply (a : E) := DFunLike.congr_fun hxg 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 :
  ∀ (a : E),
    Eq.{u_1 + 1} (α := 𝕜)
      ((((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
                (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) :
              E →ᵇ 𝕜) :
            (a : E) → 𝕜)
          a :
        𝕜)
      ((x : (a : E) → 𝕜) a : 𝕜)
⊢ (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
      (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) =
    x

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) : 𝕜) : 𝕜)
a : E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
              (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) :
            E →ᵇ 𝕜) :
          (a : E) → 𝕜)
        a :
      𝕜)
    ((x : (a : E) → 𝕜) a : 𝕜)

Tactic:
simp [hg_apply]
-- 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) : 𝕜) : 𝕜)
⊢ (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
      (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) =
    x

Tactic:
have h_comp_eq : (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal
        (x.comp reCLM (@reCLM 𝕜 _).lipschitz) = x := by
      ext a
      simp [hg_apply]
-- 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 :
  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
⊢ ∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
      (↑x : C(E, ℝ)) = g

Tactic:
use x.comp reCLM (@reCLM 𝕜 _).lipschitz

Premises used: BoundedContinuousFunction.comp, ContinuousLinearMap.lipschitz, RCLike.reCLM, DFunLike.coe
-- 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
rwa rwa₁ rwa₂ rwa₃ : x ∈ A
⊢ 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 →ᵇ 𝕜)

Tactic:
rwa [h_comp_eq]