awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
⊢ Eq (α := C(α, A)) { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := ⋯ } 0
have h : ∀ (a : α),
  Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := sorry } : (a : α) → A) a : A)
    ((0 : (a : α) → A) a : A)
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
⊢ { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := ⋯ } =
    HAdd.hAdd (α := C(α, A))
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) }
have h : ∀ (a : α),
  Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := sorry } : (a : α) → A) a : A)
    ((HAdd.hAdd (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := sorry : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := sorry : C(α, A) } :
          (a : α) → A)
        a :
      A)
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
⊢ HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f =
    HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A))
have h : ∀ (x : α),
  Eq.{u_3 + 1} (α := A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
    ((HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) : (a : α) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
⊢ c • f = HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f
have h : ∀ (x : α),
  Eq.{u_3 + 1} (α := A) ((c • f : (a : α) → A) x : A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
have obtain : ∀ (f : α → A) (m : Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s : Set C(α, A))) f)
  (w : f x ≠ f y),
  ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
Tactic: obtain ⟨f, m, w⟩ := h n
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
f : α → A
m : Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s : Set C(α, A))) f
w : f x ≠ f y
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
have rcases : ∀ (f : C(α, A)) (m : f ∈ (↑s : Set C(α, A)))
  (w :
    Ne.{u_3 + 1} (α := A) ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f x)
      ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f y)),
  ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
Tactic: rcases m with ⟨f, ⟨m, rfl⟩⟩
Cleared hypotheses: f, m, w
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
k : R
a : α
⊢ (((algebraMap R C(α, A) : (a : R) → C(α, A)) k : C(α, A)) : (a : α) → A) a = HSMul.hSMul (β := A) k 1
have rw : (HSMul.hSMul (β := C(α, A)) k 1 : (a : α) → A) a = HSMul.hSMul (β := A) k 1
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have pos : ∀ (n : x = y), ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
Tactic: by_cases n : x = y
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
pos : ∀ (n : x = y), ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have neg : ∀ (n : ¬x = y), ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
Tactic: by_cases n : x = y
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : x = y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have pos : ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) x = v x
Tactic: subst n
Cleared hypotheses: y, n
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have neg : ∀ (f : C(α, 𝕜)) (hf : f ∈ (↑s : Set C(α, 𝕜)))
  (hxy :
    Ne.{u_5 + 1} (α := 𝕜) ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f x)
      ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f y)),
  ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
Tactic: obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy :
  Ne.{u_5 + 1} (α := 𝕜) ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f x)
    ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f y)
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have hxy₁ : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
Tactic: replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have neg : ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) x = v x
Tactic: refine ⟨f', f'.prop, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
neg : ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) x = v x
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
have neg₁ : ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) y = v y
Tactic: refine ⟨f', f'.prop, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
⊢ s₁ = s₂
have inl : IsEmpty α → s₁ = s₂
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
inl : IsEmpty α → s₁ = s₂
⊢ s₁ = s₂
have inr : Nonempty α → s₁ = s₂
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : IsEmpty α
⊢ s₁ = s₂
have this : Subsingleton C(α, R)
Tactic: have : Subsingleton C(α, R) := DFunLike.coe_injective.subsingleton
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
⊢ s₁ = s₂
have inr : ∀ (inhabited_h : Inhabited α), s₁ = s₂
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
⊢ s₁ = s₂
have inr : ∀ (f : C(α, R)), f ∈ s₁ ↔ f ∈ s₂
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)
have h : ∀ (x' : α),
  Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R)
    (((algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) : (a : α) → R) x' : R)
Tactic: ext x'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R)
    (((algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) : (a : α) → R) x' : R)
have h : Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R) ((f : (a : α) → R) default : R)
Tactic: simp only [mul_one, smul_eq_mul, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R) ((f : (a : α) → R) default : R)
have h : x' = default
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f ∈ s₁ ↔ f ∈ s₂
have h : f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)
Tactic: have h : f = algebraMap R C(α, R) (f default) := by
        ext x'
        simp only [mul_one, smul_eq_mul, algebraMap_apply]
        congr
        simp [eq_iff_true_of_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)
⊢ f ∈ s₁ ↔ f ∈ s₂
have inr : (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₁ ↔
  (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
⊢ (c₁ * c₂) • f = c₁ • c₂ • f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) (((c₁ * c₂) • f : (a : α) → M) x : M) ((c₁ • c₂ • f : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
⊢ HSMul.hSMul (α := C(α, R)) 1 f = f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 1 f : (a : α) → M) x : M) ((f : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
r : C(α, R)
⊢ HSMul.hSMul (β := C(α, M)) r 0 = 0
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := C(α, M)) r 0 : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
⊢ c • (f + g) = c • f + c • g
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((c • (f + g) : (a : α) → M) x : M) ((c • f + c • g : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) (((c₁ + c₂) • f : (a : α) → M) x : M) ((c₁ • f + c₂ • f : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
⊢ HSMul.hSMul (α := C(α, R)) 0 f = 0
have h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 0 f : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : C(α, β)
⊢ (fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β)))
      ((fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) x) =
    x
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := β)
    (((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := sorry } : C(α, β)))
            ((fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) x) :
          (a : α) → β)
        a :
      β)
    ((x : (a : α) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : α → β
⊢ (fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β))) x) =
    x
have h : ∀ (x_1 : α),
  (fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := sorry } : C(α, β))) x) x_1 =
    x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : f.comp g₁ = f.comp g₂
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_3 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : f.comp g₁ = f.comp g₂
a : α
rw : Eq.{u_3 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_3 + 1} (α := γ) ((f.comp g₂ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : f.comp g₁ = f.comp g₂
a : α
rw : Eq.{u_3 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_3 + 1} (α := γ) ((f.comp g₂ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
  ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst, inst_1] f
⊢ (mkD f g : (a : α) → β) x = f x
have rw : ({ toFun := f, continuous_toFun := hf : C(α, β) } : (a : α) → β) x = f x
Tactic: rw [mkD_of_continuous hf, coe_mk]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst, inst_1] f
rw : ({ toFun := f, continuous_toFun := hf : C(α, β) } : (a : α) → β) x = f x
⊢ (mkD f g : (a : α) → β) x = f x
have rw₁ : f x = f x
Tactic: rw [mkD_of_continuous hf, coe_mk]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hf : ¬ContinuousOn f s
⊢ mkD (s.restrict (π := fun (a : α) ↦ β) f) g = g
have hf₁ : ¬Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
x : (↑s : Type u_1)
hf : ContinuousOn f s
⊢ (mkD (s.restrict (π := fun (a : α) ↦ β) f) g : (a : (↑s : Type u_1)) → β) x = f (↑x : α)
have rw : ({ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := sorry : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β } :
      (a : (↑s : Type u_1)) → β)
    x =
  f (↑x : α)
Tactic: rw [mkD_of_continuousOn hf, coe_mk, Set.restrict_apply]