awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
pos :
  ∀ (h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))),
    Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
have neg : ∀ (h : ¬Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))),
  Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
Tactic: by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
have h₁ : Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
  ((∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p)) :
        (a : X) → Y)
      x :
    Y)
Tactic: convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p)) :
          (a : X) → Y)
        x :
      Y)
have this : Summable (α := C(X, Y)) fun (c : ℤ) ↦
  f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))
Tactic: have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
this :
  Summable (α := C(X, Y)) fun (c : ℤ) ↦
    f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p)) :
          (a : X) → Y)
        x :
      Y)
have h₁ : Eq.{u_2 + 1} (α := Y) (∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p)) : (a : X) → Y) (x + p))
  (∑' (i : ℤ),
    (f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) i : ℤ) p)) : (a : X) → Y) x)
Tactic: simp_rw [← tsum_apply h, ← tsum_apply this]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
have neg : Eq.{u_2 + 1} (α := Y) ((0 : (a : X) → Y) (x + p) : Y) ((0 : (a : X) → Y) x : Y)
Tactic: rw [tsum_eq_zero_of_not_summable h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
⊢ Eq (α := C(R, R)) (toContinuousMap X) (ContinuousMap.id R)
have h : ∀ (a : R), Eq (α := R) ((toContinuousMap X : (a : R) → R) a : R) ((ContinuousMap.id R : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
⊢ Eq (α := C((↑s : Type u_1), R)) (toContinuousMapOn X s) (restrict s (ContinuousMap.id R))
have h : ∀ (a : (↑s : Type u_1)),
  Eq (α := R) ((toContinuousMapOn X s : (a : (↑s : Type u_1)) → R) a : R)
    ((restrict s (ContinuousMap.id R) : (a : (↑s : Type u_1)) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) g : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) g : R)
have refine_1 : ∀ (p q : R[X]),
  Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) p : C(α, R)) : (a : α) → R) x : R)
      (eval ((f : (a : α) → R) x) p : R) →
    Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) q : C(α, R)) : (a : α) → R) x : R)
        (eval ((f : (a : α) → R) x) q : R) →
      Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) (p + q) : C(α, R)) : (a : α) → R) x : R)
        (eval ((f : (a : α) → R) x) (p + q) : R)
Tactic: refine Polynomial.induction_on' g ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
refine_1 :
  ∀ (p q : R[X]),
    Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) p : C(α, R)) : (a : α) → R) x : R)
        (eval ((f : (a : α) → R) x) p : R) →
      Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) q : C(α, R)) : (a : α) → R) x : R)
          (eval ((f : (a : α) → R) x) q : R) →
        Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) (p + q) : C(α, R)) : (a : α) → R) x : R)
          (eval ((f : (a : α) → R) x) (p + q) : R)
⊢ Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) g : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) g : R)
have refine_2 : ∀ (n : ℕ) (a : R),
  Eq.{u_1 + 1} (α := R)
    ((((aeval f : (a : R[X]) → C(α, R)) ((monomial n : (a : R) → R[X]) a) : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) ((monomial n : (a : R) → R[X]) a) : R)
Tactic: refine Polynomial.induction_on' g ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap 1) 1
have h : ∀ (a : R), Eq (α := R) ((toContinuousMap 1 : (a : R) → R) a : R) ((1 : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
⊢ (x * x_1).toContinuousMap = HMul.hMul (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap
have h : ∀ (a : R),
  Eq (α := R) (((x * x_1).toContinuousMap : (a : R) → R) a : R)
    ((HMul.hMul (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap 0) 0
have h : ∀ (a : R), Eq (α := R) ((toContinuousMap 0 : (a : R) → R) a : R) ((0 : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
⊢ (x + x_1).toContinuousMap = HAdd.hAdd (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap
have h : ∀ (a : R),
  Eq (α := R) (((x + x_1).toContinuousMap : (a : R) → R) a : R)
    ((HAdd.hAdd (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x : R
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap ((algebraMap R R[X] : (a : R) → R[X]) x))
    ((algebraMap R C(R, R) : (a : R) → C(R, R)) x)
have h : ∀ (a : R),
  Eq (α := R) ((toContinuousMap ((algebraMap R R[X] : (a : R) → R[X]) x) : (a : R) → R) a : R)
    ((((algebraMap R C(R, R) : (a : R) → C(R, R)) x : C(R, R)) : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn 1 X) 1
have h : ∀ (a : (↑X : Type u_1)),
  Eq (α := R) ((toContinuousMapOn 1 X : (a : (↑X : Type u_1)) → R) a : R) ((1 : (a : (↑X : Type u_1)) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
⊢ (x * x_1).toContinuousMapOn X =
    HMul.hMul (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X)
have h : ∀ (a : (↑X : Type u_1)),
  Eq (α := R) (((x * x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
    ((HMul.hMul (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn 0 X) 0
have h : ∀ (a : (↑X : Type u_1)),
  Eq (α := R) ((toContinuousMapOn 0 X : (a : (↑X : Type u_1)) → R) a : R) ((0 : (a : (↑X : Type u_1)) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
⊢ (x + x_1).toContinuousMapOn X =
    HAdd.hAdd (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X)
have h : ∀ (a : (↑X : Type u_1)),
  Eq (α := R) (((x + x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
    ((HAdd.hAdd (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x : R
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn ((algebraMap R R[X] : (a : R) → R[X]) x) X)
    ((algebraMap R C((↑X : Type u_1), R) : (a : R) → C((↑X : Type u_1), R)) x)
have h : ∀ (a : (↑X : Type u_1)),
  Eq (α := R) ((toContinuousMapOn ((algebraMap R R[X] : (a : R) → R[X]) x) X : (a : (↑X : Type u_1)) → R) a : R)
    ((((algebraMap R C((↑X : Type u_1), R) : (a : R) → C((↑X : Type u_1), R)) x : C((↑X : Type u_1), R)) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
⊢ (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)) =
    Set.range (ι := R[X]) (⇑(toContinuousMapOnAlgHom X) : (a : R[X]) → C((↑X : Type u_1), R))
have h : ∀ (x : C((↑X : Type u_1), R)),
  x ∈ (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)) ↔
    Membership.mem (γ := Set C((↑X : Type u_1), R))
      (Set.range (ι := R[X]) (⇑(toContinuousMapOnAlgHom X) : (a : R[X]) → C((↑X : Type u_1), R))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
⊢ ∃ (f : (↑X : Type u_1) → R),
    Membership.mem (γ := Set ((↑X : Type u_1) → R))
        ((fun (f : C((↑X : Type u_1), R)) ↦ (⇑f : (a : (↑X : Type u_1)) → R)) ''
          (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)))
        f ∧
      f x ≠ f y
have refine : Ne.{u_1 + 1} (α := R)
  ((fun (f : C((↑X : Type u_1), R)) ↦ ((⇑f : (a : (↑X : Type u_1)) → R) : (a : (↑X : Type u_1)) → R))
    (((↑(toContinuousMapOnAlgHom X) : R[X] →+* C((↑X : Type u_1), R)) : (a : R[X]) → C((↑X : Type u_1), R))
      Polynomial.X)
    x)
  ((fun (f : C((↑X : Type u_1), R)) ↦ ((⇑f : (a : (↑X : Type u_1)) → R) : (a : (↑X : Type u_1)) → R))
    (((↑(toContinuousMapOnAlgHom X) : R[X] →+* C((↑X : Type u_1), R)) : (a : R[X]) → C((↑X : Type u_1), R))
      Polynomial.X)
    y)
Tactic: refine ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
⊢ ¬eval (↑x : R) Polynomial.X = eval (↑y : R) Polynomial.X
have simp : ¬(↑x : R) = (↑y : R)
Tactic: simp only [Polynomial.eval_X]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.comap
      (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
      (polynomialFunctions I))
    (polynomialFunctions (Set.Icc a b))
have h₁ : ∀ (f : C((↑(Set.Icc a b) : Type), ℝ)),
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f ↔
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f ↔
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
have h₁ : Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.comap
      (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
      (polynomialFunctions I))
    f →
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
h₁ :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f →
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f ↔
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
have h₂ : Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f →
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.comap
      (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
      (polynomialFunctions I))
    f
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (hypothesis)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  Eq (α := C((↑I : Type), ℝ))
    (((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) p :
      C((↑I : Type), ℝ))
    (((↑(compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))) :
            C((↑(Set.Icc a b) : Type), ℝ) →+* C((↑I : Type), ℝ)) :
          (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
        f :
      C((↑I : Type), ℝ))
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
have w₁ : ∀ (x : (↑I : Type)),
  Eq (α := ℝ)
    (((((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) p :
            C((↑I : Type), ℝ)) :
          (a : (↑I : Type)) → ℝ)
        x :
      ℝ)
    (((((↑(compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))) :
                  C((↑(Set.Icc a b) : Type), ℝ) →+* C((↑I : Type), ℝ)) :
                (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
              f :
            C((↑I : Type), ℝ)) :
          (a : (↑I : Type)) → ℝ)
        x :
      ℝ)
Tactic: rw [DFunLike.ext_iff] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
have h₁ : q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])
Tactic: refine ⟨q, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
h₁ : q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
have h₂ : ((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
      (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
    q =
  f
Tactic: refine ⟨q, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
⊢ ((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
        (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
      q =
    f
have h₁ : ∀ (x : (↑(Set.Icc a b) : Type)),
  Eq (α := ℝ)
    (((((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
              q :
            C((↑(Set.Icc a b) : Type), ℝ)) :
          (a : (↑(Set.Icc a b) : Type)) → ℝ)
        x :
      ℝ)
    ((f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
⊢ Eq (α := ℝ)
    (((((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
              q :
            C((↑(Set.Icc a b) : Type), ℝ)) :
          (a : (↑(Set.Icc a b) : Type)) → ℝ)
        x :
      ℝ)
    ((f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x : ℝ)
have h₁ : Polynomial.eval ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) p = (f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x
Tactic: simp only [q, neg_mul, map_neg, map_mul, AlgHom.coe_toRingHom,
        Polynomial.eval_X, Polynomial.eval_neg, Polynomial.eval_C, Polynomial.eval_smul,
        smul_eq_mul, Polynomial.eval_mul, Polynomial.eval_add,
        Polynomial.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
        Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
⊢ Polynomial.eval ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) p = (f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x
have h₁ : x =
  (Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) sorry)
Tactic: convert! w ⟨_, _⟩