ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>f₁ f₂ : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>(((mk R M N).compr₂ (map (f₁ + f₂) g)) x✝¹) x✝ = (((mk R M N).compr₂ (map f₁ g + map f₂ g)) x✝¹) x✝
<VAR>α✝ : Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>σ : Perm α<VAR>m n : ℤ<VAR>x : α<GOAL>(σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)
<VAR>R✝ : Type u<VAR>K : Type u'<VAR>M✝ : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι✝ : Type x<VAR>ι' : Type x'<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : Module R✝ M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : Module R✝ M₃<VAR>φ : ι✝ → Type i<VAR>inst✝⁶ : (i : ι✝) → AddCommMonoid (φ i)<VAR>inst✝⁵ : (i : ι✝) → Module R✝ (φ i)<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : CommRing R<VAR>M : ι → Type u_3<VAR>inst✝¹ : (i : ι) → AddCommGroup (M i)<VAR>inst✝ : (i : ι) → Module R (M i)<VAR>x : (i : ι) → M i<GOAL>((lsum R M R) single) x = id x
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>j j' : J<VAR>h : j ≠ j'<GOAL>ι f j ≫ π f j' = 0
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n.pred] ∘ f = f^[n]
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hi : Disjoint x z<VAR>hs : x ⊔ z = y<VAR>h : y ⊓ x = x<GOAL>y ⊓ x ⊓ z = ⊥
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>f : M →* N × P<VAR>x : M<GOAL>(((fst N P).comp f).prod ((snd N P).comp f)) x = f x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x✝ : ↑(P.obj X)<GOAL>(P.map (f ≫ g)) x✝ = ((P.map g).comp (P.map f)) x✝
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Fintype G<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction G R<VAR>x : R<VAR>g : G<VAR>n : ℕ<GOAL>g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p.degree < q.degree<GOAL>p % q = p
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s✝ s t : Set (Sym2 V)<VAR>v w : V<GOAL>(fromEdgeSet (s ∩ t)).Adj v w ↔ (fromEdgeSet s ⊓ fromEdgeSet t).Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s✝ s t : Set (Sym2 V)<VAR>v w : V<GOAL>(s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
<VAR>a : Ordinal.{u_1}<GOAL>a ^ 1 = a
<VAR>a : Ordinal.{u_1}<GOAL>a ^ 0 * a = a
<VAR>f✝ f : Bool → Bool → Bool<VAR>h : autoParam (f false false = false) _auto✝<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(if bit a m = 0 then if f false true = true then bit b n else 0 else if bit b n = 0 then if f true false = true then bit a m else 0 else let n' := bit a m / 2; let m' := bit b n / 2; let b₁ := bit a m % 2 = 1; let b₂ := bit b n % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = bit (f a b) (bitwise f m n)
<VAR>f✝ f : Bool → Bool → Bool<VAR>h : autoParam (f false false = false) _auto✝<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(if (if a = true then 2 * m + 1 else 2 * m) = 0 then if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0 else if (if b = true then 2 * n + 1 else 2 * n) = 0 then if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0 else if f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1)) (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) = true then bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + 1 else bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) = if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
<VAR>f✝ f : Bool → Bool → Bool<VAR>h : autoParam (f false false = false) _auto✝<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h2 : ∀ (x : ℕ), (x + x + 1) % 2 = 1<GOAL>(if (if a = true then 2 * m + 1 else 2 * m) = 0 then if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0 else if (if b = true then 2 * n + 1 else 2 * n) = 0 then if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0 else if f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1)) (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) = true then bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + 1 else bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) = if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
<VAR>f✝ f : Bool → Bool → Bool<VAR>h : autoParam (f false false = false) _auto✝<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h2 : ∀ (x : ℕ), (x + x + 1) % 2 = 1<VAR>h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x<GOAL>(if (if a = true then 2 * m + 1 else 2 * m) = 0 then if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0 else if (if b = true then 2 * n + 1 else 2 * n) = 0 then if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0 else if f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1)) (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) = true then bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + 1 else bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) + bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) = if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source<VAR>x : X<VAR>hx✝ : x ∈ s<VAR>e : PartialHomeomorph X Y<VAR>hx : x ∈ e.source<VAR>he : Set.EqOn f (↑e) e.source<GOAL>∃ e, x ∈ e.source ∧ f = ↑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<GOAL>∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<VAR>hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i<GOAL>∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>a /. b ≤ c /. d ↔ a * d ≤ c * b
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
<VAR>x : ℝ<VAR>h : cos x = 0<GOAL>deriv tan x = 1 / cos x ^ 2
<VAR>x : ℝ<VAR>h : cos x = 0<VAR>this : ¬DifferentiableAt ℝ tan x<GOAL>deriv tan x = 1 / cos x ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<GOAL>MeasurableSet {a | IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<GOAL>MeasurableSet {a | IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<GOAL>MeasurableSet {a | IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<VAR>h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}<GOAL>MeasurableSet {a | IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<VAR>h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}<VAR>h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}<GOAL>MeasurableSet {a | IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<VAR>h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}<VAR>h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}<GOAL>{a | IsRatStieltjesPoint f a} = {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩ {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<VAR>h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}<VAR>h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}<VAR>a : α<GOAL>a ∈ {a | IsRatStieltjesPoint f a} ↔ a ∈ {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩ {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>h1 : MeasurableSet {a | Monotone (f a)}<VAR>h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}<VAR>h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}<VAR>h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}<VAR>a : α<GOAL>IsRatStieltjesPoint f a ↔ ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t
<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>m n : PosNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ : G<GOAL>x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ : G<GOAL>(∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (g : G), g * x✝ = x✝ * g
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>(p * X ^ n).natTrailingDegree = p.natTrailingDegree + n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>(p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hvw : M.Adj v w<GOAL>h.toEdge ⟨v, hv⟩ = ⟨s(v, w), hvw⟩
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hvw : M.Adj v w<GOAL>s(v, Exists.choose ⋯) = s(v, w)
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hvw : M.Adj v w<GOAL>Exists.choose ⋯ = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>h : Periodic f c<VAR>hc : c ≠ 0<VAR>a : α<GOAL>f '' uIcc a (a + c) = range f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<GOAL>(sesqFormOfInner (A x)) y = (sesqFormOfInner x) ((adjoint A) y)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.natTrailingDegree = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f = 0 ∨ f ≠ 0
<VAR>n a b : ℕ<VAR>ha' : 1 < a<VAR>hb' : 1 < b<VAR>hab : a.Coprime b<VAR>ha : ∑ i ∈ a.divisors, Λ i = Real.log ↑a<VAR>hb : ∑ i ∈ b.divisors, Λ i = Real.log ↑b<GOAL>∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)
<VAR>n a b : ℕ<VAR>ha' : 1 < a<VAR>hb' : 1 < b<VAR>hab : a.Coprime b<VAR>ha : ∑ a ∈ filter IsPrimePow a.divisors, Real.log ↑a.minFac = Real.log ↑a<VAR>hb : ∑ a ∈ filter IsPrimePow b.divisors, Real.log ↑a.minFac = Real.log ↑b<GOAL>∑ a ∈ filter IsPrimePow (a * b).divisors, Real.log ↑a.minFac = Real.log ↑(a * b)
<VAR>R✝ : Type u_1<VAR>inst✝³ : AddMonoidWithOne R✝<VAR>inst✝² : CharZero R✝<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CharZero R<VAR>q n : ℕ<VAR>hn : n ≠ 0<GOAL>↑q ^ n = 1 ↔ q = 1
<VAR>R✝ : Type u_1<VAR>inst✝³ : AddMonoidWithOne R✝<VAR>inst✝² : CharZero R✝<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CharZero R<VAR>q n : ℕ<VAR>hn : n ≠ 0<GOAL>q ^ n = 1 ↔ q = 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>hi : i ∉ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<VAR>j : ι<VAR>hj : j ∈ s<GOAL>t j (update f i a j) = t j (f j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>hi : i ∉ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<VAR>j : ι<VAR>hj : j ∈ s<GOAL>j ≠ i
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<GOAL>finInsepDegree F ↥⊤ = finInsepDegree F K
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Fintype ι<GOAL>¬LinearIndependent R v ↔ ∃ g, ∑ i : ι, g i • v i = 0 ∧ ∃ i, g i ≠ 0
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<GOAL>lift.{v', v} (Module.rank R S) = lift.{v, v'} (Module.rank R' S')
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<VAR>this : ((algebraMap R' S').comp i.toRingHom) r = (j.toRingHom.comp (algebraMap R S)) r<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<VAR>this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<GOAL>ClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>ClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>Filter.comap (fun x => (↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.1, ↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.2)) (𝓤 C(↑(spectrum R a), R)) = 𝓤 C(↑(σₙ R a), R)₀
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<VAR>this : inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) = UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance<GOAL>Filter.comap (fun x => (↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.1, ↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.2)) (𝓤 C(↑(spectrum R a), R)) = 𝓤 C(↑(σₙ R a), R)₀