ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<VAR>f' : unop (op [m]) ⟶ [n + 1]<VAR>hf : (standardSimplex.objEquiv [n + 1] (op [m])).symm f' = ↑f<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<VAR>f' : unop (op [m]) ⟶ [n + 1]<VAR>hf : (standardSimplex.objEquiv [n + 1] (op [m])).symm f' = ↑f<VAR>j : Fin (n + 2)<VAR>hji : ¬j = i<VAR>hfj : ∀ (k : Fin ((unop (op [m])).len + 1)), (Hom.toOrderHom f') k ≠ j<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<VAR>f' : unop (op [m]) ⟶ [n + 1]<VAR>hf : (standardSimplex.objEquiv [n + 1] (op [m])).symm f' = ↑f<VAR>j : Fin (n + 2)<VAR>hji : ¬j = i<VAR>hfj : ∀ (k : Fin ((unop (op [m])).len + 1)), (Hom.toOrderHom f') k ≠ j<VAR>H : f = Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<VAR>f' : unop (op [m]) ⟶ [n + 1]<VAR>hf : (standardSimplex.objEquiv [n + 1] (op [m])).symm f' = ↑f<VAR>j : Fin (n + 2)<VAR>hji : ¬j = i<VAR>hfj : ∀ (k : Fin ((unop (op [m])).len + 1)), (Hom.toOrderHom f') k ≠ j<VAR>H : f = Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)<VAR>H₁ : (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₁.app (op [m])) (face i j hji) = (σ₁.app (op [n]) ≫ S.map (factor_δ f' j).op) (face i j hji)<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<VAR>f' : unop (op [m]) ⟶ [n + 1]<VAR>hf : (standardSimplex.objEquiv [n + 1] (op [m])).symm f' = ↑f<VAR>j : Fin (n + 2)<VAR>hji : ¬j = i<VAR>hfj : ∀ (k : Fin ((unop (op [m])).len + 1)), (Hom.toOrderHom f') k ≠ j<VAR>H : f = Λ[n + 1, i].map (factor_δ f' j).op (face i j hji)<VAR>H₁ : (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₁.app (op [m])) (face i j hji) = (σ₁.app (op [n]) ≫ S.map (factor_δ f' j).op) (face i j hji)<VAR>H₂ : (Λ[n + 1, i].map (factor_δ f' j).op ≫ σ₂.app (op [m])) (face i j hji) = (σ₂.app (op [n]) ≫ S.map (factor_δ f' j).op) (face i j hji)<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<GOAL>x - (toZMod x).cast ∈ maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<GOAL>(toZMod x).cast = ↑x.zmodRepr
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<GOAL>(↑x.zmodRepr).cast = ↑x.zmodRepr
<VAR>r : ℚ<VAR>p' : ℕ<VAR>hp_prime : Fact (Nat.Prime (0 + p' + 1))<VAR>x : ℤ_[0 + p' + 1]<GOAL>(↑x.zmodRepr).cast = ↑x.zmodRepr
<VAR>r : ℚ<VAR>p' : ℕ<VAR>hp_prime : Fact (Nat.Prime (0 + p' + 1))<VAR>x : ℤ_[0 + p' + 1]<GOAL>↑(↑x.zmodRepr).val = ↑x.zmodRepr
<VAR>r : ℚ<VAR>p' : ℕ<VAR>hp_prime : Fact (Nat.Prime (0 + p' + 1))<VAR>x : ℤ_[0 + p' + 1]<GOAL>x.zmodRepr % (p' + 1) = x.zmodRepr
<VAR>r : ℚ<VAR>p' : ℕ<VAR>hp_prime : Fact (Nat.Prime (0 + p' + 1))<VAR>x : ℤ_[0 + p' + 1]<GOAL>x.zmodRepr < p' + 1
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>IsOpenImmersion x✝ ↔ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f) x✝
<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>a b c : E<GOAL>‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h0 : a ≠ 0<VAR>hI : a ≠ ⊤<GOAL>a * (b / a) = b
<VAR>m n a b c d : ℤ<GOAL>a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x < 1<GOAL>rexp x ≤ 1 / (1 - x)
<VAR>h1 : 0 ≤ 0<VAR>h2 : 0 < 1<GOAL>rexp 0 ≤ 1 / (1 - 0)
<VAR>x : ℝ<VAR>h1✝ : 0 ≤ x<VAR>h2 : x < 1<VAR>h1 : 0 < x<GOAL>rexp x ≤ 1 / (1 - x)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<GOAL>{K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₁ : {w | w.IsReal}.Nonempty<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<GOAL>∃ x ∈ ⋃ f, ⋃ (_ : f.natDegree ≤ D ∧ ∀ (i : ℕ), f.coeff i ∈ Set.Icc (-↑C) ↑C), ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset, ↑⟨K, hK₀⟩ = ℚ⟮x⟯
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₁ : {w | w.IsReal}.Nonempty<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<GOAL>∃ x, (∃ i, ∃ (_ : i.natDegree ≤ D ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Set.Icc (-↑C) ↑C), x ∈ ↑(Polynomial.map (algebraMap ℤ A) i).roots.toFinset) ∧ K = ℚ⟮x⟯
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsReal}<GOAL>minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this✝ : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsReal}<VAR>this : 1 ≤ convexBodyLTFactor ↥K<GOAL>minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this✝ : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsReal}<VAR>this : 1 ≤ convexBodyLTFactor ↥K<GOAL>minkowskiBound (↥K) 1 = (fun x => x * minkowskiBound (↥↑⟨K, hK₀⟩) 1) ↑1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h1 : f ∣ g<VAR>h2 : g ≠ 0<GOAL>f.natSepDegree ≤ g.natSepDegree
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h1 : f ∣ g<VAR>h2 : g ≠ 0<GOAL>(f.aroots (AlgebraicClosure F)).toFinset.card ≤ (g.aroots (AlgebraicClosure F)).toFinset.card
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>Scheme.Hom.app f U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>(Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>(↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π<GOAL>(↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π<GOAL>cos ↑θ + sin ↑θ * I = cos ↑(toIocMod Real.two_pi_pos (-π) θ) + sin ↑(toIocMod Real.two_pi_pos (-π) θ) * I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a b c : α<GOAL>￢⊤ = ⊥
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<GOAL>Tendsto (fun n => setToFun μ T hT (fs n)) l (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<GOAL>∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<GOAL>Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<GOAL>Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<GOAL>Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}<GOAL>Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}<GOAL>Tendsto (fun n => ((fun n => setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}<GOAL>∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}<GOAL>∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs (x (n + k)) a) atTop (𝓝 (f a))
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x : ℤ<GOAL>↑x = mk K p (0, ↑x)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>a✝ : ℕ<GOAL>-mk K p (0, ↑(a✝ + 1)) = mk K p (0, -↑(a✝ + 1))
<VAR>n x y p : ℕ<VAR>hp : Prime p<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<GOAL>x * y = p ^ 2 ↔ x = p ∧ y = p
<VAR>n x y p : ℕ<VAR>hp : Prime p<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<GOAL>x = p ∧ y = p
<VAR>n x y p : ℕ<VAR>hp : Prime p<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>pdvdxy : p ∣ x * y<GOAL>x = p ∧ y = p
<VAR>n x y p : ℕ<VAR>hp : Prime p<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>pdvdxy : p ∣ x * y<GOAL>∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
<VAR>n x✝ y✝ p : ℕ<VAR>hp : Prime p<VAR>hx✝ : x✝ ≠ 1<VAR>hy✝ : y✝ ≠ 1<VAR>h✝ : x✝ * y✝ = p ^ 2<VAR>pdvdxy : p ∣ x✝ * y✝<VAR>x y : ℕ<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>a : ℕ<VAR>ha : x = p * a<GOAL>x = p ∧ y = p
<VAR>n x✝ y✝ p : ℕ<VAR>hp : Prime p<VAR>hx✝ : x✝ ≠ 1<VAR>hy✝ : y✝ ≠ 1<VAR>h✝ : x✝ * y✝ = p ^ 2<VAR>pdvdxy : p ∣ x✝ * y✝<VAR>x y : ℕ<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>a : ℕ<VAR>ha : x = p * a<VAR>this : a ∣ p<GOAL>x = p ∧ y = p
<VAR>n x✝ y✝ p : ℕ<VAR>hp : Prime p<VAR>hx✝ : x✝ ≠ 1<VAR>hy✝ : y✝ ≠ 1<VAR>h✝ : x✝ * y✝ = p ^ 2<VAR>pdvdxy : p ∣ x✝ * y✝<VAR>x y : ℕ<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>a : ℕ<VAR>ha : x = p * a<VAR>this : a ∣ p<VAR>ha1 : a = 1<GOAL>x = p ∧ y = p
<VAR>n x✝ y✝ p : ℕ<VAR>hp : Prime p<VAR>hx✝ : x✝ ≠ 1<VAR>hy✝ : y✝ ≠ 1<VAR>h✝ : x✝ * y✝ = p ^ 2<VAR>pdvdxy : p ∣ x✝ * y✝<VAR>x y : ℕ<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>h : x * y = p ^ 2<VAR>a : ℕ<VAR>ha : x = p * a<VAR>this : a ∣ p<VAR>hap : a = p<GOAL>x = p ∧ y = p
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>y : R<VAR>hy : y ∈ ↑N<GOAL>IsUnit ((algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩)