ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] := let __src := mapRingHom (eval s); { toRingHom := __src, commutes' := ⋯ }<GOAL>(aeval (Fin.cons y s)) (X 0) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X 0) ∧ ∀ (i : Fin n), (aeval (Fin.cons y s)) (X i.succ) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i.succ)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Coindep X ↔ ∃ B, M.Base B ∧ B ⊆ M.E \ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a⁻¹ * b = 1 ↔ a = b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup Gᵐᵒᵖ<GOAL>stabilizer G ↑s = s.unop
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup Gᵐᵒᵖ<GOAL>∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.unop
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Subgroup Gᵐᵒᵖ<VAR>a : G<VAR>h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s<GOAL>a ∈ s.unop
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Subgroup Gᵐᵒᵖ<VAR>a : G<VAR>h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s<VAR>this : 1 * op a ∈ s<GOAL>a ∈ s.unop
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.82622, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasLeftHomology<VAR>hg : S.g = 0<GOAL>S.cycles ≅ S.X₂
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.82622, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasLeftHomology<VAR>hg : S.g = 0<VAR>this : IsIso S.iCycles<GOAL>S.cycles ≅ S.X₂
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<GOAL>((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<GOAL>(if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<GOAL>∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<GOAL>n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>ha : ∀ (x : α), x ∈ zpowers a<GOAL>image (fun i => a ^ i) (range (Fintype.card α)) = univ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<GOAL>(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Subsingleton A<GOAL>(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Nontrivial A<GOAL>(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Nontrivial A<GOAL>(Algebra.lmul A S) pb.gen = (Matrix.toLin pb.basis pb.basis) (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Nontrivial A<VAR>k : Fin pb.dim<GOAL>((Algebra.lmul A S) pb.gen) (pb.basis k) = ((Matrix.toLin pb.basis pb.basis) (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)) (pb.basis k)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Nontrivial A<VAR>k : Fin pb.dim<GOAL>((Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) = ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>h✝ : Nontrivial A<VAR>k : Fin pb.dim<GOAL>pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasStrictInitialObjects C<VAR>I X : C<VAR>inst✝ : HasBinaryProduct I X<VAR>hI : IsInitial I<GOAL>I ⨯ X ≅ I
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasStrictInitialObjects C<VAR>I X : C<VAR>inst✝ : HasBinaryProduct I X<VAR>hI : IsInitial I<VAR>this : IsIso prod.fst<GOAL>I ⨯ X ≅ I
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m K<VAR>h : IsUnit A<GOAL>Function.Injective ⇑A.vecMulLinear
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m K<VAR>h : IsUnit A<GOAL>∀ (m_1 : m → K), A.vecMulLinear m_1 = 0 → m_1 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y z : α<GOAL>(swap x y * f) z = (f * swap (f⁻¹ x) (f⁻¹ y)) z
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y z : α<GOAL>(if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>x✝ : Y<GOAL>(h.symm.trans h) x✝ = (Homeomorph.refl Y) x✝
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>fst✝ : E<VAR>snd✝ : F<GOAL>(fst✝, snd✝) ∈ f.graph ↔ ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F₁ F₂ : C × D ⥤ E<VAR>h : curry.obj F₁ = curry.obj F₂<GOAL>F₁ = F₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>a : X<VAR>x✝ : ↑I<GOAL>((refl a).trans (refl a)) x✝ = (refl a) x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>a : X<VAR>x✝ : ↑I<GOAL>{ toFun := (fun t => a) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } x✝ = (refl a) x✝
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>t : Set β<VAR>ht : 0 ∈ t<VAR>hs : MeasurableSet s<GOAL>t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>q : ℕ → Prop := fun i => p i ∧ 0 < r i<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>q : ℕ → Prop := fun i => p i ∧ 0 < r i<VAR>h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>q : ℕ → Prop := fun i => p i ∧ 0 < r i<VAR>h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q<VAR>h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>q : ℕ → Prop := fun i => p i ∧ 0 < r i<VAR>h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q<VAR>h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop q =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>DenseEmbedding Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>DenseRange Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<GOAL>f ∈ closure (Set.range Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<VAR>hfi' : Memℒp (↑↑f) p μ<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<VAR>hfi' : Memℒp (↑↑f) p μ<VAR>this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<VAR>hfi' : Memℒp (↑↑f) p μ<VAR>this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})<GOAL>Tendsto (fun n => ↑(toLp (SimpleFunc.approxOn ↑↑f ⋯ (Set.range ↑↑f ∪ {0}) 0 ⋯ n) ⋯)) atTop (𝓝 f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f : ↥(Lp E p μ)<VAR>hfi' : Memℒp (↑↑f) p μ<VAR>this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})<GOAL>f = Memℒp.toLp (↑↑f) hfi'
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hq : eval₂ f x q = 0<GOAL>eval₂ f x (p * q) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hq : eval₂ f x q = 0<GOAL>eval₂ f x p * eval₂ f x q = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : sSup {m | IsSimpleModule R ↥m} = ⊤<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<GOAL>∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>f : X → ℝ<VAR>hf : Continuous f<VAR>hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s<VAR>hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ<VAR>h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1<GOAL>∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>f : X → ℝ<VAR>hf : Continuous f<VAR>hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s<VAR>hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ<VAR>h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1<VAR>A : t ⊆ (interior k)ᶜ<GOAL>∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>f : X → ℝ<VAR>hf : Continuous f<VAR>hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s<VAR>hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ<VAR>h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1<VAR>A : t ⊆ (interior k)ᶜ<GOAL>HasCompactSupport ⇑{ toFun := fun x => 1 - f x, continuous_toFun := ⋯ }
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>f : X → ℝ<VAR>hf : Continuous f<VAR>hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s<VAR>hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ<VAR>h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1<VAR>A : t ⊆ (interior k)ᶜ<VAR>x : X<GOAL>{ toFun := fun x => 1 - f x, continuous_toFun := ⋯ } x ∈ Icc 0 1
<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>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>x✝¹ : N<VAR>x✝ : Dual R N<GOAL>(↑(e ≪≫ₗ e.flip.symm.dualMap) x✝¹) x✝ = ((Dual.eval R N) x✝¹) x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>hG : 0 < Fintype.card G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ ∅ ^ k<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<VAR>mono : Monotone fun n => Fintype.card ↑(S ^ n)<GOAL>∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<VAR>mono : Monotone fun n => Fintype.card ↑(S ^ n)<VAR>n : ℕ<VAR>h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))<GOAL>∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<VAR>mono : Monotone fun n => Fintype.card ↑(S ^ n)<VAR>n : ℕ<VAR>h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))<VAR>h₂ : S ^ n * {a} = S ^ (n + 1)<GOAL>∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<VAR>mono : Monotone fun n => Fintype.card ↑(S ^ n)<VAR>n : ℕ<VAR>h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))<VAR>h₂ : S ^ n * {a} = S ^ (n + 1)<GOAL>∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)