ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>x₀ : M<GOAL>𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹⁴ : Semiring R<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : Semiring R₃<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>f : M →ₗ[R] M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<GOAL>ker (f.restrict hf) = ker (f.domRestrict p)
<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>absorbs : Absorbent ℝ s<VAR>a : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r ∈ Ioo 0 a, r • s
<VAR>k : ℕ<VAR>x✝ : k + 2 ≠ 0<VAR>m : ℕ := (k + 2).minFac<VAR>this : (k + 2) / m < k + 2<GOAL>(k + 2).primeFactorsList.prod = k + 2
<VAR>k : ℕ<VAR>x✝ : k + 2 ≠ 0<VAR>m : ℕ := (k + 2).minFac<VAR>this : (k + 2) / m < k + 2<VAR>h₁ : (k + 2) / m ≠ 0<GOAL>(k + 2).primeFactorsList.prod = k + 2
<VAR>α : Type u<VAR>β : α → Type v<VAR>κ : Cardinal.{max u v}<VAR>hκ : (sum fun a => κ ^ lift.{u, v} #(β a)) ≤ κ<GOAL>#(WType β) ≤ κ
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type (max u v)<VAR>hκ : (sum fun a => #γ ^ lift.{u, v} #(β a)) ≤ #γ<GOAL>#(WType β) ≤ #γ
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type (max u v)<VAR>hκ : (sum fun a => #γ ^ lift.{max u v, v} #(β a)) ≤ #γ<GOAL>#(WType β) ≤ #γ
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type (max u v)<VAR>hκ : (sum fun a => lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ<GOAL>#(WType β) ≤ #γ
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type (max u v)<VAR>hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)<GOAL>#(WType β) ≤ #γ
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type (max u v)<VAR>hκ : (i : α) × (β i → γ) ↪ γ<GOAL>#(WType β) ≤ #γ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>S.leftRightHomologyComparison = S.leftHomologyIso.hom ≫ S.rightHomologyIso.inv
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t u : Multiset α<GOAL>s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>m : Multiset ι<VAR>hm : m.Nodup<GOAL>{ val := m, nodup := hm }.prod f ≠ 0 → ({ val := m, nodup := hm }.prod f).roots = { val := m, nodup := hm }.val.bind fun i => (f i).roots
<VAR>a : ℕ<VAR>l : List ℕ<VAR>x : Γ'<VAR>h : x ∈ trList (a :: l)<GOAL>x ≠ Γ'.consₗ
<VAR>a : ℕ<VAR>l : List ℕ<VAR>x : Γ'<VAR>h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l<GOAL>x ≠ Γ'.consₗ
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p n = (filter p (range n)).card
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>(List.filter (fun b => decide (p b)) (List.range n)).length = (filter p (range n)).card
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>f : G →* N<GOAL>Injective ⇑f.rangeRestrict ↔ Injective ⇑f
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<GOAL>MeasurableSet {a | κ a ⟂ₘ η a}
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<GOAL>MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<GOAL>Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<VAR>h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)<GOAL>∀ (ib : Set Y), b ∉ ib ∧ IsClosed ib → ∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<VAR>h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)<VAR>s : Set Y<VAR>hbs : b ∉ s<VAR>hsc : IsClosed s<GOAL>∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<VAR>h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)<VAR>s : Set Y<VAR>hbs : b ∉ s<VAR>hsc : IsClosed s<GOAL>a ∈ closure (f ⁻¹' s) → b ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<VAR>h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)<VAR>s : Set Y<VAR>hbs : b ∉ s<VAR>hsc : IsClosed s<GOAL>a ∈ seqClosure (f ⁻¹' s) → b ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<VAR>h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)<VAR>s : Set Y<VAR>hbs : b ∉ s<VAR>hsc : IsClosed s<VAR>u : ℕ → X<VAR>hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s<VAR>hu : Tendsto u atTop (𝓝 a)<GOAL>b ∈ s
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>‖f p‖ < 1
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>Summable fun n => f p ^ n
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>Summable fun n => f (p ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s t : Set α<VAR>S : Set (Set α)<VAR>hs : t ∈ S<VAR>h : s ∩ ⋃₀ S = ∅<GOAL>s ∩ t ⊆ s ∩ ⋃₀ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>x : E<GOAL>(k⁻¹ • fun x => x -ᵥ c) ((fun x => k • x +ᵥ c) x) = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>p : P<GOAL>(fun x => k • x +ᵥ c) ((k⁻¹ • fun x => x -ᵥ c) p) = p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>x y : E<GOAL>edist ({ toFun := fun x => k • x +ᵥ c, invFun := k⁻¹ • fun x => x -ᵥ c, left_inv := ⋯, right_inv := ⋯ }.toFun x) ({ toFun := fun x => k • x +ᵥ c, invFun := k⁻¹ • fun x => x -ᵥ c, left_inv := ⋯, right_inv := ⋯ }.toFun y) = ↑‖k‖₊ * edist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>x y : E<GOAL>edist (k • x) (k • y) = ↑‖k‖₊ * edist x y
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid N₁<VAR>inst✝⁶ : AddCommMonoid N₂<VAR>inst✝⁵ : AddCommMonoid N₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₃<VAR>σ : R →+* S<VAR>F : Type u_17<VAR>inst✝¹ : FunLike F M M₃<VAR>inst✝ : SemilinearMapClass F σ M M₃<VAR>f g : F<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid N₁<VAR>inst✝⁶ : AddCommMonoid N₂<VAR>inst✝⁵ : AddCommMonoid N₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₃<VAR>σ : R →+* S<VAR>F : Type u_17<VAR>inst✝¹ : FunLike F M M₃<VAR>inst✝ : SemilinearMapClass F σ M M₃<VAR>f g : F<VAR>h : ↑f = ↑g<GOAL>∀ (x : M), f x = g x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid N₁<VAR>inst✝⁶ : AddCommMonoid N₂<VAR>inst✝⁵ : AddCommMonoid N₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₃<VAR>σ : R →+* S<VAR>F : Type u_17<VAR>inst✝¹ : FunLike F M M₃<VAR>inst✝ : SemilinearMapClass F σ M M₃<VAR>f g : F<VAR>h : ↑f = ↑g<VAR>m : M<GOAL>f m = g m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>s : SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : ↑s A ≤ 0<VAR>hB₂ : ↑s B ≤ 0<VAR>hAB : ↑s (A ∪ B) = 0<GOAL>↑s A = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>s : SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : ↑s A ≤ 0<VAR>hB₂ : ↑s B ≤ 0<VAR>hAB : ↑s A + ↑s B = 0<GOAL>↑s A = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α → β<VAR>inst✝ : DecidableEq β<VAR>y : β<GOAL>(filter (fun x => f x = y) s).card ≠ 0 ↔ y ∈ image f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<GOAL>¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>h : ∀ o' < o, P I o'<VAR>hho : o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C o<GOAL>LinearIndependent ℤ (eval C)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>h : ∀ o' < o, P I o'<VAR>hho : o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C o<GOAL>LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x y z : ℝ<VAR>h : 0 ≤ x<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<GOAL>x ^ z ≤ y ^ z
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>h : 0 ≤ x<VAR>h₂ : 0 ≤ z<VAR>h₁ : x ≤ x<GOAL>x ^ z ≤ x ^ z
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x y z : ℝ<VAR>h : 0 ≤ x<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<VAR>h₁' : x < y<GOAL>x ^ z ≤ y ^ z
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x y : ℝ<VAR>h : 0 ≤ x<VAR>h₁ : x ≤ y<VAR>h₁' : x < y<VAR>h₂ : 0 ≤ 0<GOAL>x ^ 0 ≤ y ^ 0
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x y z : ℝ<VAR>h : 0 ≤ x<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<VAR>h₁' : x < y<VAR>h₂' : 0 < z<GOAL>x ^ z ≤ y ^ z
<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>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⟪v i, ∑ i ∈ s, l i • v i⟫_𝕜 = l i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<GOAL>(filter (fun l => !l.isEmpty) ([] :: L)).join = ([] :: L).join
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<GOAL>Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0<GOAL>Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0<GOAL>Algebra.adjoin K ↑(map (algebraMap K (SplittingFieldAux n.succ f)) f).roots.toFinset = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) * map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠ 0<GOAL>Algebra.adjoin K ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) * map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) * map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠ 0<GOAL>Subalgebra.restrictScalars K (Algebra.adjoin ↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) * map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠ 0<VAR>this : Subalgebra.restrictScalars K (Algebra.adjoin (↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) = Subalgebra.restrictScalars K (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor)))<GOAL>Subalgebra.restrictScalars K (Algebra.adjoin ↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) = ⊤
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hfn : f.natDegree = n.succ<VAR>hndf : f.natDegree ≠ 0<VAR>hfn0 : f ≠ 0<VAR>hmf0 : map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) * map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠ 0<VAR>this : Subalgebra.restrictScalars K (Algebra.adjoin (↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) = Subalgebra.restrictScalars K (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor)))<GOAL>Subalgebra.restrictScalars K (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) = ⊤
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹⁴ : Ring k<VAR>inst✝¹³ : AddCommGroup V₁<VAR>inst✝¹² : Module k V₁<VAR>inst✝¹¹ : AffineSpace V₁ P₁<VAR>inst✝¹⁰ : AddCommGroup V₂<VAR>inst✝⁹ : Module k V₂<VAR>inst✝⁸ : AffineSpace V₂ P₂<VAR>inst✝⁷ : AddCommGroup V₃<VAR>inst✝⁶ : Module k V₃<VAR>inst✝⁵ : AffineSpace V₃ P₃<VAR>inst✝⁴ : AddCommGroup V₄<VAR>inst✝³ : Module k V₄<VAR>inst✝² : AffineSpace V₄ P₄<VAR>R' : Type u_10<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Module R' V₁<VAR>c p : P₁<GOAL>(homothety c (-1)) p = (pointReflection R' c) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMinOrder α<VAR>a b : α<GOAL>interior (Ico a b) = Ioo a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : ψ ∘ φ = id<VAR>hφ : Tendsto φ f g<VAR>hψ : Tendsto ψ g f<GOAL>comap φ g = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : ψ ∘ φ = id<VAR>hφ : Tendsto φ f g<VAR>hψ : Tendsto ψ g f<GOAL>comap φ (comap ψ f) ≤ f
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hcst : μ[|s] t ≠ 0<GOAL>0 < μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hcst : μ[|s] t ≠ 0<GOAL>(μ s)⁻¹ * μ (s ∩ t) ≠ 0
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hcst : μ[|s] t ≠ 0<GOAL>(μ s)⁻¹ * μ (s ∩ t) = μ[|s] t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>(↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : Finite p a ∧ Finite p b<GOAL>multiplicity p (a * b) = multiplicity p a + multiplicity p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : ¬(Finite p a ∧ Finite p b)<GOAL>multiplicity p (a * b) = multiplicity p a + multiplicity p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : ¬(Finite p a ∧ Finite p b)<GOAL>⊤ = multiplicity p a + multiplicity p b
<VAR>m n : Nat<GOAL>m ∈ range n ↔ m < n
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<VAR>v : P<VAR>y : ↥S<GOAL>(f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<VAR>v : P<VAR>y : ↥S<GOAL>g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v