awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : Set X
hU : U ∈ countableBasis X
hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ U }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
⊢ ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
have h : ∀ (U : { x : Set X // x ∈ countableBasis X }) (hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V)
  (x : { x : X // x ∈ (↑U : Set X) }) (hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)),
  ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
Tactic: lift U to countableBasis X using hU
Cleared hypotheses: U, hU, hUV, x, hxV
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
⊢ ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
have h : ∀ (n : ℕ)
  (hn :
    Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))),
  ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
Tactic: rcases (K U).exists_mem_nhds x with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
have h : image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
  𝓝 (↑x : X)
Tactic: refine ⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
h :
  image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
    𝓝 (↑x : X)
⊢ ∃ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
have h₁ : MapsTo.{u_1, u_2} (α := X) (⇑f : (a : X) → Y)
  (image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
  V
Tactic: refine ⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
    𝓝 (↑x : X)
have h : image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
  map (Subtype.val (p := Membership.mem (↑U : Set X))) (𝓝 (Subtype.mk (p := Membership.mem (↑U : Set X)) (↑x : X) sorry))
Tactic: rw [← map_nhds_subtype_coe_eq_nhds x.2]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
h :
  image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
    map (Subtype.val (p := Membership.mem (↑U : Set X))) (𝓝 (Subtype.mk (p := Membership.mem (↑U : Set X)) (↑x : X) ⋯))
⊢ image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) ∈
    𝓝 (↑x : X)
have h₁ : ∀ᶠ (x : X) in 𝓝 (↑x : X), x ∈ (↑U : Set X)
Tactic: rw [← map_nhds_subtype_coe_eq_nhds x.2]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ MapsTo.{u_1, u_2} (α := X) (⇑f : (a : X) → Y)
    (image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
    V
have h : MapsTo.{u_1, u_2} (α := { x : X // x ∈ (↑U : Set X) })
  ((⇑f : (a : X) → Y) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
  ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) V
Tactic: rw [mapsTo_image_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Sigma (goal)
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'))
⊢ 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')
have 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')
Tactic: obtain ⟨rfl, hg⟩ : i = i' ∧ ⇑g ≍ ⇑g' :=
      Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h
Cleared hypotheses: i', g', h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)
have refine : ∀ (x y : C(α, R)), x ≤ y ↔ ∃ (s : C(α, R)), y = x + star s * s
Tactic: refine StarOrderedRing.of_le_iff ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)
⊢ f ≤ g ↔ ∃ (s : C(α, R)), g = f + star s * s
have mp : f ≤ g → ∃ (s : C(α, R)), g = f + star s * s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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
⊢ f ≤ g ↔ ∃ (s : C(α, R)), g = f + star s * s
have mpr : (∃ (s : C(α, R)), g = f + star s * s) → f ≤ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)
⊢ f ≤ g → ∃ (s : C(α, R)), g = f + star s * s
have 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
Tactic: rw [ContinuousMap.le_def]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)
⊢ ∃ (s : C(α, R)), g = f + star s * s
have 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry :
          ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) })
Tactic: use (mk _ ContinuousSqrt.continuousOn_sqrt.restrict).comp
      ⟨_, map_continuous (f.prodMk g) |>.codRestrict (s := {x | x.1 ≤ x.2}) (by exact h)⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StarOrdered (goal)
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)
⊢ 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) })
have 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : ContinuousMap.{u_1, u_2} α (↑{x : R × R | x.1 ≤ x.2} : Type u_2) }) :
          (a : α) → R)
        x :
      R)
Tactic: ext x
-- 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)₀
⊢ 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
have 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
Tactic: constructor
-- 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)₀
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
⊢ 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
have 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
Tactic: constructor
-- 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)₀
⊢ 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
have 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
Tactic: rw [le_def, ← ContinuousMap.coe_coe, ← ContinuousMap.coe_coe g, ← ContinuousMap.le_def,
        StarOrderedRing.le_iff]
-- 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 : C(α, R)
f g : C(α, R)₀
hp : (↑g : C(α, R)) = HAdd.hAdd (α := C(α, R)) (↑f : C(α, R)) 0
⊢ g = f + 0
have h : ∀ (x : α), Eq.{u_2 + 1} (α := R) ((g : (a : α) → R) x : R) ((f + 0 : (a : α) → R) x : R)
Tactic: ext x