ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>u : Set ι<VAR>hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ ⋃ n ∈ u, s n<VAR>ht2 : t2 ∈ s'<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>u : Set ι<VAR>hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht2 : t2 ∈ s'<VAR>ht1 : ∃ i, ∃ (_ : i ∈ u), t1 ∈ s i<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : f ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : f ≈ 0<VAR>hg : g ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : ¬f ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>padicNorm p (↑f (stationaryPoint ⋯)) = padicNorm p (↑g (stationaryPoint ⋯))
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∀ (x : X), {i | x ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))} → ρ.fintsupport x ⊆ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ y : X<VAR>hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}<VAR>z : ι<VAR>hz : z ∈ ρ.fintsupport y<GOAL>z ∈ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ y : X<VAR>hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}<VAR>z : ι<VAR>hz : y ∈ tsupport ⇑(ρ z)<GOAL>x₀ ∈ tsupport ⇑(ρ z)
<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>(o.oangle (x - y) x).sin * ‖x - y‖ = ‖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 y x = ↑(π / 2)<GOAL>((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖
<VAR>l m₁ m₂ r : List Char<VAR>s : Substring<VAR>h : ValidFor l (m₁ ++ m₂) r s<VAR>n : Nat<GOAL>s.nextn n (s.next { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Splits (RingHom.id K) f<GOAL>Multiset.card f.roots = f.natDegree
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Splits (RingHom.id K) f<GOAL>f = map (RingHom.id K) f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>0 < ⌊a⌋ ↔ 1 ≤ a
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>C : FreeAlgebra R X → Prop<VAR>h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)<VAR>h_grade1 : ∀ (x : X), C (ι R x)<VAR>h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)<VAR>h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)<VAR>a : FreeAlgebra R X<VAR>s : Subalgebra R (FreeAlgebra R X) := { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }<VAR>of : X → ↥s := Subtype.coind (ι R) h_grade1<VAR>of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>C : FreeAlgebra R X → Prop<VAR>h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)<VAR>h_grade1 : ∀ (x : X), C (ι R x)<VAR>h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)<VAR>h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)<VAR>a : FreeAlgebra R X<VAR>s : Subalgebra R (FreeAlgebra R X) := { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }<VAR>of : X → ↥s := Subtype.coind (ι R) h_grade1<VAR>of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)<GOAL>a = ↑(((lift R) of) a)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>C : FreeAlgebra R X → Prop<VAR>h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)<VAR>h_grade1 : ∀ (x : X), C (ι R x)<VAR>h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)<VAR>h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)<VAR>a : FreeAlgebra R X<VAR>s : Subalgebra R (FreeAlgebra R X) := { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }<VAR>of : X → ↥s := Subtype.coind (ι R) h_grade1<VAR>of_id : ∀ (x : FreeAlgebra R X), x = ↑(((lift R) of) x)<GOAL>a = ↑(((lift R) of) a)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>μ ν : Measure Ω<VAR>h_le : ε₁ ≤ ε₂<VAR>B : Set Ω<VAR>hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁<VAR>ε_top : ¬ε₂ = ⊤<GOAL>μ B ≤ ν (thickening ε₂.toReal B) + ε₂
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>μ ν : Measure Ω<VAR>h_le : ε₁ ≤ ε₂<VAR>B : Set Ω<VAR>hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁<VAR>ε_top : ¬ε₂ = ⊤<GOAL>ν (thickening ε₁.toReal B) ≤ ν (thickening ε₂.toReal B)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<GOAL>max ℵ₀ #K ≤ Module.rank K (ℕ → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<GOAL>max ℵ₀ #K ≤ Module.rank K (ℕ → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<GOAL>#K ≤ Module.rank K (ℕ → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : #K ≤ ℵ₀<GOAL>#K ≤ Module.rank K (ℕ → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<GOAL>#K ≤ Module.rank K (ℕ → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this : Module.rank K (ℕ → K) < #K<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>rep_e : (Finsupp.total ιK (ℕ → K) K ⇑bK) (bK.repr (⇑bL ∘ ⇑e)) = ⇑bL ∘ ⇑e<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>rep_e : ∑ a ∈ (bK.repr (⇑bL ∘ ⇑e)).support, (bK.repr (⇑bL ∘ ⇑e)) a • bK a = ⇑bL ∘ ⇑e<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)<VAR>s : Finset ιK := c.support<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)<VAR>s : Finset ιK := c.support<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)<VAR>s : Finset ιK := c.support<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)<VAR>s : Finset ιK := c.support<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>i : ℕ<VAR>hi : i ∈ t<VAR>hgi : g i ≠ 0<GOAL>False
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)<VAR>s : Finset ιK := c.support<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>i : ℕ<VAR>hi : i ∈ t<VAR>hgi : g i ≠ 0<GOAL>∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i : ℕ<VAR>hi : i ∈ t<VAR>hgi : g i ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<GOAL>∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i : ℕ<VAR>hi : i ∈ t<VAR>hgi : g i ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<GOAL>∑ x ∈ t, ∑ x_1 ∈ s, g x • c x_1 • bK x_1 x = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i : ℕ<VAR>hi : i ∈ t<VAR>hgi : g i ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<GOAL>∑ y ∈ s, ∑ x ∈ t, g x • c y • bK y x = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i✝ : ℕ<VAR>hi✝ : i✝ ∈ t<VAR>hgi : g i✝ ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>eq0 : ∑ i ∈ t, g i • f i = 0<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>i : ιK<VAR>hi : i ∈ s<GOAL>∑ x ∈ t, g x • c i • bK i x = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i✝ : ℕ<VAR>hi✝ : i✝ ∈ t<VAR>hgi : g i✝ ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>i : ιK<VAR>hi : i ∈ s<VAR>eq0 : L.subtype ((∑ i ∈ t, g i • f i) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)<GOAL>∑ x ∈ t, g x • c i • bK i x = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝¹ : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i✝ : ℕ<VAR>hi✝ : i✝ ∈ t<VAR>hgi : g i✝ ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>i : ιK<VAR>hi : i ∈ s<VAR>eq0 : ∑ x ∈ t, L.subtype ((g x • f x) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)<GOAL>∑ x ∈ t, g x • c i • bK i x = 0
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝² : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝¹ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i✝ : ℕ<VAR>hi✝ : i✝ ∈ t<VAR>hgi : g i✝ ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this✝ : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>i : ιK<VAR>hi : i ∈ s<VAR>eq0 : ∑ x ∈ t, L.subtype ((g x • f x) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)<VAR>this : SMulCommClass (↥L)ᵐᵒᵖ K K<GOAL>∑ x ∈ t, g x • c i • bK i x = 0