ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<GOAL>(∃ z ∈ s, dist x z < ε + δ) → ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x z : E<VAR>hz : z ∈ s<VAR>hxz : dist x z < ε + δ<GOAL>∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x z : E<VAR>hz : z ∈ s<VAR>hxz : dist x z < δ + ε<GOAL>∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y✝ z✝ : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x z : E<VAR>hz : z ∈ s<VAR>hxz : dist x z < δ + ε<VAR>y : E<VAR>hxy : dist x y < ε<VAR>hyz : dist y z < δ<GOAL>∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>padicNorm p q ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>↑p ^ (-padicValRat p q) ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>↑p ≠ 0
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Bornology M<VAR>inst✝¹ : AddZeroClass E<VAR>inst✝ : DistribSMul M E<VAR>s₁ s₂ t : Set E<VAR>x : E<VAR>h₁ : Absorbent M s₁<VAR>h₂ : Absorbs M s₂ t<GOAL>Absorbs M (s₁ + s₂) (x +ᵥ t)
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Bornology M<VAR>inst✝¹ : AddZeroClass E<VAR>inst✝ : DistribSMul M E<VAR>s₁ s₂ t : Set E<VAR>x : E<VAR>h₁ : Absorbent M s₁<VAR>h₂ : Absorbs M s₂ t<GOAL>Absorbs M (s₁ + s₂) ({x} +ᵥ t)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.ΨSq ↑n).natDegree ≤ n ^ 2 - 1 ∧ (W.ΨSq ↑n).coeff (n ^ 2 - 1) = ↑(↑n ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<GOAL>(W.ΨSq ↑n).natDegree ≤ n ^ 2 - 1 ∧ (W.ΨSq ↑n).coeff (n ^ 2 - 1) = ↑(↑n ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<GOAL>(W.ΨSq ↑n).natDegree ≤ n ^ 2 - 1 ∧ (W.ΨSq ↑n).coeff (n ^ 2 - 1) = ↑(↑n ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<GOAL>(W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<GOAL>(W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<VAR>hc : (↑n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1<GOAL>(W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1) ^ 2 - 1 = 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<VAR>hc : (↑n + 1) ^ 2 = WeierstrassCurve.expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1<GOAL>((W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ 2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0) ∧ (W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff (2 * WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0) = ↑(↑(n + 1) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<GOAL>Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Inv G<VAR>inst✝⁵ : ContinuousInv G<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : Group β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousInv β<VAR>f : F<VAR>_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>ContinuousInv α
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Inv G<VAR>inst✝⁵ : ContinuousInv G<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : Group β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousInv β<VAR>f : F<VAR>_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous (⇑f ∘ fun a => a⁻¹)
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Inv G<VAR>inst✝⁵ : ContinuousInv G<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : Group β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousInv β<VAR>f : F<VAR>_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>a : α<VAR>inst✝ : Invertible a<GOAL>⅟a < 0 ↔ a < 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>f : E → F<VAR>s : Set E<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ∀ (y : E), ContDiffOn 𝕜 (↑n) (fun x => (fderivWithin 𝕜 f s x) y) s
<VAR>n : Type u<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α : Type v<VAR>inst✝² : CommRing α<VAR>inst✝¹ : StarRing α<VAR>A✝ : Matrix n n α<VAR>β : Type v<VAR>inst✝ : CommRing β<VAR>A : Matrix n n β<GOAL>A ∈ orthogonalGroup n β ↔ A * star A = 1
<VAR>n : Type u<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α : Type v<VAR>inst✝² : CommRing α<VAR>inst✝¹ : StarRing α<VAR>A✝ : Matrix n n α<VAR>β : Type v<VAR>inst✝ : CommRing β<VAR>A : Matrix n n β<VAR>hA : A * star A = 1<GOAL>star A * A = 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<GOAL>Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(lineMap z y) '' Set.Ioi 1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>↑x.order = x.orderTop
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : F<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => c - f x) (-f') x
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ n₂ : ℕ<VAR>hn : n₁ ≤ n₂<GOAL>∀ (g₁ : F[X]), g₁.Separable → (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ n₂ : ℕ<VAR>hn : n₁ ≤ n₂<VAR>hf0 : f ≠ 0<GOAL>∀ (g₁ : F[X]), g₁.Separable → (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ n₂ : ℕ<VAR>hn : n₁ ≤ n₂<VAR>hf0 : f ≠ 0<VAR>g₁ : F[X]<VAR>hg₁ : g₁.Separable<VAR>hgf₁ : (expand F (p ^ n₁)) g₁ = f<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>hgf₂ : (expand F (p ^ n₂)) g₂ = f<GOAL>n₁ = n₂ ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ n₂ : ℕ<VAR>hn : ∃ c, n₂ = n₁ + c<VAR>hf0 : f ≠ 0<VAR>g₁ : F[X]<VAR>hg₁ : g₁.Separable<VAR>hgf₁ : (expand F (p ^ n₁)) g₁ = f<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>hgf₂ : (expand F (p ^ n₂)) g₂ = f<GOAL>n₁ = n₂ ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>hf0 : f ≠ 0<VAR>g₁ : F[X]<VAR>hg₁ : g₁.Separable<VAR>hgf₁ : (expand F (p ^ n₁)) g₁ = f<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>k : ℕ<VAR>hgf₂ : (expand F (p ^ (n₁ + k))) g₂ = f<GOAL>n₁ = n₁ + k ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>hf0 : f ≠ 0<VAR>g₁ : F[X]<VAR>hg₁ : g₁.Separable<VAR>hgf₁ : (expand F (p ^ n₁)) g₁ = f<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>k : ℕ<VAR>hgf₂ : (expand F (p ^ k)) g₂ = g₁<GOAL>n₁ = n₁ + k ∧ g₁ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>k : ℕ<VAR>hg₁ : ((expand F (p ^ k)) g₂).Separable<VAR>hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))<VAR>hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) ≠ 0<GOAL>n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>k : ℕ<VAR>hg₁ : ((expand F (p ^ k)) g₂).Separable<VAR>hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))<VAR>hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) ≠ 0<VAR>h : IsUnit g₂<GOAL>n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
<VAR>F✝ : Type u<VAR>inst✝¹ : Field F✝<VAR>p✝ : ℕ<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : 0 < p<VAR>n₁ : ℕ<VAR>g₂ : F[X]<VAR>hg₂ : g₂.Separable<VAR>hg₁ : ((expand F (p ^ 0)) g₂).Separable<VAR>hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))<VAR>hf0 : (expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂) ≠ 0<GOAL>n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) g₂ = g₂
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x < 0<GOAL>b ^ logb b x = -x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x < 0<GOAL>|x| = -x
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>s : Multiset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hp : P.IsPrime<GOAL>(Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y v₁ v₂ : M<VAR>h✝ : SameRay R x y<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>r₁ r₂ : R<VAR>hr₁ : 0 < r₁<VAR>hr₂ : 0 < r₂<VAR>h : r₁ • x = r₂ • y<GOAL>(r₂⁻¹ * r₁) • x = y
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>x✝ : ι<GOAL>(b.repr (fract b (fract b m))) x✝ = (b.repr (fract b m)) x✝
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>u v : ↑(sphere 0 1)<GOAL>u = v ↔ ⟪↑u, ↑v⟫_ℝ = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<VAR>h : a ≤ b<GOAL>a ∆ b = b \ a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁸ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Type u_9<VAR>inst✝³ : Monoid S<VAR>inst✝² : SMul S R<VAR>inst✝¹ : MulAction S M<VAR>inst✝ : IsScalarTower S R M<VAR>r : S<VAR>x : M<GOAL>span R {r • x} ≤ span R {x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁸ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Type u_9<VAR>inst✝³ : Monoid S<VAR>inst✝² : SMul S R<VAR>inst✝¹ : MulAction S M<VAR>inst✝ : IsScalarTower S R M<VAR>r : S<VAR>x : M<GOAL>r • x ∈ span R {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤<VAR>hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => |x i|<GOAL>∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤<VAR>hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l x ∨ ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l x<GOAL>∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>x : ℤ<GOAL>x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ x ∈ Ideal.span {↑(addOrderOf a)}
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>((F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.inv) ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f) = (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app Q.complex ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv = (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app Q.complex ≫ (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>p : α → Prop<VAR>hp : ComputablePred p<GOAL>ComputablePred fun a => ¬p a
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>f : α → Bool<VAR>hf : Computable f<VAR>hp : ComputablePred fun a => f a = true<GOAL>ComputablePred fun a => ¬(fun a => f a = true) a
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝² : HasSmallLocalizedHom W X X<VAR>inst✝¹ : HasSmallLocalizedHom W X Y<VAR>inst✝ : HasSmallLocalizedHom W Y X<VAR>f : Y ⟶ X<VAR>hf : W f<GOAL>(equiv W W.Q) ((mkInv f hf).comp (mk W f)) = (equiv W W.Q) (mk W (𝟙 X))
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b' b₁ b₂ b₃ c₁ c₂ : R<VAR>k : ℕ<GOAL>a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>x y z : Finmap β<GOAL>(x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z
<VAR>n✝ : ℕ<VAR>inst✝ : NeZero (n✝ + 1)<VAR>a : ZMod (n✝ + 1)<GOAL>a.val < n✝ + 1
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin 0 → α<GOAL>∀ (i : Fin 1), vecCons x u i = x
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin 0 → α<GOAL>vecCons x u 0 = x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<GOAL>corootSpace ⇑α = ⊥ ↔ α.IsZero
<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>f : E →ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : U ⟂ V<GOAL>Submodule.comap f U ⟂ Submodule.comap f V
<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>f : E →ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫_𝕜 = 0<GOAL>∀ u ∈ Submodule.comap f U, ∀ v ∈ Submodule.comap f V, ⟪u, v⟫_𝕜 = 0
<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>f : E →ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫_𝕜 = 0<GOAL>∀ (u : E), f u ∈ U → ∀ (v : E), f v ∈ V → ⟪f u, f v⟫_𝕜 = 0
<GOAL>Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (2 + 0)⁻¹)
<VAR>n : ℕ<VAR>hn : n ≥ 1<GOAL>(2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<GOAL>Integrable (fun x => g x • f x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => g x • f x) = fun x => g x • f x<GOAL>Integrable (fun x => g x • f x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => g x • f x) = fun x => g x • f x<GOAL>Integrable (fun a => g a • K.indicator f a) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => g x • f x) = fun x => g x • f x<GOAL>Integrable (K.indicator f) μ