ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b✝ : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<VAR>a b : α<GOAL>map f ↑a ≤ map f ↑b ↔ ↑a ≤ ↑b
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b c : α<VAR>inst✝ : Invertible c<GOAL>a * c = b ↔ a = b * ⅟c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<GOAL>projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a
<VAR>p : ℝ[X]<GOAL>∑ x ∈ p.roots.toFinset, (Multiset.count x p.roots - 1 + 1) = ∑ x ∈ p.roots.toFinset, (rootMultiplicity x p - 1) + p.roots.toFinset.card
<VAR>p : ℝ[X]<GOAL>∑ x ∈ p.roots.toFinset, rootMultiplicity x (derivative p) + (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots + (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)
<VAR>p : ℝ[X]<GOAL>∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots + (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots + (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)
<VAR>p : ℝ[X]<GOAL>∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, 1 ≤ ∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots
<VAR>p : ℝ[X]<VAR>x : ℝ<VAR>hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset<GOAL>0 < Multiset.count x (derivative p).roots
<VAR>p : ℝ[X]<VAR>x : ℝ<VAR>hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset<GOAL>x ∈ (derivative p).roots.toFinset
<VAR>p : ℝ[X]<GOAL>∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots + (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1) = Multiset.card (derivative p).roots + 1
<VAR>p : ℝ[X]<GOAL>∀ x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset, x ∉ (derivative p).roots.toFinset → Multiset.count x (derivative p).roots = 0
<VAR>p : ℝ[X]<VAR>x : ℝ<VAR>a✝ : x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset<VAR>hx₂ : x ∉ (derivative p).roots.toFinset<GOAL>Multiset.count x (derivative p).roots = 0
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : NormalWord d<GOAL>(base φ) h • w = h • w
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : StrongRankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : (α →₀ R) →ₗ[R] β →₀ R<VAR>i : Injective ⇑f<VAR>P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β<VAR>Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>hs : TotallyBounded s<VAR>ε : ℝ<VAR>ε_pos : ε > 0<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}<VAR>ε : ℝ<VAR>ε_pos : ε > 0<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>s ⊆ a • univ
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>s ⊆ univ
<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>hs₁ : StarConvex ℝ 0 s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ s<GOAL>x ∉ 1 • s
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : Group β<VAR>f : α → β<VAR>hf : IsMulHom f<GOAL>f 1 * f 1 = f 1
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiff 𝕜 ⊤ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 f y
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiffOn 𝕜 ⊤ f univ ↔ DifferentiableOn 𝕜 f univ ∧ ContDiffOn 𝕜 ⊤ (fun y => fderivWithin 𝕜 f univ y) univ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : K<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : K<GOAL>x ∈ LinearMap.range (↑ℤ (↑↑I).subtype) ↔ x ∈ ↑↑I
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<GOAL>im 1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>essSup g (Measure.map f μ) = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>h_eq : ∀ᵐ (x : α) ∂μ, g (f x) = AEMeasurable.mk g hg (f x)<GOAL>AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>h_eq : (fun x => g (f x)) =ᶠ[ae μ] fun x => AEMeasurable.mk g hg (f x)<GOAL>AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑g₁₂ ⇑g₂₃<GOAL>Exact ⇑f₁₂ ⇑f₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑g₁₂ ⇑g₂₃<GOAL>f₁₂.comp ↑e₁.symm = (↑e₂.symm).comp g₁₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑g₁₂ ⇑g₂₃<GOAL>f₂₃.comp ↑e₂.symm = (↑e₃.symm).comp g₂₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<GOAL>IsSeparable (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<GOAL>IsSeparable (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<GOAL>range f ⊆ closure (⋃ n, range ↑(hf.approx n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<VAR>x : α<GOAL>f x ∈ closure (⋃ n, range ↑(hf.approx n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<VAR>x : α<GOAL>∀ᶠ (x_1 : ℕ) in atTop, ↑(hf.approx x_1) x ∈ ⋃ n, range ↑(hf.approx n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<VAR>x : α<VAR>n : ℕ<GOAL>↑(hf.approx n) x ∈ ⋃ n, range ↑(hf.approx n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>this : IsSeparable (closure (⋃ n, range ↑(hf.approx n)))<VAR>x : α<VAR>n : ℕ<GOAL>↑(hf.approx n) x ∈ range ↑(hf.approx n)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<GOAL>(oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ha : ↑(oreDenom (↑s₁) s₂) * ↑s₁ = oreNum (↑s₁) s₂ * ↑s₂<GOAL>(oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<GOAL>(sa • r₁ + ra • r₂) /ₒ (sa * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<GOAL>∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<GOAL>∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<VAR>this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂<GOAL>∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<VAR>this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂<VAR>sd : ↥S<VAR>hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)<GOAL>∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<VAR>this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂<VAR>sd : ↥S<VAR>hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)<GOAL>∃ v, (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<VAR>this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂<VAR>sd : ↥S<VAR>hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)<GOAL>(sd * sc) • (sb • r₁ + rb • r₂) = (↑sd * rc) • (sa • r₁ + ra • r₂) ∧ ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = ↑sd * rc * ↑(sa * s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * sb = rc * ↑sa<VAR>this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂<VAR>sd : ↥S<VAR>hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)<GOAL>(↑sd * ↑sc * sb) • r₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂ ∧ ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝¹ : NoMaxOrder α<VAR>inst✝ : DenselyOrdered α<VAR>w : α<VAR>hw : a < w<GOAL>∃ a_1 ∈ Ioi a, a_1 < w
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : CommSemiring A'<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R A'<VAR>inst✝³ : Algebra R B<VAR>p✝ q✝ : R[X]<VAR>x : A<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>inst✝ : Algebra S T<VAR>p q : S[X]<VAR>h₁ : p ∣ q<VAR>a : T<VAR>h₂ : (aeval a) p = 0<GOAL>(aeval a) q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : CommSemiring A'<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R A'<VAR>inst✝³ : Algebra R B<VAR>p✝ q✝ : R[X]<VAR>x : A<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>inst✝ : Algebra S T<VAR>p q : S[X]<VAR>h₁ : p ∣ q<VAR>a : T<VAR>h₂ : eval a (map (algebraMap S T) p) = 0<GOAL>eval a (map (algebraMap S T) q) = 0
<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✝⁶ : 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>a b : R<VAR>x y : M<VAR>η : Type u_8<VAR>ιs : η → Type u_9<VAR>f : (j : η) → ιs j → M<VAR>hindep : ∀ (j : η), LinearIndependent R (f j)<VAR>hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))<VAR>a✝ : Nontrivial R<GOAL>LinearIndependent (ι := { x // x ∈ range fun ji => f ji.fst ji.snd }) R Subtype.val
<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✝⁶ : 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>a b : R<VAR>x y : M<VAR>η : Type u_8<VAR>ιs : η → Type u_9<VAR>f : (j : η) → ιs j → M<VAR>hindep : ∀ (j : η), LinearIndependent R (f j)<VAR>hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))<VAR>a✝ : Nontrivial R<GOAL>LinearIndependent (ι := { x // x ∈ ⋃ a, range fun b => f ⟨a, b⟩.fst ⟨a, b⟩.snd }) R Subtype.val
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : Fintype m<VAR>R : Type v<VAR>inst✝⁴ : CommRing R<VAR>α : Type u_3<VAR>inst✝³ : Monoid α<VAR>inst✝² : DistribMulAction α R<VAR>inst✝¹ : IsScalarTower α R R<VAR>inst✝ : SMulCommClass α R R<VAR>c : α<VAR>A : Matrix n n R<GOAL>(c • A).det = c ^ Fintype.card n • A.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>val✝ : Infinite ι<GOAL>IsSFiniteKernel (Kernel.sum κs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>val✝¹ : Infinite ι<VAR>val✝ : Denumerable ι<GOAL>IsSFiniteKernel (Kernel.sum κs)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : MulOneClass M<VAR>l✝ : List M<VAR>a : M<VAR>l : List ι<GOAL>(map (fun x => 1) l).prod = 1
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>T : (i : ι) → Set (Set (X i))<VAR>cond : ∀ (i : ι), IsTopologicalBasis (T i)<GOAL>IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}
<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 : OpenEmbedding f<VAR>s : Set X<VAR>h : IsOpen (f '' s)<GOAL>IsOpen s
<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 : OpenEmbedding f<VAR>s : Set X<VAR>h : IsOpen (f '' s)<GOAL>f ⁻¹' (f '' s) = s
<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>f : F[X]<VAR>n : ℕ<GOAL>(f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
<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>f : F[X]<VAR>n : ℕ<GOAL>(n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card
<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>f : F[X]<VAR>n : ℕ<VAR>h : ¬n = 0<GOAL>(n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : α<GOAL>(Ioi a).card = (Ici a).card - 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{v}<GOAL>Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{v}<VAR>a : Ordinal.{max v u}<VAR>ha : a < Ordinal.lift.{u, v} c.ord<GOAL>a < (lift.{u, v} c).ord
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{v}<GOAL>(lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1<GOAL>χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1