awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
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
⊢ ∃ (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

Premises used: rfl
-- 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_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)
⊢ Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)

Tactic:
simpa using congr($(hp) 0).symm

Premises used: congrArg, id, OfNat.ofNat, Eq.symm, 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)
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)
⊢ 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
-- 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_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)
⊢ (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p

Tactic:
rw [← add_assoc] at hp

Premises used: add_assoc
-- 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_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)
hp₁ : (↑g : C(α, R)) = (↑f : C(α, R)) + star s * s + p
⊢ Eq.{u_2 + 1} (α := R) ((star s * s + p : (a : α) → R) 0 : R) (0 : R)

Tactic:
rw [← add_assoc] at hp

Premises used: add_assoc
-- 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_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)
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)
⊢ LE.le.{u_2} (α := R) (0 : R) ((p : (a : α) → R) 0 : R)

Tactic:
rw [← StarOrderedRing.nonneg_iff] at p_mem

Premises used: StarOrderedRing.nonneg_iff
-- 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_1 p : C(α, R)
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:
p_mem 0

Premises used: OfNat.ofNat
-- 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_1 p : C(α, R)
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:
exact p_mem 0

Premises used: OfNat.ofNat
-- 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_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)

Tactic:
have p'₀ : 0 ≤ p 0 := by rw [← StarOrderedRing.nonneg_iff] at p_mem; exact p_mem 0
-- 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_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)
⊢ 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))
-- 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_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)
⊢ Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)

Tactic:
aesop
-- 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_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)
⊢ Eq.{u_2 + 1} (α := R) ((s : (a : α) → R) 0 : R) (0 : R)

Tactic:
have s₀' : s 0 = 0 := by aesop
-- 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_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₀' }
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
⊢ ∃ (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 ⟨p', hp'_mem, rfl⟩ := hp' (f + star s' * s') g hp

Premises used: HMul.hMul, HAdd.hAdd, rfl, Star.star
-- 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_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
rw rw₁ : f + (star s' * s' + p') = f + (star s' * s' + p')
⊢ f + star s' * s' + p' = f + (star s' * s' + p')

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- 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_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
mp :
  Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s))
    (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:
refine ⟨star s' * s' + p', ?_, by rw [add_assoc]⟩
-- 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_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
⊢ Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s))
    (star s' * s' + p')

Tactic:
add_mem (AddSubmonoid.subset_closure ⟨s', rfl⟩) hp'_mem

Premises used: AddSubmonoid.subset_closure, Exists.intro, AddMemClass.add_mem, rfl
-- 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_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
⊢ Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s))
    (star s' * s' + p')

Tactic:
exact add_mem (AddSubmonoid.subset_closure ⟨s', rfl⟩) hp'_mem
-- 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)₀
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
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
⊢ ∃ (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

Premises used: add_assoc, rfl