ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * ↑((1 / x) ^ P.k)) = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * (↑(x ^ P.k))⁻¹) = 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<GOAL>Unbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s✝ : Finset ι<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable<VAR>h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)<VAR>h2 : ∀ x ∈ insert a s, (f x).Separable<GOAL>(∏ x ∈ insert a s, f x).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s✝ : Finset ι<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable<VAR>h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable<VAR>h1 : ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧ (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)<GOAL>(∏ x ∈ insert a s, f x).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s✝ : Finset ι<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable<VAR>h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable<VAR>h1 : ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧ (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)<GOAL>(f a * ∏ x ∈ s, f x).Separable
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Represents b A f<VAR>h' : Represents b A' f'<GOAL>((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.total R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap) (A * A') = (PiToModule.fromEnd R b) (f * f')
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Represents b A f<VAR>h' : Represents b A' f'<GOAL>((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.total R R) b)) (algEquivMatrix'.symm A * algEquivMatrix'.symm A') = (PiToModule.fromEnd R b) (f * f')
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Represents b A f<VAR>h' : Represents b A' f'<VAR>i✝ : ι<GOAL>((Fintype.total R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) = f (f' (((Fintype.total R R) b) (Pi.single i✝ 1)))
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Represents b A f<VAR>h' : Represents b A' f'<VAR>i✝ : ι<GOAL>((Fintype.total R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) = ((Fintype.total R R) b) (A *ᵥ A' *ᵥ Pi.single i✝ 1)
<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>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<GOAL>Tendsto (fun n => Memℒp.toLp (f n) ⋯) fi (𝓝 (Memℒp.toLp f_lim f_lim_ℒp)) ↔ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) fi (𝓝 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>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<GOAL>Tendsto (fun n => eLpNorm (↑↑(Memℒp.toLp (f n) ⋯) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) fi (𝓝 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>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<VAR>n : ι<GOAL>eLpNorm (↑↑(Memℒp.toLp (f n) ⋯) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ = eLpNorm (f n - f_lim) 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>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<VAR>n : ι<GOAL>↑↑(Memℒp.toLp (f n) ⋯) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp) =ᶠ[ae μ] f n - f_lim
<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>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<VAR>n : ι<VAR>a✝ : α<VAR>hx₁ : ↑↑(Memℒp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝<VAR>hx₂ : ↑↑(Memℒp.toLp (f n) ⋯ - Memℒp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(Memℒp.toLp (f n) ⋯) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝<GOAL>(↑↑(Memℒp.toLp (f n) ⋯) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>H₁ : ∀ a' ∈ l, R a a'<VAR>H₂ : Pairwise R l<GOAL>Pairwise (Lex (swap R)) (a :: l).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>H₁ : ∀ a' ∈ l, R a a'<VAR>H₂ : Pairwise R l<GOAL>Pairwise (Lex (swap R)) l.sublists' ∧ Pairwise (fun a_1 b => Lex (swap R) (a :: a_1) (a :: b)) l.sublists' ∧ ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>H₁ : ∀ a' ∈ l, R a a'<VAR>H₂ : Pairwise R l<GOAL>∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>H₁ : ∀ a' ∈ l, R a a'<VAR>H₂ : Pairwise R l<VAR>l₂ : List α<VAR>a✝ : l₂ <+ l<VAR>b : α<VAR>l₁ : List α<VAR>sl₁ : b :: l₁ <+ l<GOAL>Lex (swap R) (b :: l₁) (a :: l₂)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<GOAL>Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<GOAL>∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<VAR>L₁✝ L₂✝ : List (α × Bool)<VAR>x✝ : α<VAR>b✝ : Bool<VAR>eq : [(x1, !b1), (x2, b2)] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝<GOAL>False
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<VAR>L₁✝ L₂✝ : List (α × Bool)<VAR>x✝ : α<VAR>b✝ : Bool<VAR>eq : L₁✝ = [] ∧ (x✝ = x1 ∧ b✝ = !b1) ∧ (x✝ = x2 ∧ (!b✝) = b2) ∧ L₂✝ = []<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁ ≤ N₂<VAR>m : M<VAR>hm : m ∈ N₁.normalizer<GOAL>m ∈ N₂.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁ ≤ N₂<VAR>m : M<VAR>hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁<GOAL>∀ (x : L), ⁅x, m⁆ ∈ N₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<VAR>B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<VAR>B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s<VAR>this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<VAR>B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s<VAR>this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>hij : i ≠ j<VAR>x : α<VAR>hxi : f^[i] x ∈ s<VAR>hxj : f^[j] x ∈ s<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<VAR>B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s<VAR>this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)<VAR>x : α<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>hij : i ≠ j<VAR>hxi : f^[i] x ∈ s<VAR>hxj : f^[j] x ∈ s<VAR>hlt : i < j<GOAL>∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>hvol : μ univ < ↑n * μ s<VAR>A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ<VAR>B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s<VAR>this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)<VAR>x : α<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>hij : i ≠ j<VAR>hxi : f^[i] x ∈ s<VAR>hxj : f^[j] x ∈ s<VAR>hlt : i < j<GOAL>f^[j - i] (f^[i] x) ∈ s
<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>k : ℕ<VAR>x✝ : 2 ≤ k + 2<GOAL>n.descFactorial (k + 2) < n ^ (k + 2)
<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>k : ℕ<VAR>x✝ : 2 ≤ k + 2<GOAL>n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : s.card = t.card<GOAL>(fun x => x + t.card) (s \ t).card = (fun x => x + t.card) (t \ s).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)<GOAL>∀ (n : ℕ), AEMeasurable (fun a => ENNReal.ofReal ‖F n a - f a‖) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)<GOAL>∫⁻ (a : α), b a ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)<VAR>hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f g : X → ℝ<VAR>s t : Set X<VAR>hf✝ : IntegrableOn f s μ<VAR>hg : IntegrableOn g s μ<VAR>c : ℝ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>hf : ∀ x ∈ s, c ≤ f x<VAR>hfint : IntegrableOn (fun x => f x) s μ<GOAL>c * (μ s).toReal ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f g : X → ℝ<VAR>s t : Set X<VAR>hf✝ : IntegrableOn f s μ<VAR>hg : IntegrableOn g s μ<VAR>c : ℝ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>hf : ∀ x ∈ s, c ≤ f x<VAR>hfint : IntegrableOn (fun x => f x) s μ<GOAL>∫ (x : X) in s, c ∂μ ≤ ∫ (x : X) in s, f x ∂μ
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>f.neLocus (f + g) = g.support
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle (-x) y = o.oangle x y + ↑π
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑((-o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.kahler x) y ≠ 0
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>α β : Type u<VAR>f : β ⟶ α<VAR>s : S.obj (op α)<VAR>x : β<GOAL>eval S β (S.map f.op s) x = eval S α s (f x)
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>α β : Type u<VAR>f : β ⟶ α<VAR>s : S.obj (op α)<VAR>x : β<GOAL>S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>inst✝ : Fintype ι<VAR>f : ι → Set α<VAR>a : α<GOAL>a ∈ ∏ i : ι, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>inst✝ : Fintype ι<VAR>f : ι → Set α<VAR>a : α<GOAL>(∃ g, ∃ (_ : ∀ {i : ι}, i ∈ Finset.univ → g i ∈ f i), ∏ i : ι, g i = a) ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a