ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<GOAL>(IsInternal fun i => A ↑i) ↔ IsInternal A
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<GOAL>(CompleteLattice.Independent fun i => A ↑i) ∧ ⨆ i, A ↑i = ⊤ ↔ CompleteLattice.Independent A ∧ iSup A = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v w : V<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<GOAL>mk K v hv = mk K w hw ↔ ∃ a, a • w = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v w : V<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<GOAL>(∃ a, a • w = v) ↔ ∃ a, a • w = v
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<GOAL>S.disconnect.IsTotallyDisconnected
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<GOAL>∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>n : ℕ<GOAL>(fun x => x ^ n) '' σ a ⊆ σ (a ^ n)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<GOAL>a ^ 3 = a * (a * a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>(convexHull R) s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>basicOpen f ≤ basicOpen g ↔ f ∈ (Ideal.span {g}).radical
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a✝ : α<VAR>m n✝ : ℕ<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>r : ℝ<VAR>hr : Tendsto (fun n => ∑ i ∈ Finset.range n, |f i|) atTop (𝓝 r)<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>r : ℝ<VAR>hr : Tendsto (fun n => ∑ i ∈ Finset.range n, |f i|) atTop (𝓝 r)<GOAL>∀ (i : ℕ), 0 ≤ ‖f i‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>r : ℝ<VAR>hr : Tendsto (fun n => ∑ i ∈ Finset.range n, |f i|) atTop (𝓝 r)<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, ‖f i‖) atTop (𝓝 r)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.v p q hpq
<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>hf : LeftInvOn f' f s<GOAL>f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
<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>hf : LeftInvOn f' f s<GOAL>f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s
<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>hf : LeftInvOn f' f s<GOAL>f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<GOAL>↑(toSimpleFunc (posPart (-f))) =ᶠ[ae μ] ↑(-toSimpleFunc f).posPart
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<GOAL>∀ (a : α), ↑(toSimpleFunc (posPart (-f))) a = ↑(toSimpleFunc (-f)).posPart a → ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a → ↑(toSimpleFunc (posPart (-f))) a = ↑(-toSimpleFunc f).posPart a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G✝ : Type u_4<VAR>inst✝¹² : Mul G✝<VAR>inst✝¹¹ : TopologicalSpace G✝<VAR>inst✝¹⁰ : ChartedSpace H G✝<VAR>inst✝⁹ : SmoothMul I G✝<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H' M<VAR>g✝ h✝ : G✝<VAR>G : Type u_8<VAR>inst✝³ : Semigroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : ChartedSpace H G<VAR>inst✝ : SmoothMul I G<VAR>g h x✝ : G<GOAL>(𝑹 I (g * h)) x✝ = ((𝑹 I h).comp (𝑹 I g)) x✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp : 0 ≠ ⊤<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) 0 μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<VAR>hp₀' : 0 ≤ 1 / p.toReal<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<VAR>hp₀' : 0 ≤ 1 / p.toReal<VAR>hp₀'' : 0 < p.toReal<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<VAR>hp₀' : 0 ≤ 1 / p.toReal<VAR>hp₀'' : 0 < p.toReal<VAR>η : ℝ≥0<VAR>hη_pos : 0 < η<VAR>hη_le : ↑‖c‖₊ * ↑η ^ (1 / p.toReal) ≤ ε<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<VAR>hp₀' : 0 ≤ 1 / p.toReal<VAR>hp₀'' : 0 < p.toReal<VAR>η : ℝ≥0<VAR>hη_pos : 0 < η<VAR>hη_le : ↑‖c‖₊ * ↑η ^ (1 / p.toReal) ≤ ε<VAR>s : Set α<VAR>hs : μ s ≤ ↑η<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ : Set α<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h'p : p ≠ 0<VAR>hp₀ : 0 < p<VAR>hp₀' : 0 ≤ 1 / p.toReal<VAR>hp₀'' : 0 < p.toReal<VAR>η : ℝ≥0<VAR>hη_pos : 0 < η<VAR>hη_le : ↑‖c‖₊ * ↑η ^ (1 / p.toReal) ≤ ε<VAR>s : Set α<VAR>hs : μ s ≤ ↑η<GOAL>↑‖c‖₊ * μ s ^ (1 / p.toReal) ≤ ↑‖c‖₊ * ↑η ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → E<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in s, g x ∂μ
<VAR>l₁ l₂ : List Nat<GOAL>Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂
<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>f : ι → Y<VAR>l : Filter ι<VAR>y : Y<VAR>hg : Inducing g<GOAL>Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p k : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>eval 1 (cyclotomic (p ^ (k + 1)) R) = ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Infinite α<VAR>inst✝ : Finite β<VAR>f : α → β<GOAL>∃ y, Infinite ↑(f ⁻¹' {y})
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U<GOAL>T1Space G
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U<VAR>x y : G<VAR>hspec : x ⤳ y<VAR>hne : ¬x = y<GOAL>False
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U<VAR>x y : G<VAR>hspec : x ⤳ y<VAR>hne : ¬x = y<VAR>U : Set G<VAR>hU₁ : U ∈ 𝓝 1<VAR>hU : x * y⁻¹ ∉ U<GOAL>False
<VAR>q : ℚ<GOAL>0 ≤ q.num ↔ 0 ≤ q
<VAR>q : ℚ<GOAL>0 < q.num ∨ 0 = q.num → ¬q = 0 → q.num < 0 ∨ q = 0 → 0 < q.num ∨ 0 = q.num
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>⨆ i, ⨆ (_ : p i), S i = AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>⨆ i, ⨆ (_ : p i), S i ≤ AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) ≤ ⨆ i, ⨆ (_ : p i), S i
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>L R : ListBlank Γ<GOAL>trTape enc0 (Tape.mk' L R) = trTape' enc0 L R
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Monoid M<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : DistribMulAction M E<VAR>inst✝ : Bornology M<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>h₁ : Absorbs M s₁ t₁<VAR>h₂ : Absorbs M s₂ t₂<GOAL>Absorbs M (s₁ - s₂) (t₁ - t₂)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasCoequalizer f g<VAR>inst✝ : HasCoequalizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<GOAL>G.map f ≫ G.map h = G.map g ≫ G.map h
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasCoequalizer f g<VAR>inst✝ : HasCoequalizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<GOAL>coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasCoequalizer f g<VAR>inst✝ : HasCoequalizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<GOAL>coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) ⋯
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>t : (ZMod ↑n)ˣ<GOAL>minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K ⋯).gen
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>t : (ZMod ↑n)ˣ<VAR>this : NeZero ↑↑n<GOAL>minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K ⋯).gen
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>t : (ZMod ↑n)ˣ<VAR>this : NeZero ↑↑n<GOAL>minpoly K (zeta n K L) = minpoly K (zeta n K L ^ (↑t).val)
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>t : (ZMod ↑n)ˣ<VAR>this : NeZero ↑↑n<VAR>hr : cyclotomic (↑n) K = minpoly K (zeta n K L ^ (↑t).val)<GOAL>minpoly K (zeta n K L) = minpoly K (zeta n K L ^ (↑t).val)
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>(fun t => (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) ((↑__src✝).toFun f) = f
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>(IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯ = f
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>↑((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) = ↑f
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>↑((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) (IsPrimitiveRoot.powerBasis K hζ).gen = ↑f (IsPrimitiveRoot.powerBasis K hζ).gen
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) (IsPrimitiveRoot.powerBasis K hζ).gen = f (IsPrimitiveRoot.powerBasis K hζ).gen
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>f : L ≃ₐ[K] L<GOAL>(IsPrimitiveRoot.powerBasis K ⋯).gen = f (IsPrimitiveRoot.powerBasis K hζ).gen
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<GOAL>(↑__src✝).toFun ((fun t => (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) x) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<GOAL>(IsPrimitiveRoot.autToPow K ⋯) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x