ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ β : Type u<VAR>c✝ : Cardinal.{?u.232416}<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<VAR>t : Set ↑s<GOAL>Injective Subtype.val
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α ι<VAR>i : ι<VAR>a✝ x : α<VAR>l : Line (η → α) ι<VAR>a : η → α<VAR>ie : ι × η<GOAL>↑l.toSubspace a ie = (fun x i => (l.idxFun i).getD x) a ie.1 ie.2
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (f.coprod g) (p.prod q) = map f p ⊔ map g q
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (f.coprod g) (p.prod q) ≤ map f p ⊔ map g q
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>p ≤ comap f (map (f.coprod g) (p.prod q))
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>q ≤ comap g (map (f.coprod g) (p.prod q))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>f : Dual R N<VAR>x : N<GOAL>(p (p.toDualLeft.symm f)) x = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>f : Dual R N<VAR>x : N<VAR>h : p.toDualLeft (p.toDualLeft.symm f) = f<GOAL>(p (p.toDualLeft.symm f)) x = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>f : Dual R N<VAR>x : N<VAR>h : p (p.toDualLeft.symm f) = f<GOAL>(p (p.toDualLeft.symm f)) x = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>i : ℕ<VAR>m : M<GOAL>(comp p) ((single R i) m) = p ^ i • (single R 0) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>i : ℕ<VAR>m : M<GOAL>(eval p) ((map R[X] (lsingle R 0)) ((single R i) m)) = p ^ i • (single R 0) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>i : ℕ<VAR>m : M<GOAL>p ^ i • (lsingle R 0) m = p ^ i • (single R 0) m
<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✝ : DecidableEq α<VAR>l : List α<GOAL>(map (fun x => count x l) l.dedup).sum = l.length
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<VAR>D : (↑s).Pairwise (Disjoint on fun c => ball c δ)<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<VAR>D : (↑s).Pairwise (Disjoint on fun c => ball c δ)<VAR>A_subset : A ⊆ ball 0 ρ<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<VAR>D : (↑s).Pairwise (Disjoint on fun c => ball c δ)<VAR>A_subset : A ⊆ ball 0 ρ<VAR>I : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1)<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<VAR>D : (↑s).Pairwise (Disjoint on fun c => ball c δ)<VAR>A_subset : A ⊆ ball 0 ρ<VAR>I : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1)<VAR>J : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>μ : Measure E := Measure.addHaar<VAR>δ : ℝ := 1 / 2<VAR>ρ : ℝ := 5 / 2<VAR>ρpos : 0 < ρ<VAR>A : Set E := ⋃ c ∈ s, ball c δ<VAR>hA : A = ⋃ c ∈ s, ball c δ<VAR>D : (↑s).Pairwise (Disjoint on fun c => ball c δ)<VAR>A_subset : A ⊆ ball 0 ρ<VAR>I : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1)<VAR>J : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)<VAR>K : ↑s.card ≤ 5 ^ finrank ℝ E<GOAL>s.card ≤ 5 ^ finrank ℝ E
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>Wbtw R ((lineMap w ((lineMap w z) t₁)) t₂) ((lineMap w z) t₁) z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>(lineMap ((lineMap w ((lineMap w z) t₁)) t₂) z) ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) = (lineMap w z) t₁
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>(((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hca : c ∣ a<VAR>h : ¬c = 0<GOAL>a % c + b % c < c
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hca : c ∣ a<VAR>h : ¬c = 0<GOAL>b % c < c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : IsPRadical i p<GOAL>Ideal.comap i (pNilradical L p) = pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<VAR>h : x ∈ Ideal.comap i (pNilradical L p)<GOAL>∃ n, x ^ p ^ n = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<VAR>h : x ∈ pNilradical K p<GOAL>x ∈ Ideal.comap i (pNilradical L p)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<VAR>h : ∃ n, x ^ p ^ n = 0<GOAL>∃ n, i x ^ p ^ n = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<VAR>n : ℕ<VAR>h : x ^ p ^ n = 0<GOAL>∃ n, i x ^ p ^ n = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμsc : c = 0 ∨ μ s ≠ ⊤<GOAL>Memℒp (s.indicator fun x => c) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμsc : c = 0 ∨ μ s ≠ ⊤<GOAL>Memℒp (fun x => c) p (μ.restrict s)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>r : ℝ≥0∞<GOAL>volume (EMetric.closedBall a r) = 2 * r
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (EMetric.closedBall a ⊤) = 2 * ⊤
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>volume (EMetric.closedBall a r) = 2 * r
<VAR>m n k : ℕ<GOAL>(m + k * n).gcd n = m.gcd n
<VAR>n : ℕ<GOAL>orderOf (r 1) = n
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>orderOf (r 1) = n
<VAR>α : Type u_1<VAR>inst✝² : Ring α<VAR>n₁ n₂ : ℤ<VAR>a₁ a₂ : α<VAR>inst✝¹ : Invertible a₁<VAR>inst✝ : Invertible a₂<GOAL>↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : E<GOAL>‖v‖ ≤ ‖u‖ + ‖u / v‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : E<GOAL>‖v‖ ≤ ‖u‖ + ‖v / u‖
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ι : Type u_4<VAR>t : ι → IntermediateField K L<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)<VAR>x : L<VAR>hx : x ∈ ⨆ i, t i<GOAL>IsAlgebraic K ⟨x, hx⟩
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ι : Type u_4<VAR>t : ι → IntermediateField K L<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)<VAR>x : L<VAR>hx✝ : x ∈ ⨆ i, t i<VAR>s : Finset ((i : ι) × ↥(t i))<VAR>hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯<GOAL>IsAlgebraic K ⟨x, hx✝⟩
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ι : Type u_4<VAR>t : ι → IntermediateField K L<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)<VAR>x : L<VAR>hx✝ : x ∈ ⨆ i, t i<VAR>s : Finset ((i : ι) × ↥(t i))<VAR>hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯<GOAL>IsAlgebraic K ⟨x, hx⟩
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ι : Type u_4<VAR>t : ι → IntermediateField K L<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)<VAR>x : L<VAR>hx✝ : x ∈ ⨆ i, t i<VAR>s : Finset ((i : ι) × ↥(t i))<VAR>hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯<VAR>this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional K ↥K⟮↑i.snd⟯<GOAL>IsAlgebraic K ⟨x, hx⟩
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n✝ : ℕ<VAR>a b c : α<VAR>n : ℕ<GOAL>|(-1) ^ n| = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : Zero γ<VAR>c : α<VAR>f : β → γ<VAR>x : β<GOAL>(x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ : Measure α<VAR>κ : Kernel α β<VAR>h : ¬SFinite μ<GOAL>μ ⊗ₘ κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ : Measure α<VAR>κ : Kernel α β<VAR>h : ¬SFinite μ<GOAL>¬IsSFiniteKernel (Kernel.const Unit μ)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactSpace (X × Y)<GOAL>Continuous curry
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactSpace (X × Y)<GOAL>Continuous (Function.uncurry fun x y => x.curry y)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactSpace (X × Y)<GOAL>Continuous (Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactSpace (X × Y)<GOAL>Continuous ((Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y) ∘ ⇑(Homeomorph.prodAssoc C(X × Y, Z) X Y).symm)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m<VAR>m : ℕ<GOAL>A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m<VAR>m : ℕ<VAR>h : A⁻¹ * A = 1<VAR>h' : A * A⁻¹ = 1<GOAL>A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<VAR>IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m<VAR>m : ℕ<VAR>h : A⁻¹ = 0<GOAL>A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>x y : α<VAR>n : ℕ<VAR>f : α →+* β<GOAL>f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<VAR>ha : a < c.ord<GOAL>nfpFamily f a < c.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<VAR>ha : a < c.ord<GOAL>ℵ₀ < c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<VAR>ha : a < c.ord<GOAL>lift.{v, u} #ι < c
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hl : (monomial n) s ∈ lifts f<VAR>hzero : ¬s = 0<GOAL>∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hl : (monomial n) s ∈ Set.range (map f)<VAR>hzero : ¬s = 0<GOAL>∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : map f q = (monomial n) s<GOAL>∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<GOAL>∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<GOAL>∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<GOAL>map f ((monomial n) (q.coeff n)) = (monomial n) s ∧ ((monomial n) (q.coeff n)).degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<GOAL>((monomial n) (q.coeff n)).degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<VAR>hqzero : q.coeff n ≠ 0<GOAL>((monomial n) (q.coeff n)).degree = ((monomial n) s).degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<VAR>hqzero : q.coeff n ≠ 0<GOAL>(C (q.coeff n) * X ^ n).degree = ((monomial n) s).degree