awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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_1 s : C(α, R)
s_mem : Membership.mem (γ := Set C(α, R)) (Set.range fun (s : C(α, R)) ↦ star s * s) s
p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + (s + p)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have mp : ∀ (s : C(α, R)) (hp : (↑g : C(α, R)) = (↑f : C(α, R)) + ((fun (s : C(α, R)) ↦ star s * s) s + p)),
  ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
Tactic: obtain ⟨s, rfl⟩ := s_mem
Cleared hypotheses: s, s_mem, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (hypothesis)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + (star s * s + p)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
Tactic: have h₀ : (star s * s + p) 0 = 0 := by simpa using congr($(hp) 0).symm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (hypothesis)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + (star s * s + p)
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have hp₁ : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
Tactic: rw [← add_assoc] at hp
Cleared hypotheses: hp, h₀
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
⊢ LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
have rw : ∀ (p_mem : 0 ≤ p)
  (hp' :
    ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀) (s : C(α, R)) (hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p)
  (h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)),
  LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
Tactic: rw [← StarOrderedRing.nonneg_iff] at p_mem
Cleared hypotheses: p_mem, hp', f, g, s, hp, h₀
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (hypothesis)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
Tactic: have p'₀ : 0 ≤ p 0 := by rw [← StarOrderedRing.nonneg_iff] at p_mem; exact p_mem 0
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (hypothesis)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have s₉ : Eq.{u_2 + 1} (α := R) ((star s * s : (a : α) → R) 0 : R) (0 : R)
Tactic: have s₉ : (star s * s) 0 = 0 := le_antisymm ((le_add_of_nonneg_right p'₀).trans_eq h₀)
          (star_mul_self_nonneg (s 0))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (hypothesis)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
s₉ : Eq.{u_2 + 1} (α := R) ((star s * s : (a : α) → R) 0 : R) (0 : R)
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have s₀' : Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)
Tactic: have s₀' : s 0 = 0 := by aesop
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
s₉ : Eq.{u_2 + 1} (α := R) ((star s * s : (a : α) → R) 0 : R) (0 : R)
s₀' : Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)
s' : C(α, R)₀ := { toContinuousMap := s, map_zero' := s₀' }
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have mp : ∀ (p' : C(α, R)₀)
  (hp'_mem :
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p')
  (hp : (↑(f + star s' * s' + p') : C(α, R)) = (↑f : C(α, R)) + star s * s + p),
  ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      f + star s' * s' + p' = f + p
Tactic: obtain ⟨p', hp'_mem, rfl⟩ := hp' (f + star s' * s') g hp
Cleared hypotheses: g, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
s₉ : Eq.{u_2 + 1} (α := R) ((star s * s : (a : α) → R) 0 : R) (0 : R)
s₀' : Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)
s' : C(α, R)₀ := { toContinuousMap := s, map_zero' := s₀' }
p' : C(α, R)₀
hp'_mem :
  Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p'
hp : (↑(f + star s' * s' + p') : C(α, R)) = (↑f : C(α, R)) + star s * s + p
⊢ f + star s' * s' + p' = f + (star s' * s' + p')
have rw : f + (star s' * s' + p') = f + (star s' * s' + p')
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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_1 p : C(α, R)
p_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp' :
  ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀
s : C(α, R)
h₀ : Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)
p'₀ : LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)
s₉ : Eq.{u_2 + 1} (α := R) ((star s * s : (a : α) → R) 0 : R) (0 : R)
s₀' : Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)
s' : C(α, R)₀ := { toContinuousMap := s, map_zero' := s₀' }
p' : C(α, R)₀
hp'_mem :
  Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p'
hp : (↑(f + star s' * s' + p') : C(α, R)) = (↑f : C(α, R)) + star s * s + p
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      f + star s' * s' + p' = f + p
have mp : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s))
  (star s' * s' + p')
Tactic: refine ⟨star s' * s' + p', ?_, by rw [add_assoc]⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)₀
p : C(α, R)
hp_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp : (↑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
have mp : ∀ (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: induction hp_mem using AddSubmonoid.closure_induction_left generalizing f g with
      | zero => exact ⟨0, zero_mem _, by ext x; congrm($(hp) x)⟩
      | add_left s s_mem p p_mem hp' =>
        obtain ⟨s, rfl⟩ := s_mem
        simp only at *
        have h₀ : (star s * s + p) 0 = 0 := by simpa using congr($(hp) 0).symm
        rw [← add_assoc] at hp
        have p'₀ : 0 ≤ p 0 := by rw [← StarOrderedRing.nonneg_iff] at p_mem; exact p_mem 0
        have s₉ : (star s * s) 0 = 0 := le_antisymm ((le_add_of_nonneg_right p'₀).trans_eq h₀)
          (star_mul_self_nonneg (s 0))
        have s₀' : s 0 = 0 := by aesop
        let s' : C(α, R)₀ := ⟨s, s₀'⟩
        obtain ⟨p', hp'_mem, rfl⟩ := hp' (f + star s' * s') g hp
        refine ⟨star s' * s' + p', ?_, by rw [add_assoc]⟩
        exact add_mem (AddSubmonoid.subset_closure ⟨s', rfl⟩) hp'_mem
Cleared hypotheses: f, g, hp_mem, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)₀
p : C(α, R)
hp_mem : Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p
hp : (↑g : C(α, R)) = (↑f : C(α, R)) + p
mp :
  ∀ (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
⊢ ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
have mp₁ : ∀ (s : C(α, R)) (s_mem : Membership.mem (γ := Set C(α, R)) (Set.range fun (s : C(α, R)) ↦ star s * s) s) (p : C(α, R))
  (p_mem :
    Membership.mem (γ := AddSubmonoid C(α, R)) (AddSubmonoid.closure (Set.range fun (s : C(α, R)) ↦ star s * s)) p)
  (hp' :
    ∀ (f g : C(α, R)₀) (hp : (↑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 : C(α, R)₀) (hp : (↑g : C(α, R)) = (↑f : C(α, R)) + (s + p)),
  ∃ (p : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p ∧
      g = f + p
Tactic: induction hp_mem using AddSubmonoid.closure_induction_left generalizing f g with
      | zero => exact ⟨0, zero_mem _, by ext x; congrm($(hp) x)⟩
      | add_left s s_mem p p_mem hp' =>
        obtain ⟨s, rfl⟩ := s_mem
        simp only at *
        have h₀ : (star s * s + p) 0 = 0 := by simpa using congr($(hp) 0).symm
        rw [← add_assoc] at hp
        have p'₀ : 0 ≤ p 0 := by rw [← StarOrderedRing.nonneg_iff] at p_mem; exact p_mem 0
        have s₉ : (star s * s) 0 = 0 := le_antisymm ((le_add_of_nonneg_right p'₀).trans_eq h₀)
          (star_mul_self_nonneg (s 0))
        have s₀' : s 0 = 0 := by aesop
        let s' : C(α, R)₀ := ⟨s, s₀'⟩
        obtain ⟨p', hp'_mem, rfl⟩ := hp' (f + star s' * s') g hp
        refine ⟨star s' * s' + p', ?_, by rw [add_assoc]⟩
        exact add_mem (AddSubmonoid.subset_closure ⟨s', rfl⟩) hp'_mem
Cleared hypotheses: f, g, hp_mem, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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 s : C(α, R)₀
s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s
f : C(α, R)₀
⊢ f ≤ f + s
have mpr : ∀ (s : C(α, R)₀), f ≤ f + (fun (s : C(α, R)₀) ↦ star s * s) s
Tactic: obtain ⟨s, rfl⟩ := s_mem
Cleared hypotheses: s, s_mem
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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 p : C(α, R)₀
hp : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p
⊢ f ≤ f + p
have mpr : ∀ (s : C(α, R)₀) (s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s)
  (f : C(α, R)₀), f ≤ f + s
Tactic: induction hp using AddSubmonoid.closure_induction generalizing f with
      | mem s s_mem =>
        obtain ⟨s, rfl⟩ := s_mem
        exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))
      | zero => simp
      | add g₁ g₂ _ _ h₁ h₂ => calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _
Cleared hypotheses: f, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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 p : C(α, R)₀
hp : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p
mpr :
  ∀ (s : C(α, R)₀) (s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s)
    (f : C(α, R)₀), f ≤ f + s
⊢ f ≤ f + p
have mpr₁ : ∀ (f : C(α, R)₀), f ≤ f + 0
Tactic: induction hp using AddSubmonoid.closure_induction generalizing f with
      | mem s s_mem =>
        obtain ⟨s, rfl⟩ := s_mem
        exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))
      | zero => simp
      | add g₁ g₂ _ _ h₁ h₂ => calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _
Cleared hypotheses: f, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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 p : C(α, R)₀
hp : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p
mpr :
  ∀ (s : C(α, R)₀) (s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s)
    (f : C(α, R)₀), f ≤ f + s
mpr₁ : ∀ (f : C(α, R)₀), f ≤ f + 0
⊢ f ≤ f + p
have mpr₂ : ∀ (g₁ g₂ : C(α, R)₀),
  Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁ →
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₂ →
      ∀ (h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁) (h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂) (f : C(α, R)₀), f ≤ f + (g₁ + g₂)
Tactic: induction hp using AddSubmonoid.closure_induction generalizing f with
      | mem s s_mem =>
        obtain ⟨s, rfl⟩ := s_mem
        exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))
      | zero => simp
      | add g₁ g₂ _ _ h₁ h₂ => calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _
Cleared hypotheses: f, hp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound =
    (↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ))
have h : ∀ (a : X),
  Eq (α := ℝ)
    ((comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound :
          (a : X) → ℝ)
        a :
      ℝ)
    (((↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ)) : (a : X) → ℝ) a : ℝ)
Tactic: ext