awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    ((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 := hk;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) =
      r
have subst : ∀ (r : ℝ),
  ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
            let __spread.0 := hk;
            𝕜 →+ ℝ)
            (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            re)
            sorry :
          let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
          𝕜 →+ ℝ) :
        (a : 𝕜) → ℝ)
      (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
              ℝ →+* 𝕜 } :
            (a : ℝ) → 𝕜)
          r :
        𝕜) =
    r
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              r :
            𝕜) :
        ℝ)
      (0 : ℝ)
have subst : ∀ (r : ℝ),
  Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              im)
              sorry :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) :
      ℝ)
    (0 : ℝ)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                re)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
        ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                re)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          z :
        ℝ)
have subst : ∀ (z : 𝕜),
  Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              sorry :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
      ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              sorry :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        z :
      ℝ)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
        ℝ)
      (-((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            z :
        ℝ)
have subst : ∀ (z : 𝕜),
  Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              im)
              sorry :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
      ℝ)
    (-((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                sorry :
              let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          z :
      ℝ)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)
have subst : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    HMul.hMul (α := ℝ) (β := ℝ)
        (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            z :
          ℝ)
        (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            I :
          ℝ) =
      ((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              im)
              ⋯ :
            let __spread.0 := hk;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        z
have subst : ∀ (z : 𝕜),
  HMul.hMul (α := ℝ) (β := ℝ)
      (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                sorry :
              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)
                sorry :
              let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          I :
        ℝ) =
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
            let __spread.0 := hk;
            𝕜 →+ ℝ)
            (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            im)
            sorry :
          let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
          𝕜 →+ ℝ) :
        (a : 𝕜) → ℝ)
      z
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
hk : NormedField 𝕜
h : IsRCLikeNormedField 𝕜
⊢ RCLike 𝕜
have choose : (p : RCLike 𝕜) → (hp : hk = DenselyNormedField.toNormedField) → RCLike 𝕜
Tactic: choose p hp using h.out
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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).symm = α⁻¹ • e.symm
have h : ∀ (x : W), Eq.{u_6 + 1} (α := G) (((α • e).symm : (a : W) → G) x : G) ((α⁻¹ • e.symm : (a : W) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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
⊢ (α • e).trans f = HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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
⊢ e.trans (α • f) = HSMul.hSMul (β := V ≃ₗᵢ[𝕜] W) α (e.trans f)
have 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)
Tactic: ext
-- 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 →ᵇ 𝕜)
⊢ 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)))
have h : ∀ (g : C(E, ℝ)),
  Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
      (Subalgebra.map (toContinuousMapₐ ℝ)
        (Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry)
          (Subalgebra.restrictScalars ℝ A.toSubalgebra)))
      g ↔
    Membership.mem (γ := Subalgebra ℝ C(E, ℝ))
      (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm sorry)
        (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))
      g
Tactic: ext g
-- 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, ℝ)
⊢ 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
have h : (∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (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 sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
Tactic: simp only [Subalgebra.mem_map, Subalgebra.mem_comap, Subalgebra.mem_restrictScalars,
    StarSubalgebra.mem_toSubalgebra, toContinuousMapₐ_apply, StarSubalgebra.mem_map]
-- 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 →ᵇ ℝ),
      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, 𝕜))
have h : (∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (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 sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
Tactic: constructor
-- 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, ℝ)
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, 𝕜))
⊢ (∃ (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, 𝕜))
have h₁ : (∃ x ∈ A,
    Eq (α := C(E, 𝕜)) ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜))
      ((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))) →
  ∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
      (↑x : C(E, ℝ)) = g
Tactic: constructor
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑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, 𝕜))
have right : Eq (α := C(E, 𝕜))
  ((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
      ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
    C(E, 𝕜))
  ((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜))
Tactic: use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
⊢ 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, 𝕜))
have right : ∀ (a : E),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜))
              ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x) :
            C(E, 𝕜)) :
          (a : E) → 𝕜)
        a :
      𝕜)
    ((((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)
Tactic: ext a
-- 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 :
  Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜)
hxg : (↑x : C(E, ℝ)) = g
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 : 𝕜)
have right : Eq (α := ℝ) ((x : (a : E) → ℝ) a : ℝ) ((g : (a : E) → ℝ) a : ℝ)
Tactic: simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuousBounded_apply_apply,
      ofRealAm_coe, AlgHom.compLeftContinuous_apply_apply, algebraMap.coe_inj]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.BoundedContinuous (hypothesis)
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, 𝕜))
⊢ ∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
      (↑x : C(E, ℝ)) = g
have hg_apply : ∀ (a : E),
  Eq.{u_1 + 1} (α := 𝕜) ((((toContinuousMapStarₐ 𝕜 : (a : E →ᵇ 𝕜) → C(E, 𝕜)) x : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)
    ((((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(E, ℝ)) → C(E, 𝕜)) g : C(E, 𝕜)) : (a : E) → 𝕜) a : 𝕜)
Tactic: have hg_apply (a : E) := DFunLike.congr_fun hxg a
-- 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) : 𝕜) : 𝕜)
⊢ (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
      (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) ⋯ x) =
    x
have h : ∀ (a : E),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
              (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) :
            E →ᵇ 𝕜) :
          (a : E) → 𝕜)
        a :
      𝕜)
    ((x : (a : E) → 𝕜) a : 𝕜)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.RCLike.BoundedContinuous (hypothesis)
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) : 𝕜) : 𝕜)
⊢ ∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
      (↑x : C(E, ℝ)) = g
have h_comp_eq : (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
    (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) =
  x
Tactic: have h_comp_eq : (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal
        (x.comp reCLM (@reCLM 𝕜 _).lipschitz) = x := by
      ext a
      simp [hg_apply]
-- 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
⊢ ∃ (x : E →ᵇ ℝ),
    Membership.mem (α := E →ᵇ 𝕜) A
        ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯ : (a : E →ᵇ ℝ) → E →ᵇ 𝕜) x : E →ᵇ 𝕜) ∧
      (↑x : C(E, ℝ)) = g
have h : Membership.mem (α := E →ᵇ 𝕜) A
    ((AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) sorry : (a : E →ᵇ ℝ) → E →ᵇ 𝕜)
        (comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) :
      E →ᵇ 𝕜) ∧
  (↑(comp (⇑reCLM : (a : 𝕜) → ℝ) (C := NNNorm.nnnorm.{u_1} (E := 𝕜 →L[ℝ] ℝ) reCLM) sorry x) : C(E, ℝ)) = g
Tactic: use x.comp reCLM (@reCLM 𝕜 _).lipschitz