ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε<VAR>s : Finset ℕ<VAR>hs : N.primesBelow ≤ s<GOAL>‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε<VAR>s : Finset ℕ<VAR>hs : N.primesBelow ≤ s<VAR>this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε<GOAL>‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.remainingToString = { data := r }
<VAR>l r : List Char<VAR>h : ValidFor l r { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }<GOAL>{ s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.remainingToString = { data := r }
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<GOAL>a * c < b * c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>a * c < b * c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>a * c + (b * d + a * d) < b * c + (b * d + a * d)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v y < v x<GOAL>v (x + y) = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v y < v x<GOAL>v (y + x) = v x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g✝ : E → F<VAR>f' f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x : E<VAR>s t✝ : Set E<VAR>L L₁ L₂ : Filter E<VAR>g' : G → G'<VAR>g : F → G<VAR>t : Set F<VAR>u : Set G<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h2g : MapsTo g t u<VAR>h2f : MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hg : DifferentiableWithinAt 𝕜 g t (f x)<VAR>hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))<GOAL>fderivWithin 𝕜 (g' ∘ g ∘ f) s x = (fderivWithin 𝕜 g' u (g (f x))).comp ((fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x))
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>(f.sum fun e a => C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>(∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f ∧ MeasurableSpace.comap f inst✝¹ = inst✝² ∧ MeasurableSet (range f)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f ∧ MeasurableSpace.comap f inst✝¹ = inst✝² ∧ MeasurableSet (range f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (f '' (f ⁻¹' s))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₂ k₁ k₀ : ι<VAR>r₂₁ : c.Rel k₂ k₁<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<GOAL>G.cliqueSet n = ∅ ↔ G.CliqueFree n
<VAR>m n✝ n : ℕ<VAR>inst✝ : Fact (1 < n)<GOAL>val 1 = 1
<VAR>m n✝ n : ℕ<VAR>inst✝ : Fact (1 < n)<GOAL>1 % n = 1
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>v : n → α<VAR>i j : n<GOAL>(diagonal v).adjugate i j = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>v : n → α<VAR>i j : n<GOAL>((diagonal v).updateColumn j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>v : n → α<VAR>i : n<GOAL>((diagonal v).updateColumn i (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>v : n → α<VAR>i j : n<VAR>hij : i ≠ j<GOAL>((diagonal v).updateColumn j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>0 < finrank R M ↔ ∃ x, x ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>(fun x => (map f μ).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>Measurable fun x => (map f μ).rnDeriv (map f ν) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>Measurable (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<GOAL>∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<GOAL>∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<VAR>hs_eq : s = f ⁻¹' (f '' s)<GOAL>∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<VAR>hs_eq : s = f ⁻¹' (f '' s)<VAR>this : SigmaFinite (map f ν)<GOAL>∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>span R s ⊔ p = span R (s ∪ ↑p)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x : α<VAR>l : List α<VAR>h : (x :: l).Nodup<VAR>n : ℕ<GOAL>((x :: l).formPerm ^ n) x = (x :: l).get ⟨n % (x :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x : α<VAR>l : List α<VAR>h : (x :: l).Nodup<VAR>n : ℕ<GOAL>n = ↑⟨0, ⋯⟩ + n
<VAR>m n : ℕ<VAR>x : { x // x ≠ Fin.last n }<GOAL>(finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯
<VAR>m n : ℕ<VAR>x : { x // x ≠ Fin.last n }<GOAL>some ((finSuccAboveEquiv (Fin.last n)).symm x) = some ((↑x).castLT ⋯)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)<VAR>s : Finset α<VAR>f : α →₀ M<VAR>hf : f.support = ∅<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)<VAR>s✝ : Finset α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : ∀ (f : α →₀ M), f.support = s → p f<VAR>f : α →₀ M<VAR>hf : f.support = cons a s has<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)<VAR>s✝ : Finset α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : ∀ (f : α →₀ M), f.support = s → p f<VAR>f : α →₀ M<VAR>hf : f.support = cons a s has<GOAL>p (erase a f + single a (f a))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<GOAL>s.card ≤ (s.biUnion f).card + (filter (fun i => f i = ∅) s).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<GOAL>(filter (fun a => ¬f a = ∅) s).card + (filter (fun i => f i = ∅) s).card ≤ (s.biUnion f).card + (filter (fun i => f i = ∅) s).card
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<GOAL>β ∈ F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<GOAL>β ∈ F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<GOAL>β ∈ F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<VAR>h_sep : h.Separable<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<VAR>h_sep : h.Separable<VAR>h_root : eval β h = 0<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<VAR>h_sep : h.Separable<VAR>h_root : eval β h = 0<VAR>h_splits : Splits ιEE' h<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)