ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<GOAL>0 = (a *ᵥ NumberField.house.ξ K x) k
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ r : K →+* ℂ, ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u<GOAL>0 = (a *ᵥ NumberField.house.ξ K x) k
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ y : β, ∑ x_1 : K →+* ℂ, ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u<GOAL>0 = (a *ᵥ NumberField.house.ξ K x) k
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ y : β, ∑ x_1 : K →+* ℂ, ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u<VAR>l : β<GOAL>∑ x_1 : K →+* ℂ, ↑(x (l, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l x_1 u) * (NumberField.house.newBasis K) u = (fun j => a k j) l * NumberField.house.ξ K x l
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ y : β, ∑ x_1 : K →+* ℂ, ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u<VAR>l : β<GOAL>∑ x_1 : K →+* ℂ, ↑(x (l, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l x_1 u) * (NumberField.house.newBasis K) u = ∑ i : K →+* ℂ, (fun j => a k j) l * (↑(x (l, i)) * (NumberField.house.newBasis K) i)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ y : β, ∑ x_1 : K →+* ℂ, ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u<VAR>l✝ : β<VAR>l : K →+* ℂ<GOAL>↑(x (l✝, l)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l✝ l u) * (NumberField.house.newBasis K) u = (fun j => a k j) l✝ * (↑(x (l✝, l)) * (NumberField.house.newBasis K) l)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<VAR>this✝ : 0 = ∑ u : K →+* ℂ, (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u<VAR>this : 0 = ∑ y : β, ∑ x_1 : K →+* ℂ, ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u<VAR>l✝ : β<VAR>l : K →+* ℂ<GOAL>↑(x (l✝, l)) * (a k l✝ * (NumberField.house.newBasis K) l) = (fun j => a k j) l✝ * (↑(x (l✝, l)) * (NumberField.house.newBasis K) l)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>i : X.basicOpen f ⟶ U<GOAL>IsLocalization.Away f ↑Γ(X, X.basicOpen f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>x : X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfa : f ≤ 𝓟 {x}<GOAL>𝓟 {x} ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<GOAL>(γ.trans γ').symm t = (γ'.symm.trans γ.symm) t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<GOAL>(if h : ↑(σ t) ≤ 1 / 2 then γ ⟨2 * ↑(σ t), ⋯⟩ else γ' ⟨2 * ↑(σ t) - 1, ⋯⟩) = if h : ↑t ≤ 1 / 2 then γ' (σ ⟨2 * ↑t, ⋯⟩) else γ (σ ⟨2 * ↑t - 1, ⋯⟩)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<VAR>h✝ : ↑(σ t) ≤ 1 / 2<VAR>h : 1 - ↑t ≤ 1 / 2<VAR>h₁ : ↑t ≤ 1 / 2<GOAL>γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<VAR>h✝ : ↑(σ t) ≤ 1 / 2<VAR>h : 1 - ↑t ≤ 1 / 2<VAR>h₁ : ¬↑t ≤ 1 / 2<GOAL>γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<VAR>h✝ : ¬↑(σ t) ≤ 1 / 2<VAR>h : ¬1 - ↑t ≤ 1 / 2<VAR>h₂ : ↑t ≤ 1 / 2<GOAL>γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<VAR>h✝ : ¬↑(σ t) ≤ 1 / 2<VAR>h : ¬1 - ↑t ≤ 1 / 2<VAR>h₂ : ¬↑t ≤ 1 / 2<GOAL>γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>g✝ : G<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] t<VAR>g : G<GOAL>g ∈ aestabilizer G μ s ↔ g ∈ aestabilizer G μ t
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l init tail : List α<GOAL>(init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>init tail : List α<GOAL>(init, tail) ∈ ([], []) :: [].zip [] ↔ init ++ tail = []
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>hd : α<VAR>tl : List α<VAR>ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl<VAR>init tail : List α<GOAL>(init, tail) ∈ ([], hd :: tl) :: (map (fun t => hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯<GOAL>(trace R M) (φ x ∘ₗ φ y) = (trace R ↥↑N) ((φ x ∘ₗ φ y).restrict hy')
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>hy' : optParam (∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N) ⋯<GOAL>∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ<VAR>hr : |r| < 1<GOAL>Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < π / 2<GOAL>2 / π * x < sin x
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < π / 2<GOAL>(π / 2)⁻¹ * x < sin x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Monoid R<VAR>inst✝ : HasDistribNeg R<VAR>n : ℕ<VAR>h : (-1) ^ n = -1<GOAL>(-1) ^ (n + 1) = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Monoid R<VAR>inst✝ : HasDistribNeg R<VAR>n : ℕ<VAR>h : (-1) ^ n = 1<GOAL>(-1) ^ (n + 1) = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>h : μ.HaveLebesgueDecomposition ν<GOAL>Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>h : μ.HaveLebesgueDecomposition ν<GOAL>Measurable (Classical.choose ⋯).2 ∧ (Classical.choose ⋯).1 ⟂ₘ ν ∧ μ = (Classical.choose ⋯).1 + ν.withDensity (Classical.choose ⋯).2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(_root_.latticeClosure s).Finite
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(supClosure (infClosure s)).Finite
<VAR>S : Type u_1<VAR>G : Type u_2<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : LinearOrder G<VAR>x✝ : SetLike S G<VAR>inst✝ : NegMemClass S G<VAR>H : S<VAR>x : G<GOAL>|x| ∈ H ↔ x ∈ H
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsWeakUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsWeakUpperModularLattice α<VAR>a b : α<GOAL>b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<GOAL>IsCompl W (B.orthogonal W)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>this : W ⊓ B.orthogonal W = ⊥<GOAL>IsCompl W (B.orthogonal W)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>this : W ⊓ B.orthogonal W = ⊥<GOAL>finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>this : W ⊓ B.orthogonal W = ⊥<GOAL>finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>this : W ⊓ B.orthogonal W = ⊥<GOAL>finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<VAR>H : a ≠ 0<GOAL>((monomial n) a).support = {n}
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<VAR>H : a ≠ 0<GOAL>(match { toFinsupp := Finsupp.single n a } with | { toFinsupp := p } => p.support) = {n}
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>normSq (-z) = normSq z
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g✝ : G<VAR>a✝ b : α<VAR>g : G<VAR>a : α<GOAL>g • g⁻¹ • a = a
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η✝ : Kernel α β<VAR>μ : Measure α<VAR>inst✝² : SFinite μ<VAR>κ η : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<GOAL>μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η✝ : Kernel α β<VAR>μ : Measure α<VAR>inst✝² : SFinite μ<VAR>κ η : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<GOAL>(Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ + Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) () = μ ⊗ₘ κ + μ ⊗ₘ η
<VAR>b x y : ℕ<VAR>hb : 1 < b<VAR>h : b ^ x ≤ y<GOAL>x ≤ log b y
<VAR>b x y : ℕ<VAR>hb : 1 < b<VAR>h : b ^ x ≤ y<VAR>hy : y ≠ 0<GOAL>x ≤ log b y
<VAR>b x : ℕ<VAR>hb : 1 < b<VAR>h : b ^ x ≤ 0<GOAL>x ≤ log b 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)<GOAL>∑ a ∈ s, ∑ _i ∈ t a, 1 = ∑ u ∈ s, (t u).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : IsBasis p s<VAR>U : Set α<GOAL>U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<GOAL>ω ^ e.repr ≤ (e.oadd n a).repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<GOAL>ω ^ e.repr ≤ ω ^ e.repr * ↑↑n
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<GOAL>Tendsto f atBot (𝓝 (limUnder atBot f))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<GOAL>∃ a, Tendsto f atBot (𝓝 a)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g✝ g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>g : ℝ → E := f ∘ fun x => -x<GOAL>∃ a, Tendsto f atBot (𝓝 a)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g✝ g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>g : ℝ → E := f ∘ fun x => -x<VAR>hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x<GOAL>∃ a, Tendsto f atBot (𝓝 a)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g✝ g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>g : ℝ → E := f ∘ fun x => -x<VAR>hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x<VAR>L : Tendsto g atTop (𝓝 (limUnder atTop g))<GOAL>∃ a, Tendsto f atBot (𝓝 a)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g✝ g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>g : ℝ → E := f ∘ fun x => -x<VAR>hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x<VAR>L : Tendsto g atTop (𝓝 (limUnder atTop g))<GOAL>Tendsto f atBot (𝓝 (limUnder atTop g))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g✝ g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>g : ℝ → E := f ∘ fun x => -x<VAR>hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x<VAR>L : Tendsto g atTop (𝓝 (limUnder atTop g))<VAR>this : Tendsto (fun x => g (-x)) atBot (𝓝 (limUnder atTop g))<GOAL>Tendsto f atBot (𝓝 (limUnder atTop g))
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<GOAL>normUnit X = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => r) a = (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>(cfcHom ha) { toFun := (spectrum R a).restrict fun x => r, continuous_toFun := ⋯ } = (cfcHom ha) ((algebraMap R C(↑(spectrum R a), R)) r)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ s₃ : AList β<GOAL>∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂ ∪ s₃).entries ↔ y ∈ dlookup x (s₁ ∪ (s₂ ∪ s₃)).entries
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))