ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<GOAL>sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<GOAL>{a | (μ.restrict s) {x | a < f x} = 0} ⊆ {a | μ {x | a < f x} = 0}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<VAR>a : ℝ≥0∞<VAR>ha : (μ.restrict s) {x | a < f x} = 0<GOAL>a ∈ {a | μ {x | a < f x} = 0}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<VAR>a : ℝ≥0∞<VAR>ha : μ ({x | a < f x} ∩ s) = 0<GOAL>a ∈ {a | μ {x | a < f x} = 0}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<VAR>a : ℝ≥0∞<VAR>ha : μ ({x | a < f x} ∩ s) = 0<GOAL>∀ (g : G), g • {x | a < f x} = {x | a < f x}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<VAR>a : ℝ≥0∞<VAR>ha : μ ({x | a < f x} ∩ s) = 0<VAR>γ : G<VAR>x : α<GOAL>x ∈ γ • {x | a < f x} ↔ x ∈ {x | a < f x}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<VAR>a : ℝ≥0∞<VAR>ha : μ ({x | a < f x} ∩ s) = 0<VAR>γ : G<VAR>x : α<GOAL>γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}
<VAR>n a p k : ℕ<VAR>pp : Prime p<VAR>h₁ : ¬a ∣ p ^ k<VAR>h₂ : a ∣ p ^ (k + 1)<GOAL>a = p ^ (k + 1)
<VAR>n p k : ℕ<VAR>pp : Prime p<VAR>l : ℕ<VAR>h : l ≤ k + 1<VAR>h₁ : ¬p ^ l ∣ p ^ k<VAR>h₂ : p ^ l ∣ p ^ (k + 1)<GOAL>p ^ l = p ^ (k + 1)
<VAR>n p k : ℕ<VAR>pp : Prime p<VAR>l : ℕ<VAR>h : l ≤ k + 1<VAR>h₁ : ¬p ^ l ∣ p ^ k<VAR>h₂ : p ^ l ∣ p ^ (k + 1)<GOAL>l = k + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p q : α × β<GOAL>p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>a✝ : ℕ<VAR>h : t.chainHeight = ↑a✝<GOAL>(s ∪ t).chainHeight = s.chainHeight + ↑a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>a✝ : ℕ<VAR>h : t.chainHeight = ↑a✝<GOAL>(s ∪ t).chainHeight ≤ s.chainHeight + ↑a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>a✝ : ℕ<VAR>h : t.chainHeight = ↑a✝<GOAL>s.chainHeight + ↑a✝ ≤ (s ∪ t).chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>a✝ : ℕ<VAR>h : t.chainHeight = ↑a✝<GOAL>∀ l ∈ s.subchain, ∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>a✝ : ℕ<VAR>h : t.chainHeight = ↑a✝<VAR>l : List α<VAR>hl : l ∈ s.subchain<GOAL>∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>l : List α<VAR>hl : l ∈ s.subchain<VAR>l' : List α<VAR>hl' : l' ∈ t.subchain<VAR>h : t.chainHeight = ↑l'.length<GOAL>∃ l'_1 ∈ (s ∪ t).subchain, l.length + l'.length ≤ l'_1.length + 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>l : List α<VAR>hl : l ∈ s.subchain<VAR>l' : List α<VAR>hl' : l' ∈ t.subchain<VAR>h : t.chainHeight = ↑l'.length<VAR>x : α<VAR>hx : x ∈ l.getLast?<VAR>y : α<VAR>hy : y ∈ l'.head?<GOAL>x < y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<VAR>l : List α<VAR>hl : l ∈ s.subchain<VAR>l' : List α<VAR>hl' : l' ∈ t.subchain<VAR>h : t.chainHeight = ↑l'.length<VAR>i : α<VAR>hi : i ∈ l ++ l'<GOAL>i ∈ s ∪ t
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>(h.coeffs (lc e l)) i = l i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<GOAL>(fun x => !x) ∘ isSome = isNone
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>x✝ : Option α<GOAL>((fun x => !x) ∘ isSome) x✝ = x✝.isNone
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : Mul α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : DistribMulAction R α<VAR>inst✝ : IsScalarTower R α α<VAR>x : R<VAR>v w : m → α<GOAL>x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β✝<VAR>β : Type u_6<VAR>i : Finset β<VAR>f : β → Multiset α<VAR>a : Multiset α<GOAL>a.Disjoint (i.sum f) ↔ ∀ b ∈ i, a.Disjoint (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>b : β<VAR>x y : α<GOAL>edist ((fun x => b) x) ((fun x => b) y) ≤ ↑0 * edist x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<VAR>hfc : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' frontier s = frontier (f ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>I : ι → FractionalIdeal R⁰ K<VAR>hS : ∀ i ∈ s, I i ≠ 0<GOAL>count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>ι : Type u_3<VAR>I : ι → FractionalIdeal R⁰ K<VAR>hS : ∀ i ∈ ∅, I i ≠ 0<GOAL>count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>ι : Type u_3<VAR>I : ι → FractionalIdeal R⁰ K<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)<VAR>hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0<GOAL>count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a b : G<GOAL>x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a b x✝ : G<GOAL>(x /ᵒᶠ (a + b)) x✝ = (x /ᵒᶠ a /ᵒᶠ b) x✝
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>x✝ : ↑n ≠ -1<GOAL>A ^ (↑n + 1) = A ^ ↑n * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>x✝ : -(↑n + 2) ≠ -1<GOAL>A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>x✝ : -(↑n + 2) ≠ -1<VAR>h : A⁻¹ * A = 1<VAR>right✝ : A * A⁻¹ = 1<GOAL>A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>x✝ : -(↑n + 2) ≠ -1<VAR>h : A⁻¹ = 0<GOAL>A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>R : Type u_2<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : Fintype Mˣ<VAR>χ : MulChar M R<VAR>a✝ : Mˣ<GOAL>(χ ^ Fintype.card Mˣ) ↑a✝ = 1 ↑a✝
<VAR>a c : ℕ<GOAL>a.choose c ≤ a.succ.choose c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>c : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c<VAR>hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A<GOAL>Convex 𝕜 (⋃₀ c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>c : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c<VAR>hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A<GOAL>Convex 𝕜 (⋃ i, ↑i)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>a * ↑r = r • a
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>LSeriesSummable (f - g) s
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : NormalSpace α<VAR>inst✝¹⁰ : R1Space α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedAlgebra ℝ 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : IsFiniteMeasure μ<GOAL>DenseRange ⇑(toLp p μ 𝕜)
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : NormalSpace α<VAR>inst✝¹⁰ : R1Space α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedAlgebra ℝ 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : IsFiniteMeasure μ<GOAL>range ⇑(BoundedContinuousFunction.toLp p μ 𝕜) ⊆ range ⇑(toLp p μ 𝕜)
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : NormalSpace α<VAR>inst✝¹⁰ : R1Space α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedAlgebra ℝ 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>(BoundedContinuousFunction.toLp p μ 𝕜) f ∈ range ⇑(toLp p μ 𝕜)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<GOAL>(affineCombination k s p₁) w₁ = (affineCombination k s p₂) w₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : DecidableEq ι<VAR>I : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>J : Finset ι<VAR>f : (i : ι) → α i<GOAL>f ∈ cylinder I S ↔ f ∈ cylinder (I ∪ J) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>inst✝⁴ : NonAssocSemiring R<VAR>inst✝³ : NonAssocSemiring S<VAR>inst✝² : NonAssocSemiring R'<VAR>inst✝¹ : NonAssocSemiring S'<VAR>inst✝ : Subsingleton S<VAR>fst✝ : R<VAR>snd✝ : S<GOAL>(fun x => (x, 0)) (fst✝, snd✝).1 = (fst✝, snd✝)
<VAR>z : ℍ<GOAL>‖cexp (2 * ↑π * Complex.I * ↑z)‖ < 1
<VAR>z : ℍ<GOAL>0 < 2 * π * z.im
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : BijOn f s ∅<GOAL>s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>BijOn f ∅ ∅
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>neg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>p a ha
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>neg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∃ (x : a ∈ closure s), p a x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>neg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∀ (x y : R), (∃ (x_1 : x ∈ closure s), p x x_1) → (∃ (x : y ∈ closure s), p y x) → ∃ (x_1 : x + y ∈ closure s), p (x + y) x_1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>neg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∀ (x y : R), (∃ (x_1 : x ∈ closure s), p x x_1) → (∃ (x : y ∈ closure s), p y x) → ∃ (x_1 : x * y ∈ closure s), p (x * y) x_1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F) (-2) = χ₈' ↑(Fintype.card F)
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>x : ℕ<GOAL>bit a x % 2 = if a = true then 1 else 0
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>x : ℕ<GOAL>(if a = true then 2 * x + 1 else 2 * x) % 2 = if a = true then 1 else 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>x y : FreeAlgebra R M<VAR>h : Rel R M x y<GOAL>((FreeAlgebra.lift R) ⇑f) x = ((FreeAlgebra.lift R) ⇑f) y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<GOAL>(fun F => F.toLinearMap ∘ₗ ι R) ((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) f) = f
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<GOAL>(fun F => F.toLinearMap ∘ₗ { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }) ((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) f) = f
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>x : M<GOAL>((fun F => F.toLinearMap ∘ₗ { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }) ((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) f)) x = f x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>F : TensorAlgebra R M →ₐ[R] A<VAR>x : M<GOAL>(⇑(((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) ((fun F => F.toLinearMap ∘ₗ ι R) F)).comp (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x = (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>F : TensorAlgebra R M →ₐ[R] A<VAR>x : M<GOAL>(⇑(((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) ((fun F => F.toLinearMap ∘ₗ { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }) F)).comp (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x = (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>H : ¬1 = 0<VAR>n : ℕ<GOAL>(X ^ n).support = {n}
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>H : ¬1 = 0<VAR>n : ℕ<GOAL>X ^ n = (monomial n) 1
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖fun i => (WithLp.equiv 1 (n → α)).symm (A i)‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : CommRing 𝕜<VAR>inst✝⁴ : PartialOrder 𝕜<VAR>inst✝³ : StarRing 𝕜<VAR>inst✝² : StarOrderedRing 𝕜<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>(Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : CommRing 𝕜<VAR>inst✝⁴ : PartialOrder 𝕜<VAR>inst✝³ : StarRing 𝕜<VAR>inst✝² : StarOrderedRing 𝕜<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>hBAB : (Bᴴ * A⁻¹ * B).IsHermitian<GOAL>(Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : CommRing 𝕜<VAR>inst✝⁴ : PartialOrder 𝕜<VAR>inst✝³ : StarRing 𝕜<VAR>inst✝² : StarOrderedRing 𝕜<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>hBAB : (Bᴴ * A⁻¹ * B).IsHermitian<GOAL>A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>R' : Type v<VAR>inst✝ : CommMonoid R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<VAR>a b : R<VAR>h : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)<GOAL>a = b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>R' : Type v<VAR>inst✝ : CommMonoid R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<VAR>a b : R<VAR>h : ψ.mulShift (a + -b) = 1<GOAL>a = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>IsLocalization ((toSpec 𝒜 f).val.base x).asIdeal.primeCompl (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)