ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<GOAL>v ∈ (span 𝕜 {u})ᗮ ↔ ⟪v, u⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MulZeroClass M₀<VAR>a✝ b✝ a b : M₀<VAR>h : a ≠ 0 → b = 0<VAR>ha : a = 0<GOAL>a * b = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MulZeroClass M₀<VAR>a✝ b✝ a b : M₀<VAR>h : a ≠ 0 → b = 0<VAR>ha : ¬a = 0<GOAL>a * b = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>hR : HasUnitMulPowIrreducibleFactorization R<VAR>inst✝ : IsDomain R<VAR>p : R := Classical.choose hR<VAR>spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := Classical.choose_spec hR<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod x
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>hR : HasUnitMulPowIrreducibleFactorization R<VAR>inst✝ : IsDomain R<VAR>p : R := Classical.choose hR<VAR>spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := Classical.choose_spec hR<VAR>x : R<VAR>hx : x ≠ 0<GOAL>(∀ b ∈ Multiset.replicate (Classical.choose ⋯) p, Prime b) ∧ Associated (Multiset.replicate (Classical.choose ⋯) p).prod x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t a : α<VAR>ts : List α<VAR>ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2<GOAL>permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t a : α<VAR>ts : List α<VAR>ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2<GOAL>map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).2 = (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t a : α<VAR>ts : List α<VAR>ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2<GOAL>map (cons a) ((permutationsAux2 t [] [] ts id).2 ++ [ts ++ [t]]) = (permutationsAux2 t [] [] ts fun x => a :: x).2 ++ [a :: (ts ++ [t])]
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<GOAL>Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<GOAL>∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<GOAL>∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ<GOAL>∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ<VAR>hφpos : ∀ x ∈ s, 0 ≤ φ i x<VAR>h''i : IntegrableOn (fun x => φ i x • g x) s μ<GOAL>‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ<VAR>hφpos : ∀ x ∈ s, 0 ≤ φ i x<VAR>h''i : IntegrableOn (fun x => φ i x • g x) s μ<VAR>I : IntegrableOn (φ i) t μ<GOAL>‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε<VAR>δpos : 0 < δ<VAR>δone : δ < 1<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ<VAR>hφpos : ∀ x ∈ s, 0 ≤ φ i x<VAR>h''i : IntegrableOn (fun x => φ i x • g x) s μ<VAR>I : IntegrableOn (φ i) t μ<VAR>B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ<VAR>C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ<GOAL>‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h : a ≤ b<VAR>hf : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))<GOAL>¬AEStronglyMeasurable f (μ.restrict (Ι a b))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>0 < ↑q ↔ 0 < q
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>f : R[T;T⁻¹]<VAR>m : ℤ<VAR>a : R<GOAL>T n * (C a * T m) = C a * T m * T n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>f : R[T;T⁻¹]<VAR>m : ℤ<VAR>a : R<GOAL>AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SDiff α<VAR>a b : Part α<VAR>hab : (a \ b).Dom<GOAL>(a \ b).get hab = a.get ⋯ \ b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SDiff α<VAR>a b : Part α<VAR>hab : (a \ b).Dom<GOAL>(a.bind fun y => map (fun x => y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f✝ : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>∃ fsymm, 0 < fsymm.nnnorm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f✝ : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<VAR>C : ℝ<VAR>hC : C > 0<VAR>fsymm : F → E<VAR>h : ∀ (y : F), f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖<GOAL>∃ fsymm, 0 < fsymm.nnnorm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f✝ : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<VAR>C : ℝ<VAR>hC : C > 0<VAR>fsymm : F → E<VAR>h : ∀ (y : F), f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖<GOAL>0 < { toFun := fsymm, nnnorm := ⟨C, ⋯⟩, bound' := ⋯, right_inv' := ⋯ }.nnnorm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>X : Type u_5<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<GOAL>Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>X : Type u_5<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i<GOAL>Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>X : Type u_5<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i<VAR>nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅<GOAL>Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>X : Type u_5<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i<VAR>nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅<VAR>key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 (μ (⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i)))<GOAL>Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>X : Type u_5<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>Es : ℕ → Set X<VAR>Es_mble : ∀ (i : ℕ), MeasurableSet (Es i)<VAR>Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i<VAR>nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅<VAR>key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)<GOAL>Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>q : Stmt₁<VAR>ss : Supports M S<GOAL>some q ∈ stmts M S → SupportsStmt S q
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>q : Stmt₁<VAR>ss : Supports M S<GOAL>∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝ : Star α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X₁ X₂ : Center C<VAR>f : X₁ ⟶ X₂<VAR>Y : Center C<VAR>U : C<GOAL>f.f ▷ Y.fst ▷ U ≫ ((X₂.tensorObj Y).snd.β U).hom = ((X₁.tensorObj Y).snd.β U).hom ≫ U ◁ f.f ▷ Y.fst
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X₁ X₂ : Center C<VAR>f : X₁ ⟶ X₂<VAR>Y : Center C<VAR>U : C<GOAL>f.f ▷ Y.fst ▷ U ≫ (α_ X₂.fst Y.fst U).hom ≫ X₂.fst ◁ (Y.snd.β U).hom ≫ (α_ X₂.fst U Y.fst).inv ≫ (X₂.snd.β U).hom ▷ Y.fst ≫ (α_ U X₂.fst Y.fst).hom = ((α_ X₁.fst Y.fst U).hom ≫ X₁.fst ◁ (Y.snd.β U).hom ≫ (α_ X₁.fst U Y.fst).inv ≫ (X₁.snd.β U).hom ▷ Y.fst ≫ (α_ U X₁.fst Y.fst).hom) ≫ U ◁ f.f ▷ Y.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<VAR>s : Set β<GOAL>((κ.withDensity f) a) s = ∫⁻ (b : β) in s, f a b ∂κ a
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (j : n), 0 < ∑ i : n, A i j<GOAL>A.det ≠ 0
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (j : n), 0 < ∑ i : n, A i j<VAR>h✝ : IsEmpty n<GOAL>A.det ≠ 0
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (j : n), 0 < ∑ i : n, A i j<VAR>h✝ : Nonempty n<GOAL>A.det ≠ 0
<VAR>a b : ℕ+<GOAL>a - b ≤ a
<VAR>a b : ℕ+<GOAL>(if b < a then ↑a - ↑b else 1) ≤ ↑a
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<GOAL>∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<VAR>this : X ^ (n + 1) - C 1 = ∏ i ∈ range (n + 1), (X - C (μ ^ i * 1))<GOAL>∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<VAR>this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)<GOAL>∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<VAR>this : ∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1)) = ∑ i ∈ range (n + 1), X ^ i<GOAL>∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<VAR>this : eval 1 (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) = eval 1 (∑ i ∈ range (n + 1), X ^ i)<GOAL>∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>↑↑(condexpIndL1Fin hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm hs hμs y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>↑↑(condexpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm hs hμs y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>↑↑(condexpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x) + ↑↑(condexpIndL1Fin hm hs hμs y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>↑↑(condexpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm hs hμs y) x_1