ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℝ<GOAL>Real.log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.log (x ^ n) = ↑n * Real.log x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.log (x ^ n) = ↑n * Real.log x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>Real.log √x = Real.log x / 2
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.log x ≤ x - 1
<VAR>x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<GOAL>|Real.log x * x| < 1
<GOAL>Filter.Tendsto Real.log (𝓝[≠] 0) Filter.atBot
<GOAL>Filter.Tendsto Real.log (𝓝[>] 0) Filter.atBot
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>ContinuousAt Real.log x
<VAR>x : ℝ<GOAL>ContinuousAt Real.log x ↔ x ≠ 0
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ x ∈ s, f x ≠ 0<GOAL>Real.log (∏ i ∈ s, f i) = ∑ i ∈ s, Real.log (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>f : α →₀ β<VAR>g : α → β → ℝ<VAR>hg : ∀ (a : α), g a (f a) = 0 → f a = 0<GOAL>Real.log (f.prod g) = f.sum fun a b => Real.log (g a b)
<VAR>n : ℕ<GOAL>Real.log ↑n = n.factorization.sum fun p t => ↑t * Real.log ↑p
<VAR>a b : ℝ<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => Real.log x ^ n / (a * x + b)) Filter.atTop (𝓝 0)
<VAR>n : ℕ<GOAL>(fun x => Real.log x ^ n) =o[Filter.atTop] id
<VAR>c : ℝ<GOAL>(fun x => c) =o[Filter.atTop] Real.log
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>l : Filter α<VAR>x : ℝ<VAR>h : Filter.Tendsto f l (𝓝 x)<VAR>hx : x ≠ 0<GOAL>Filter.Tendsto (fun x => Real.log (f x)) l (𝓝 (Real.log x))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>hf : Continuous f<VAR>h₀ : ∀ (x : α), f x ≠ 0<GOAL>Continuous fun x => Real.log (f x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>a : α<VAR>hf : ContinuousAt f a<VAR>h₀ : f a ≠ 0<GOAL>ContinuousAt (fun x => Real.log (f x)) a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>a : α<VAR>hf : ContinuousWithinAt f s a<VAR>h₀ : f a ≠ 0<GOAL>ContinuousWithinAt (fun x => Real.log (f x)) s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>h₀ : ∀ x ∈ s, f x ≠ 0<GOAL>ContinuousOn (fun x => Real.log (f x)) s
<VAR>y : ℝ<GOAL>Filter.Tendsto (fun x => Real.log (x + y) - Real.log x) Filter.atTop (𝓝 0)
<GOAL>Filter.Tendsto (fun k => Real.log (↑k + 1) - Real.log ↑k) Filter.atTop (𝓝 0)
<VAR>e : ℝ<VAR>n : ℕ<VAR>h : Mathlib.Meta.NormNum.IsNat e n<GOAL>0 ≤ Real.log e
<VAR>e : ℝ<VAR>n : ℕ<VAR>h : Mathlib.Meta.NormNum.IsNat e n<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>n : ℕ<VAR>h : Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n)<GOAL>0 ≤ Real.log e
<VAR>e : ℝ<VAR>n : ℕ<VAR>h : Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (1 < ↑n / ↑d) = true → 0 < Real.log e
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < -1) = true → 0 < Real.log e
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (0 < ↑n / ↑d) = true → decide (↑n / ↑d < 1) = true → Real.log e ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < 0) = true → decide (-1 < ↑n / ↑d) = true → Real.log e ≠ 0
<VAR>x y : ℝ<VAR>h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨ (∃ k, x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * Real.pi / 2<GOAL>Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)
<VAR>x y : ℝ<VAR>h : (∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2<GOAL>Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)
<VAR>x : ℝ<GOAL>Real.tan (2 * x) = 2 * Real.tan x / (1 - Real.tan x ^ 2)
<VAR>n : ℤ<GOAL>Real.tan (↑n * Real.pi / 2) = 0
<GOAL>ContinuousOn Real.tan {x | Real.cos x ≠ 0}
<GOAL>ContinuousOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
<GOAL>Set.SurjOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) Set.univ
<GOAL>Real.tan '' Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) = Set.univ
<VAR>x : ℝ<GOAL>Real.tan (Real.arctan x) = x
<VAR>x : ℝ<GOAL>Real.arctan x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
<GOAL>Set.range Real.arctan = Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
<VAR>x : ℝ<VAR>hx₁ : -(Real.pi / 2) < x<VAR>hx₂ : x < Real.pi / 2<GOAL>Real.arctan (Real.tan x) = x
<VAR>x : ℝ<GOAL>0 < Real.cos (Real.arctan x)
<VAR>x : ℝ<GOAL>Real.cos (Real.arctan x) ^ 2 = 1 / (1 + x ^ 2)
<VAR>x : ℝ<GOAL>Real.sin (Real.arctan x) = x / √(1 + x ^ 2)
<VAR>x : ℝ<GOAL>Real.cos (Real.arctan x) = 1 / √(1 + x ^ 2)
<VAR>x : ℝ<GOAL>Real.arctan x < Real.pi / 2
<VAR>x : ℝ<GOAL>-(Real.pi / 2) < Real.arctan x
<VAR>x : ℝ<GOAL>Real.arctan x = Real.arcsin (x / √(1 + x ^ 2))
<VAR>x : ℝ<VAR>h : x ∈ Set.Ioo (-1) 1<GOAL>Real.arcsin x = Real.arctan (x / √(1 - x ^ 2))
<VAR>x : ℝ<GOAL>Real.arctan x = 0 ↔ x = 0
<GOAL>Filter.Tendsto Real.arctan Filter.atTop (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2)))
<GOAL>Filter.Tendsto Real.arctan Filter.atBot (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2))))
<VAR>x y : ℝ<VAR>h : Real.tan x = y<VAR>hx : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)<GOAL>Real.arctan y = x
<VAR>x : ℝ<GOAL>Real.arctan (-x) = -Real.arctan x
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>Real.arctan x = Real.arccos (√(1 + x ^ 2))⁻¹
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>Real.arccos x = Real.arctan (√(1 - x ^ 2) / x)
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>Real.arctan x⁻¹ = Real.pi / 2 - Real.arctan x
<VAR>x : ℝ<VAR>h : x < 0<GOAL>Real.arctan x⁻¹ = -(Real.pi / 2) - Real.arctan x
<VAR>x : ℝ<VAR>k : ℤ<GOAL>Real.arctan x ≠ (2 * ↑k + 1) * Real.pi / 2
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>Real.arctan x + Real.arctan y < Real.pi / 2
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y))
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<GOAL>Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y)) + Real.pi
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : x < 0<GOAL>Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y)) - Real.pi
<VAR>x : ℝ<VAR>h₁ : -1 < x<VAR>h₂ : x < 1<GOAL>2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2))
<VAR>x : ℝ<VAR>h : 1 < x<GOAL>2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2)) + Real.pi
<VAR>x : ℝ<VAR>h : x < -1<GOAL>2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2)) - Real.pi
<GOAL>Real.arctan 2⁻¹ + Real.arctan 3⁻¹ = Real.pi / 4
<GOAL>2 * Real.arctan 2⁻¹ - Real.arctan 7⁻¹ = Real.pi / 4
<GOAL>2 * Real.arctan 3⁻¹ + Real.arctan 7⁻¹ = Real.pi / 4
<GOAL>4 * Real.arctan 5⁻¹ - Real.arctan 239⁻¹ = Real.pi / 4
<VAR>x : ℝ<GOAL>ContinuousAt Real.arctan x
<GOAL>↑Real.tanPartialHomeomorph.symm = Real.arctan
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>Real.sin x < x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>Real.sin x ≤ x
<VAR>x : ℝ<VAR>hx : x < 0<GOAL>x < Real.sin x
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>x ≤ Real.sin x
<VAR>x : ℝ<GOAL>1 - x ^ 2 / 2 ≤ Real.cos x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ Real.pi / 2<GOAL>2 / Real.pi * x ≤ Real.sin x
<VAR>x : ℝ<VAR>hx : -(Real.pi / 2) ≤ x<VAR>hx₀ : x ≤ 0<GOAL>Real.sin x ≤ 2 / Real.pi * x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ Real.pi / 2<GOAL>1 - 2 / Real.pi * x ≤ Real.cos x
<VAR>x : ℝ<VAR>hx : |x| ≤ Real.pi<GOAL>Real.cos x ≤ 1 - 2 / Real.pi ^ 2 * x ^ 2
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<GOAL>x - x ^ 3 / 4 < Real.sin x
<VAR>x : ℝ<VAR>h : Real.cos x ≠ 0<GOAL>deriv (fun y => Real.tan y - y) x = 1 / Real.cos x ^ 2 - 1
<VAR>x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < Real.pi / 2<GOAL>x < Real.tan x
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x < Real.pi / 2<GOAL>x ≤ Real.tan x
<VAR>x : ℝ<VAR>hx1 : -(3 * Real.pi / 2) ≤ x<VAR>hx2 : x ≤ 3 * Real.pi / 2<VAR>hx3 : x ≠ 0<GOAL>Real.cos x < 1 / √(x ^ 2 + 1)
<VAR>x : ℝ<VAR>hx1 : -(3 * Real.pi / 2) ≤ x<VAR>hx2 : x ≤ 3 * Real.pi / 2<GOAL>Real.cos x ≤ 1 / √(x ^ 2 + 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : outParam (A → Prop)<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>self : NonUnitalContinuousFunctionalCalculus R p<GOAL>p 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : outParam (A → Prop)<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>self : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<GOAL>p a → ∃ φ, ClosedEmbedding ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a ∧ (∀ (f : C(↑(σₙ R a), R)₀), σₙ R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ R a), R)₀), p (φ f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>self : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<GOAL>CompactSpace ↑(σₙ R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>self : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>s : Set R<VAR>CompactSpace ↑s<VAR>Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : C(↑s, R)₀ →⋆ₙₐ[R] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := h0 }<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>φ ψ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = ψ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ }<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(cfcₙHom ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<GOAL>(cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>σₙ R ((cfcₙHom ha) f) = Set.range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>p ((cfcₙHom ha) f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>φ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A<VAR>hφ₁ : Continuous ⇑φ<VAR>hφ₂ : φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a<GOAL>cfcₙHom ha = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(↑(σₙ R a), R)₀<VAR>f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀<VAR>hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)<VAR>g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀<GOAL>(cfcₙHom ha) (g.comp f') = (cfcₙHom ⋯) g
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfcₙ f a = if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then (cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } else 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ f a = (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a) := by cfc_cont_tac<VAR>hf0 : ∀ (i : ι), f i 0 = 0 := by cfc_zero_tac<GOAL>(fun i => cfcₙ (f i) a) = fun i => (cfcₙHom ha) { toFun := (σₙ R a).restrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)<GOAL>cfcₙ f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : ¬p a<GOAL>cfcₙ f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ¬ContinuousOn f (σₙ R a)<GOAL>cfcₙ f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ¬f 0 = 0<GOAL>cfcₙ f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>(cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>P : A → Prop<VAR>a : A<VAR>f : R → R<VAR>h₀ : P 0<VAR>haf : ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a), P ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := h0 })<GOAL>P (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ id a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => x) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>σₙ R (cfcₙ f a) = f '' σₙ R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<GOAL>p 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>p (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hfg : Set.EqOn f g (σₙ R a)<GOAL>cfcₙ f a = cfcₙ g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>h : cfcₙ f a = cfcₙ g a<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>Set.EqOn f g (σₙ R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ f a = cfcₙ g a ↔ Set.EqOn f g (σₙ R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<GOAL>cfcₙ 0 a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<GOAL>cfcₙ (fun x => 0) a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (fun x => f x * g x) a = cfcₙ f a * cfcₙ g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (fun x => f x + g x) a = cfcₙ f a + cfcₙ g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a) := by cfc_cont_tac<VAR>hf0 : ∀ i ∈ s, f i 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → R → R<VAR>a : A<VAR>hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a) := by cfc_cont_tac<VAR>hf0 : ∀ (i : ι), f i 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (∑ i : ι, f i) a = ∑ i : ι, cfcₙ (f i) a