ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ⟂ₘ μ<VAR>A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a<VAR>u : ℕ → ℝ≥0<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>z : ℝ≥0∞<VAR>hz : z > 0<VAR>w : ℝ≥0<VAR>w_pos : 0 < ↑w<VAR>w_lt : ↑w < z<VAR>n : ℕ<VAR>hn : u n < w<VAR>a : Set α<VAR>ha : ρ a < ↑(u n) * μ a<VAR>μa_pos : 0 < μ a<VAR>μa_lt_top : μ a < ⊤<GOAL>ρ a / μ a < z
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ⟂ₘ μ<VAR>A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a<VAR>u : ℕ → ℝ≥0<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>z : ℝ≥0∞<VAR>hz : z > 0<VAR>w : ℝ≥0<VAR>w_pos : 0 < ↑w<VAR>w_lt : ↑w < z<VAR>n : ℕ<VAR>hn : u n < w<VAR>a : Set α<VAR>ha : ρ a < ↑(u n) * μ a<VAR>μa_pos : 0 < μ a<VAR>μa_lt_top : μ a < ⊤<GOAL>ρ a < z * μ a
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<VAR>hf : Injective ⇑f<GOAL>((map f) p).degrees = p.degrees
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<GOAL>IntegrableAtFilter f ⊤ μ ↔ Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h : IntegrableAtFilter f ⊤ μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>s : Set α<VAR>hsf : s ∈ ⊤<VAR>hs : IntegrableOn f s μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>r : ℝ<VAR>hr : r < 0<GOAL>(r • j).negPart = (-r).toNNReal • j.posPart
<VAR>n : ℕ<VAR>R : Type u_1<VAR>hpos : 0 < n<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>0 < (cyclotomic n R).degree
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>gauge s x = 1 ↔ x ∈ frontier s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>x ∈ closure s ∧ x ∉ interior s ↔ x ∈ frontier s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>a b : α<VAR>hab : a < b<GOAL>a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>a b : α<VAR>hab : a < b<VAR>hmem : h.min (Set.Ioc a b) ⋯ ∈ Set.Ioc a b<GOAL>a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_8, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D<VAR>inst✝² : Category.{?u.10794, u_4} D₁<VAR>inst✝¹ : Category.{?u.10798, u_5} D₂<VAR>L₁ : C₁ ⥤ D<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D<VAR>W₂ : MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<VAR>inst✝ : L₁.IsLocalization W₁<VAR>iso : E.functor ⋙ L₂ ≅ L₁<GOAL>L₂.IsLocalization W₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_8, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D<VAR>inst✝² : Category.{?u.10794, u_4} D₁<VAR>inst✝¹ : Category.{?u.10798, u_5} D₂<VAR>L₁ : C₁ ⥤ D<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D<VAR>W₂ : MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<VAR>inst✝ : L₁.IsLocalization W₁<VAR>iso : E.functor ⋙ L₂ ≅ L₁<VAR>h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)<GOAL>L₂.IsLocalization W₂
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>hn : n ∈ p.smoothNumbers<GOAL>p.Coprime n
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>hn : n ∈ factoredNumbers (Finset.range p)<GOAL>p.Coprime n
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>eval (C L * (X - C x) + C y) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) = -(C { a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.a * X ^ 3 + C { a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.b * X ^ 2 + C { a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.c * X + C { a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.d)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>(C L * (X - C x) + C y) ^ 2 + (C W.a₁ * X + C W.a₃) * (C L * (X - C x) + C y) - (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) = -(C 1 * X ^ 3 + C (-L ^ 2 - W.a₁ * L + W.a₂) * X ^ 2 + C (2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄)) * X + C (-x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆)))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>(C L * (X - C x) + C y) ^ 2 + (C W.a₁ * X + C W.a₃) * (C L * (X - C x) + C y) - (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) = -(1 * X ^ 3 + (-C L ^ 2 - C W.a₁ * C L + C W.a₂) * X ^ 2 + (2 * C x * C L ^ 2 + (C W.a₁ * C x - 2 * C y - C W.a₃) * C L + (-C W.a₁ * C y + C W.a₄)) * X + (-C x ^ 2 * C L ^ 2 + (2 * C x * C y + C W.a₃ * C x) * C L - (C y ^ 2 + C W.a₃ * C y - C W.a₆)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>g : β ≃ₜ γ<GOAL>f.symm.toContinuousMap.comp f.toContinuousMap = ContinuousMap.id α
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>heX : e ∈ X<VAR>h : autoParam (e ∈ M.E) _auto✝<GOAL>e ∈ M.closure X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>heX : e ∈ X<VAR>h : autoParam (e ∈ M.E) _auto✝<GOAL>e ∈ M.closure (X ∩ M.E)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<GOAL>(coeff R n) (inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<GOAL>(if single () n = 0 then a else -a * ∑ x ∈ antidiagonal (single () n), if x.2 < single () n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0) = if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<GOAL>(if n = 0 then a else -a * ∑ x ∈ antidiagonal (single () n), if x.2 < single () n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0) = if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>(∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0) = ∑ x ∈ antidiagonal (single () n), if x.2 < single () n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>∀ a ∈ antidiagonal n, (match a with | (a, b) => (single () a, single () b)) ∈ antidiagonal (single () n)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>∀ a ∈ antidiagonal (single () n), (match a with | (f, g) => (f (), g ())) ∈ antidiagonal n
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>∀ a ∈ antidiagonal n, (match match a with | (a, b) => (single () a, single () b) with | (f, g) => (f (), g ())) = a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>∀ a ∈ antidiagonal (single () n), (match match a with | (f, g) => (f (), g ()) with | (a, b) => (single () a, single () b)) = a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : R⟦X⟧<VAR>h✝ : ¬n = 0<GOAL>∀ a_1 ∈ antidiagonal n, (if a_1.2 < n then (coeff R a_1.1) φ * (coeff R a_1.2) (MvPowerSeries.inv.aux a φ) else 0) = if (match a_1 with | (a, b) => (single () a, single () b)).2 < single () n then (MvPowerSeries.coeff R (match a_1 with | (a, b) => (single () a, single () b)).1) φ * (MvPowerSeries.coeff R (match a_1 with | (a, b) => (single () a, single () b)).2) (MvPowerSeries.inv.aux a φ) else 0
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>hfg : ConvolutionExists f g L μ<VAR>hfg' : ConvolutionExists f' g L μ<VAR>x : G<GOAL>((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<VAR>this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<VAR>this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup<VAR>m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<VAR>this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup<VAR>m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hm : (M.mulRightMap n) m = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<VAR>this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup<VAR>m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hm : m = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hn : LinearIndependent R n<VAR>this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup<VAR>m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hm : b = 0 ∧ a = 0<GOAL>False
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f g : α → β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᶠ[ae (μ.restrict s)] f
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f g : α → β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 s] f
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-x ≤ 0 ↔ 0 ≤ x
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : DecidableEq F<GOAL>(primitiveChar_to_Complex F).IsPrimitive
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : DecidableEq F<GOAL>Function.Injective ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : DecidableEq F<VAR>nn : ℕ+ := (primitiveChar F ℂ ⋯).n<GOAL>Function.Injective ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : F<VAR>hf : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => c - f x) (-f') x L
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>f : E →ₗᵢ[𝕜] E'<VAR>x y : E<GOAL>⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>e.trans e.symm ≈ ofSet e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>A : (e.trans e.symm).source = e.source<GOAL>e.trans e.symm ≈ ofSet e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>A : (e.trans e.symm).source = e.source<VAR>x : α<VAR>hx : x ∈ (e.trans e.symm).source<GOAL>↑(e.trans e.symm) x = ↑(ofSet e.source) x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>IsOpen {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>∀ x ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}, {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>x : α<VAR>n : Set α<VAR>ns : n ∈ 𝓝[s] x<VAR>hx : μ n = 0<GOAL>{x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>x : α<VAR>n : Set α<VAR>ns : n ∈ 𝓝[s] x<VAR>hx : μ n = 0<VAR>v : Set α<VAR>vx : v ∈ 𝓝 x<VAR>hv : v ∩ s ⊆ n<GOAL>{x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>x : α<VAR>n : Set α<VAR>ns : n ∈ 𝓝[s] x<VAR>hx : μ n = 0<VAR>v : Set α<VAR>vx : v ∈ 𝓝 x<VAR>hv : v ∩ s ⊆ n<VAR>w : Set α<VAR>wv : w ⊆ v<VAR>w_open : IsOpen w<VAR>xw : x ∈ w<GOAL>{x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>x : α<VAR>n : Set α<VAR>ns : n ∈ 𝓝[s] x<VAR>hx : μ n = 0<VAR>v : Set α<VAR>vx : v ∈ 𝓝 x<VAR>hv : v ∩ s ⊆ n<VAR>w : Set α<VAR>wv : w ⊆ v<VAR>w_open : IsOpen w<VAR>xw : x ∈ w<VAR>A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}<GOAL>{x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>x : α<VAR>n : Set α<VAR>ns : n ∈ 𝓝[s] x<VAR>hx : μ n = 0<VAR>v : Set α<VAR>vx : v ∈ 𝓝 x<VAR>hv : v ∩ s ⊆ n<VAR>w : Set α<VAR>wv : w ⊆ v<VAR>w_open : IsOpen w<VAR>xw : x ∈ w<VAR>A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}<VAR>B : w ∈ 𝓝 x<GOAL>{x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>m n : α<VAR>hm : IsPrimal m<VAR>hn : IsPrimal n<GOAL>IsPrimal (m * n)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>n : α<VAR>hn : IsPrimal n<VAR>hm : IsPrimal 0<GOAL>IsPrimal (0 * n)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>m n : α<VAR>hm : IsPrimal m<VAR>hn : IsPrimal n<VAR>h0 : m ≠ 0<GOAL>IsPrimal (m * n)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>m n : α<VAR>hm : IsPrimal m<VAR>hn : IsPrimal n<VAR>h0 : m ≠ 0<VAR>b c : α<VAR>h : m * n ∣ b * c<GOAL>∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>n : α<VAR>hn : IsPrimal n<VAR>a₁ a₂ b c : α<VAR>hm : IsPrimal (a₁ * a₂)<VAR>h0 : a₁ * a₂ ≠ 0<VAR>h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)<GOAL>∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>n : α<VAR>hn : IsPrimal n<VAR>a₁ a₂ b c : α<VAR>hm : IsPrimal (a₁ * a₂)<VAR>h0 : a₁ * a₂ ≠ 0<VAR>h : n ∣ b * c<GOAL>∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a₁ a₂ b c : α<VAR>hm : IsPrimal (a₁ * a₂)<VAR>h0 : a₁ * a₂ ≠ 0<VAR>a₁' a₂' : α<VAR>h₁ : a₁' ∣ b<VAR>h₂ : a₂' ∣ c<VAR>hn : IsPrimal (a₁' * a₂')<VAR>h : a₁' * a₂' ∣ b * c<GOAL>∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>s t : Set σ<VAR>p : MvPolynomial σ R<GOAL>p ∈ supported R ↑p.vars
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : s ≠ 1<GOAL>riemannZeta (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * riemannZeta s
<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>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<GOAL>AffineIndependent k 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>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<VAR>h : IsEmpty ι<GOAL>AffineIndependent k 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>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<VAR>h : Nonempty ι<GOAL>AffineIndependent k 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>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<VAR>i : ι<GOAL>AffineIndependent k p