ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K N : ℕ<VAR>hKN : K ≤ N<VAR>ρ : Measure ℝ := Measure.map X ℙ<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K N : ℕ<VAR>hKN : K ≤ N<VAR>ρ : Measure ℝ := Measure.map X ℙ<VAR>this : IsProbabilityMeasure ρ<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K N : ℕ<VAR>hKN : K ≤ N<VAR>ρ : Measure ℝ := Measure.map X ℙ<VAR>this : IsProbabilityMeasure ρ<VAR>A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K N : ℕ<VAR>hKN : K ≤ N<VAR>ρ : Measure ℝ := Measure.map X ℙ<VAR>this : IsProbabilityMeasure ρ<VAR>A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1<VAR>B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>f : MultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.castSucc<VAR>x y : M (last n)<GOAL>f (snoc m (x + y)) = f (snoc m x) + f (snoc m y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>a ε : α<VAR>hε : 0 < ε<GOAL>{x | (fun x => |x - a| < ε) x} ∈ 𝓟 {b | |a - b| < ε}
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Tendsto f (cocompact α) (𝓝 x)<VAR>r : Set (β × β)<VAR>hr : r ∈ 𝓤 β<GOAL>{x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Tendsto f (cocompact α) (𝓝 x)<VAR>r : Set (β × β)<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<GOAL>{x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Tendsto f (cocompact α) (𝓝 x)<VAR>r : Set (β × β)<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>s : Set α<VAR>hs : IsCompact s<VAR>hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}<GOAL>{x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Tendsto f (cocompact α) (𝓝 x)<VAR>r : Set (β × β)<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>s : Set α<VAR>hs : IsCompact s<VAR>hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}<GOAL>symmetrizeRel {x | x.1 ∈ s → (f x.1, f x.2) ∈ symmetrizeRel r} ⊆ {x | (f x.1, f x.2) ∈ r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Tendsto f (cocompact α) (𝓝 x)<VAR>r : Set (β × β)<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>s : Set α<VAR>hs : IsCompact s<VAR>hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}<VAR>b₁ b₂ : α<VAR>h : (b₁, b₂) ∈ symmetrizeRel {x | x.1 ∈ s → (f x.1, f x.2) ∈ symmetrizeRel r}<VAR>h₁ : b₁ ∉ s<VAR>h₂ : b₂ ∉ s<GOAL>(f (b₁, b₂).1, f (b₁, b₂).2) ∈ t ○ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<GOAL>MeasurableSet (range fun x => f ↑x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>this : PolishSpace ↑s<GOAL>MeasurableSet (range fun x => f ↑x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>this : PolishSpace ↑s<GOAL>Continuous fun x => f ↑x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>this : PolishSpace ↑s<GOAL>Injective fun x => f ↑x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : Preorder α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n a : ℕ<VAR>h1 : f n < f a<VAR>h2 : f a < f (n + 1)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a✝ : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset ι<VAR>f : ι → Finset β<VAR>a : α × β<GOAL>a ∈ interedges r s (t.biUnion f) ↔ a ∈ t.biUnion fun b => interedges r s (f b)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a✝ : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset ι<VAR>f : ι → Finset β<VAR>a : α × β<GOAL>a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2
<VAR>x : PartENat<GOAL>0 < ⊤ ↔ 1 ≤ ⊤
<VAR>x : PartENat<VAR>n : ℕ<GOAL>0 < ↑n ↔ 1 ≤ ↑n
<VAR>x : PartENat<VAR>n : ℕ<GOAL>0 < n ↔ 1 ≤ n
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>x y : M<GOAL>φ x = φ y → x = y
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>x y : M<VAR>h : ((var 0).equal (var 1)).Realize (⇑φ ∘ fun i => if i = 0 then x else y) ↔ ((var 0).equal (var 1)).Realize fun i => if i = 0 then x else y<GOAL>φ x = φ y → x = y
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>x y : M<VAR>h : Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 0) = Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 1) ↔ Term.realize (fun i => if i = 0 then x else y) (var 0) = Term.realize (fun i => if i = 0 then x else y) (var 1)<GOAL>φ x = φ y → x = y
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>x y : M<VAR>h : φ x = φ (if 2 = 1 then x else y) ↔ x = if 2 = 1 then x else y<GOAL>φ x = φ y → x = y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>(bind₁ fun b => (rename fun i => (b, i)) ((expand p) (W_ ℤ n))) Φ = (bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>(map (Int.castRingHom ℚ)) ((bind₁ fun b => (rename fun i => (b, i)) ((expand p) (W_ ℤ n))) Φ) = (map (Int.castRingHom ℚ)) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>(bind₁ fun i => (expand p) ((rename fun i_1 => (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ fun i => (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n)<GOAL>(bind₁ fun i => (expand p) ((rename fun i_1 => (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ fun i => (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (expand p) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)) = (expand p) ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))<GOAL>(bind₁ fun i => (expand p) ((rename fun i_1 => (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ fun i => (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun i => (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ fun i => (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)<GOAL>(bind₁ fun i => (expand p) ((rename fun i_1 => (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) = (bind₁ fun i => (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>(bind₁ fun i => (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) = (bind₁ fun i => (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>∀ i ∈ (W_ ℚ n).vars, i ∈ (W_ ℚ n).vars → (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) = (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>i : ℕ<VAR>hi : i ∈ (W_ ℚ n).vars<GOAL>(expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) = (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>i : ℕ<VAR>hi : i < n + 1<GOAL>(expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) = (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s t : Set α<VAR>h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s t : Set α<VAR>h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t<GOAL>s ∩ mulSupport f = t ∩ mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s t : Set α<VAR>h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t<VAR>x : α<GOAL>x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>a : R<GOAL>a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ a ∈ primitiveRoots n R
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>a : R<GOAL>a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ IsPrimitiveRoot a n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>a : R<GOAL>a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ (cyclotomic n R).IsRoot a
<VAR>f : ℝ → ℝ<VAR>c x✝¹ : ℝ<VAR>x✝ : x✝¹ ∈ Set.Ioo 0 1<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (x✝¹ * x) x, (fun x => c) u ∈ Set.Icc (1 * (fun x => c) x) (1 * (fun x => c) x)
<VAR>f : ℝ → ℝ<VAR>c x✝¹ : ℝ<VAR>x✝ : x✝¹ ∈ Set.Ioo 0 1<VAR>x : ℝ<GOAL>∀ u ∈ Set.Icc (x✝¹ * x) x, c ∈ Set.Icc (1 * c) (1 * c)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<GOAL>abs (cexp x - 1 - x) = abs (cexp x - ∑ m ∈ range 2, x ^ m / ↑m.factorial)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<GOAL>abs x ^ 2 * 1 = abs x ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Append α<VAR>a b : α<GOAL>some a ++ some b = some (a ++ b)
<VAR>x : ℝ<GOAL>Irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : a < b<GOAL>a % b = a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>m : ι → OuterMeasure β<GOAL>(map f) (⨅ i, (comap f) (m i)) = ⨅ i, (map f) ((comap f) (m i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set β<GOAL>(⨅ i, (map f) ((comap f) (m i))) s ≤ ((map f) (⨅ i, (comap f) (m i))) s
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set β<GOAL>∀ (i : ℕ → Set α), f ⁻¹' s ⊆ iUnion i → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (f '' (f ⁻¹' t n)) ≤ ∑' (n : ℕ), ⨅ i_2, (m i_2) (f '' i n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set β<VAR>t : ℕ → Set α<VAR>ht : f ⁻¹' s ⊆ iUnion t<GOAL>s ⊆ ⋃ n, f '' t n ∪ (range f)ᶜ
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set β<VAR>t : ℕ → Set α<VAR>ht : f ⁻¹' s ⊆ iUnion t<GOAL>∑' (n : ℕ), ⨅ i, (m i) (f '' (f ⁻¹' (fun n => f '' t n ∪ (range f)ᶜ) n)) ≤ ∑' (n : ℕ), ⨅ i, (m i) (f '' t n)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>L R : ListBlank Γ<GOAL>map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f : α → ℝ≥0∞<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>a : α<GOAL>f a = funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<GOAL>Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : IsEmpty ι<GOAL>Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<GOAL>Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<GOAL>Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<GOAL>Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<GOAL>∀ ε > 0, ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : dist y a < ε<GOAL>∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<GOAL>∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε