awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Sigma
Goal:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst : TopologicalSpace X
inst_1 : (i : ι) → TopologicalSpace (Y i)
inst_2 : Nonempty X
i : ι
g : ContinuousMap.{u_1, u_3} X (Y i)
i' : ι
g' : ContinuousMap.{u_1, u_3} X (Y i')
h :
  Eq (α := C(X, (i : ι) × Y i))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i' g'))
obtain :
  ∀ (g' : ContinuousMap.{u_1, u_3} X (Y i))
    (h :
      Eq (α := C(X, (i : ι) × Y i))
        ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
            comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
              (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g))
        ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
            comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
              (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g')))
    (hg : HEq (α := (a : X) → Y i) (⇑g : (a : X) → Y i) (β := (a : X) → Y i) (⇑g' : (a : X) → Y i)),
    Eq (α := (i : ι) × ContinuousMap.{u_1, u_3} X (Y i))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g)
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g')
⊢ Eq (α := (i : ι) × ContinuousMap.{u_1, u_3} X (Y i))
    (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g)
    (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i' g')

Tactic:
obtain ⟨rfl, hg⟩ : i = i' ∧ ⇑g ≍ ⇑g' :=
      Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h

Premises used: congr_arg, Function.eq_of_sigmaMk_comp, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.Sigma
Goal:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst : TopologicalSpace X
inst_1 : (i : ι) → TopologicalSpace (Y i)
inst_2 : Nonempty X
i : ι
g g' : ContinuousMap.{u_1, u_3} X (Y i)
h :
  Eq (α := C(X, (i : ι) × Y i))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g'))
hg : HEq (α := (a : X) → Y i) (⇑g : (a : X) → Y i) (β := (a : X) → Y i) (⇑g' : (a : X) → Y i)
⊢ Eq (α := (i : ι) × ContinuousMap.{u_1, u_3} X (Y i))
    (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g)
    (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g')

Tactic:
simpa using hg
-- Module: Mathlib.Topology.ContinuousMap.Sigma
Goal:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst : TopologicalSpace X
inst_1 : (i : ι) → TopologicalSpace (Y i)
inst_2 : ConnectedSpace X
f : C(X, (i : ι) × Y i)
⊢ ∃ (i : ι) (g : ContinuousMap.{u_1, u_3} X (Y i)), f = comp (sigmaMk (X := Y) i) g

Tactic:
let ⟨i, g, hg, hfg⟩ := (map_continuous f).exists_lift_sigma
  ⟨i, ⟨g, hg⟩, DFunLike.ext' hfg⟩

Premises used: ContinuousMap.mk, ContinuousMap.sigmaMk, ContinuousMap.comp, _private.0.ContinuousMap.exists_lift_sigma.match_1, Exists, Exists.intro, ContinuousMapClass.map_continuous, DFunLike.ext', Continuous.exists_lift_sigma, Eq
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Star β
inst_3 : ContinuousStar β
f : C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(star f) : (a : α) → β) (star (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Star β
inst_3 : ContinuousStar β
f : C(α, β)
x : α
⊢ Eq.{u_3 + 1} (α := β) ((star f : (a : α) → β) x : β) (star ((f : (a : α) → β) x) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
inst : TopologicalSpace X
𝕜 : Type u_4
inst_1 : CommSemiring 𝕜
A : Type u_5
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : IsTopologicalSemiring A
inst_5 : Star A
inst_6 : ContinuousStar A
inst_7 : Algebra 𝕜 A
⊢ Eq (α := C(X, A) →⋆ₐ[𝕜] C(X, A)) (compStarAlgHom' 𝕜 A (ContinuousMap.id X)) (StarAlgHom.id 𝕜 C(X, A))

Tactic:
StarAlgHom.ext fun _ => ContinuousMap.ext fun _ => rfl

Premises used: ContinuousMap.ext, StarAlgHom.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
𝕜 : Type u_4
inst_3 : CommSemiring 𝕜
A : Type u_5
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : IsTopologicalSemiring A
inst_7 : Star A
inst_8 : ContinuousStar A
inst_9 : Algebra 𝕜 A
g : C(Y, Z)
f : C(X, Y)
⊢ Eq (α := C(Z, A) →⋆ₐ[𝕜] C(X, A)) (compStarAlgHom' 𝕜 A (g.comp f))
    (StarAlgHom.comp (compStarAlgHom' 𝕜 A f) (compStarAlgHom' 𝕜 A g))

Tactic:
StarAlgHom.ext fun _ => ContinuousMap.ext fun _ => rfl

Premises used: ContinuousMap.ext, StarAlgHom.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : CommSemiring 𝕜
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : IsTopologicalSemiring A
inst_5 : Star A
inst_6 : ContinuousStar A
inst_7 : Algebra 𝕜 A
⊢ Eq (α := C(X, A) →⋆ₐ[𝕜] C(X, A)) (compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯) (StarAlgHom.id 𝕜 C(X, A))

Tactic:
rfl

Premises used: StarAlgHom.id, AlgHom.id, ContinuousMap.comp, ContinuousMap.compStarAlgHom, rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : TopologicalSpace X
inst_1 : CommSemiring 𝕜
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : IsTopologicalSemiring A
inst_5 : Star A
inst_6 : ContinuousStar A
inst_7 : Algebra 𝕜 A
inst_8 : TopologicalSpace B
inst_9 : Semiring B
inst_10 : IsTopologicalSemiring B
inst_11 : Star B
inst_12 : ContinuousStar B
inst_13 : Algebra 𝕜 B
inst_14 : TopologicalSpace C
inst_15 : Semiring C
inst_16 : IsTopologicalSemiring C
inst_17 : Star C
inst_18 : ContinuousStar C
inst_19 : Algebra 𝕜 C
φ : A →⋆ₐ[𝕜] B
ψ : B →⋆ₐ[𝕜] C
hφ : Continuous.{u_3, u_4} (X := A) (Y := B) (⇑φ : (a : A) → B)
hψ : Continuous.{u_4, u_5} (X := B) (Y := C) (⇑ψ : (a : B) → C)
⊢ Eq (α := C(X, A) →⋆ₐ[𝕜] C(X, C)) (compStarAlgHom X (ψ.comp φ) ⋯)
    (StarAlgHom.comp (compStarAlgHom X ψ hψ) (compStarAlgHom X φ hφ))

Tactic:
rfl

Premises used: ContinuousMap.comp, ContinuousMap.compStarAlgHom, StarAlgHom.comp, AlgHom.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
𝕜 : Type u_3
inst_2 : CommSemiring 𝕜
A : Type u_4
inst_3 : TopologicalSpace A
inst_4 : Semiring A
inst_5 : IsTopologicalSemiring A
inst_6 : StarRing A
inst_7 : ContinuousStar A
inst_8 : Algebra 𝕜 A
f : X ≃ₜ Y
g : C(Y, A)
⊢ (ContinuousMap.compStarAlgHom' 𝕜 A (↑f.symm : C(Y, X)) : (a : C(X, A)) → C(Y, A))
      ((ContinuousMap.compStarAlgHom' 𝕜 A (↑f : C(X, Y)) : (a : C(Y, A)) → C(X, A)) g) =
    g

Tactic:
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc,
        toContinuousMap_comp_symm, ContinuousMap.comp_id]

Premises used: ContinuousMap.comp_id, Homeomorph.toContinuousMap_comp_symm, ContinuousMap.comp_assoc, ContinuousMap.compStarAlgHom'_apply
-- Module: Mathlib.Topology.ContinuousMap.Star
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
𝕜 : Type u_3
inst_2 : CommSemiring 𝕜
A : Type u_4
inst_3 : TopologicalSpace A
inst_4 : Semiring A
inst_5 : IsTopologicalSemiring A
inst_6 : StarRing A
inst_7 : ContinuousStar A
inst_8 : Algebra 𝕜 A
f : X ≃ₜ Y
g : C(X, A)
⊢ (ContinuousMap.compStarAlgHom' 𝕜 A (↑f : C(X, Y)) : (a : C(Y, A)) → C(X, A))
      ((ContinuousMap.compStarAlgHom' 𝕜 A (↑f.symm : C(Y, X)) : (a : C(X, A)) → C(Y, A)) g) =
    g

Tactic:
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc,
        symm_comp_toContinuousMap, ContinuousMap.comp_id]

Premises used: ContinuousMap.comp_id, ContinuousMap.comp_assoc, ContinuousMap.compStarAlgHom'_apply, Homeomorph.symm_comp_toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
⊢ StarOrderedRing C(α, R)

Tactic:
StarOrderedRing.of_le_iff ?_

Premises used: StarOrderedRing.of_le_iff
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
refine : ∀ (x y : C(α, R)), x ≤ y ↔ ∃ (s : C(α, R)), y = x + star s * s
⊢ StarOrderedRing C(α, R)

Tactic:
refine StarOrderedRing.of_le_iff ?_

Premises used: StarOrderedRing.of_le_iff
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
mp : f ≤ g → ∃ (s : C(α, R)), g = f + star s * s
mpr : (∃ (s : C(α, R)), g = f + star s * s) → f ≤ g
⊢ f ≤ g ↔ ∃ (s : C(α, R)), g = f + star s * s

Tactic:
constructor
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
mp :
  (∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)) →
    ∃ (s : C(α, R)), g = f + star s * s
⊢ f ≤ g → ∃ (s : C(α, R)), g = f + star s * s

Tactic:
rw [ContinuousMap.le_def]

Premises used: ContinuousMap.le_def
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)
⊢ ∀ (a : α),
    Membership.mem.{u_2, u_2} (α := R × R) (γ := Set (R × R)) {x : R × R | x.1 ≤ x.2}
      ((f.prodMk g : (a : α) → R × R) a : R × R)

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)
⊢ ∀ (a : α),
    Membership.mem.{u_2, u_2} (α := R × R) (γ := Set (R × R)) {x : R × R | x.1 ≤ x.2}
      ((f.prodMk g : (a : α) → R × R) a : R × R)

Tactic:
exact h
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)
h₁ :
  g =
    f +
      HMul.hMul (α := C(α, R))
        (star
          (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
            {
              toFun :=
                Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                  (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
              continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
            { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
              continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }))
        (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
          {
            toFun :=
              Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
            continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
          { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
            continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) })
⊢ ∃ (s : C(α, R)), g = f + star s * s

Tactic:
use (mk _ ContinuousSqrt.continuousOn_sqrt.restrict).comp
      ⟨_, map_continuous (f.prodMk g) |>.codRestrict (s := {x | x.1 ≤ x.2}) (by exact h)⟩

Premises used: ContinuousMap.mk, ContinuousMap.comp, ContinuousOn.restrict, ContinuousSqrt.continuousOn_sqrt
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)
h₁ :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := R) ((g : (a : α) → R) x : R)
      ((f +
              HMul.hMul (α := C(α, R))
                (star
                  (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
                    {
                      toFun :=
                        Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                          (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
                      continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
                    { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
                      continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }))
                (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
                  {
                    toFun :=
                      Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                        (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
                    continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
                  { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
                    continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }) :
            (a : α) → R)
          x :
        R)
⊢ g =
    f +
      HMul.hMul (α := C(α, R))
        (star
          (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
            {
              toFun :=
                Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                  (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
              continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
            { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
              continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }))
        (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
          {
            toFun :=
              Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
            continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
          { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
            continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) })

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f g : C(α, R)
h : ∀ (a : α), LE.le.{u_2} (α := R) ((f : (a : α) → R) a : R) ((g : (a : α) → R) a : R)
x : α
⊢ Eq.{u_2 + 1} (α := R) ((g : (a : α) → R) x : R)
    ((f +
            HMul.hMul (α := C(α, R))
              (star
                (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
                  {
                    toFun :=
                      Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                        (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
                    continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
                  { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
                    continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }))
              (comp (β := (↑{x : R × R | x.1 ≤ x.2} : Type u_2))
                {
                  toFun :=
                    Set.restrict (π := fun (a : R × R) ↦ R) {x : R × R | x.1 ≤ x.2}
                      (@ContinuousSqrt.sqrt _ Preorder.toLE inst_2 inst_5 _),
                  continuous_toFun := ⋯ : C((↑{x : R × R | x.1 ≤ x.2} : Type u_2), R) }
                { toFun := Set.codRestrict (⇑(f.prodMk g) : (a : α) → R × R) {x : R × R | x.1 ≤ x.2} h,
                  continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }) :
          (a : α) → R)
        x :
      R)

Tactic:
simpa [IsSelfAdjoint.star_eq <| .of_nonneg (ContinuousSqrt.sqrt_nonneg (f x, g x) (h x))]
      using ContinuousSqrt.sqrt_mul_sqrt (f x, g x) (h x)

Premises used: ContinuousSqrt.sqrt_mul_sqrt, Prod.mk, DFunLike.coe, IsSelfAdjoint.star_eq
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f p : C(α, R)
⊢ f ≤ f + star p * p

Tactic:
fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))

Premises used: star_mul_self_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : PartialOrder R
inst_2 : NonUnitalSemiring R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : TopologicalSpace R
inst_6 : ContinuousStar R
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousSqrt R
f p : C(α, R)
⊢ f ≤ f + star p * p

Tactic:
exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))

Premises used: star_mul_self_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
f g : C(α, R)₀
mp :
  f ≤ g →
    ∃ (p : C(α, R)₀),
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
        g = f + p
mpr :
  (∃ (p : C(α, R)₀),
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
        g = f + p) →
    f ≤ g
⊢ f ≤ g ↔
    ∃ (p : C(α, R)₀),
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
        g = f + p

Tactic:
constructor
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
f g : C(α, R)₀
mp :
  (∃ (p : C(α, R)),
      Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p ∧
        (↑g : C(α, R)) = (↑f : C(α, R)) + p) →
    ∃ (p : C(α, R)₀),
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
        g = f + p
⊢ f ≤ g →
    ∃ (p : C(α, R)₀),
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
        g = f + p

Tactic:
rw [le_def, ← ContinuousMap.coe_coe, ← ContinuousMap.coe_coe g, ← ContinuousMap.le_def,
        StarOrderedRing.le_iff]

Premises used: ContinuousMap.le_def, ContinuousMapZero.le_def, StarOrderedRing.le_iff, ContinuousMap.coe_coe
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p : C(α, R)
f g : C(α, R)₀
hp : (↑g : C(α, R)) = HAdd.hAdd (α := C(α, R)) (↑f : C(α, R)) 0
h : ∀ (x : α), Eq.{u_2 + 1} (α := R) ((g : (a : α) → R) x : R) ((f + 0 : (a : α) → R) x : R)
⊢ g = f + 0

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p : C(α, R)
f g : C(α, R)₀
hp : (↑g : C(α, R)) = HAdd.hAdd (α := C(α, R)) (↑f : C(α, R)) 0
x : α
⊢ Eq.{u_2 + 1} (α := R) ((g : (a : α) → R) x : R) ((f + 0 : (a : α) → R) x : R)

Tactic:
congrm($(hp) x)
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p : C(α, R)
f g : C(α, R)₀
hp : (↑g : C(α, R)) = HAdd.hAdd (α := C(α, R)) (↑f : C(α, R)) 0
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p

Tactic:
exact ⟨0, zero_mem _, by ext x; congrm($(hp) x)⟩