ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ f : α →. β<VAR>s : Set β<GOAL>f.core s = f.preimage s ∪ f.Domᶜ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>m n : Num<GOAL>↑m < ↑n ↔ m < n
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(g ⊗ inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>(μ.prod ν).mass = μ.mass * ν.mass
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>(((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ).toNNReal * (↑ν univ).toNNReal
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>(((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h✝ : IsEmpty X<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h✝ : Nonempty X<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h✝ : Nonempty X<VAR>g : Y →ᵇ ℝ<VAR>hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)<VAR>hgf : ⇑g ∘ e = ⇑f<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h✝ : Nonempty X<VAR>g : Y →ᵇ ℝ<VAR>hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)<VAR>hgf : ⇑g ∘ e = ⇑f<VAR>y : Y<VAR>xl xu : X<VAR>h : g y ∈ Icc (f xl) (f xu)<GOAL>g y ∈ t
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>w : Word M<GOAL>of ((equivPair i) w).head • ((equivPair i) w).tail = w
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂) = Q₁.tmul Q₂
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>(associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂)) = (associatedHom R) (Q₁.tmul Q₂)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₁<VAR>m₂' : M₂<GOAL>((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂)))) m₁) m₂)) m₁') m₂' = ((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₂))) m₁) m₂)) m₁') m₂'
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₁<VAR>m₂' : M₂<GOAL>(((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (((associatedHom R) (Q₁.tmul Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₁<VAR>m₂' : M₂<GOAL>((LinearMap.compl₁₂ ((associated Q₂).tmul (associated Q₁)) ↑(TensorProduct.comm R M₁ M₂) ↑(TensorProduct.comm R M₁ M₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (((associated Q₁).tmul (associated Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>ι₁ : Type u₁<VAR>inst✝⁴ : DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)<VAR>inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<GOAL>(f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>ι₁ : Type u₁<VAR>inst✝⁴ : DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)<VAR>inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<VAR>this : ∀ (i₁ : ι), (f.sum fun i b => (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0<GOAL>(f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support
<VAR>n : Int<VAR>d a : Nat<VAR>a0 : a ≠ 0<GOAL>mkRat (n * ↑a) (d * a) = mkRat n d
<VAR>n : Int<VAR>d a : Nat<VAR>a0 : a ≠ 0<GOAL>mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => g / h) μ μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => g * h⁻¹) μ μ
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m m✝ : (i : ι) → E i<VAR>i✝ : ι<VAR>h : ‖m✝ i✝‖ = 0<GOAL>‖f m✝‖ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁ : dist p₁ c₁ = dist p₂ c₁<VAR>hc₂ : dist p₁ c₂ = dist p₂ c₂<GOAL>⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁ : dist p₁ c₁ = dist p₂ c₁<VAR>hc₂ : dist p₁ c₂ = dist p₂ c₂<GOAL>c₂ -ᵥ c₁ ∈ (perpBisector p₁ p₂).direction
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>inst✝ : Subsingleton α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s = univ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>a /ₚ u - b /ₚ u = (a - b) /ₚ u
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>J ∈ πi (π.biUnionIndex πi J)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<GOAL>UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>x : α<GOAL>‖{x | max C 1 ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯) x‖ ≤ ‖{x | C ≤ ‖g i x‖₊}.indicator (g i) x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>x : α<GOAL>{x | max C 1 ≤ ‖Exists.choose ⋯ x‖₊}.indicator (fun a => ‖Exists.choose ⋯ a‖) x ≤ {x | C ≤ ‖g i x‖₊}.indicator (fun a => ‖g i a‖) x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b * a < b * b⁻¹ ↔ b * a < 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>h : finrank K V₂ < finrank K V<GOAL>ker f ≠ ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>h : finrank K V₂ < finrank K V<VAR>h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V<GOAL>ker f ≠ ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>h : finrank K V₂ < finrank K V<VAR>h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V<VAR>h₂ : finrank K ↥(range f) ≤ finrank K V₂<GOAL>ker f ≠ ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>h : finrank K V₂ < finrank K V<VAR>h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V<VAR>h₂ : finrank K ↥(range f) ≤ finrank K V₂<GOAL>0 < finrank K ↥(ker f)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>s₂.tail.get n = s₂.get n.succ
<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 + g).neLocus f = g.support
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>hgauge : gauge s x < 1<GOAL>∃ y ∈ s, x ∈ openSegment ℝ 0 y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>a : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>y : E<VAR>hy : y ∈ s<VAR>hgauge : gauge s ((fun x => r • x) y) < 1<GOAL>∃ y_1 ∈ s, (fun x => r • x) y ∈ openSegment ℝ 0 y_1
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x c : ℂ<VAR>h : x ∈ slitPlane<GOAL>HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S = 1 ∨ FermatLastTheoremForThreeGen.Solution.u₄ S = -1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>h : λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S = 1 ∨ FermatLastTheoremForThreeGen.Solution.u₄ S = -1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>h : λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>X : 𝓞 K<VAR>hX : ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * X<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>X : 𝓞 K<VAR>hX : ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * X<VAR>Y : 𝓞 K<VAR>hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y<VAR>Z : 𝓞 K<VAR>hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>X : 𝓞 K<VAR>hX : ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * X<VAR>Y : 𝓞 K<VAR>hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y<VAR>Z : 𝓞 K<VAR>hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>X : 𝓞 K<VAR>hX : ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * X<VAR>Y : 𝓞 K<VAR>hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y<VAR>Z : 𝓞 K<VAR>hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>this : λ ^ 2 ∣ λ ^ 4<VAR>X : 𝓞 K<VAR>hX : ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * X<VAR>Y : 𝓞 K<VAR>hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y<VAR>Z : 𝓞 K<VAR>hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z<GOAL>∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<GOAL>μ s = μ.mass * μ.normalize s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>s : Set Ω<GOAL>0 s = mass 0 * (normalize 0) s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<VAR>h : μ ≠ 0<GOAL>μ s = μ.mass * μ.normalize s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<VAR>h : μ ≠ 0<VAR>mass_nonzero : μ.mass ≠ 0<GOAL>μ s = μ.mass * μ.normalize s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<VAR>h : μ ≠ 0<VAR>mass_nonzero : μ.mass ≠ 0<GOAL>μ s = μ.mass * ⟨↑(μ.mass⁻¹ • μ), ⋯⟩ s
<VAR>D : GlueData<VAR>i j : D.J<GOAL>⇑(D.ι j) ⁻¹' Set.range ⇑(D.ι i) = Set.range ⇑(D.f j i)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l₁ l₂✝ : List α<VAR>a b : α<VAR>l₂ l₃ : List α<VAR>h : Chain' R (l₂ ++ l₁ ++ l₃)<GOAL>Chain' R l₁
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a✝ b✝ : ValueGroup A K<VAR>a b : K<GOAL>Quot.mk Setoid.r a ≤ Quot.mk Setoid.r b ∨ Quot.mk Setoid.r b ≤ Quot.mk Setoid.r a
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b✝ : ValueGroup A K<VAR>b : K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r b ∨ Quot.mk Setoid.r b ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b : ValueGroup A K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<VAR>xb yb : A<VAR>hyb : yb ∈ nonZeroDivisors A<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ∨ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)