ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<VAR>y : ↑(Icc (x + R) (x + S))<VAR>A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)<GOAL>c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<VAR>y : ↑(Icc (x + R) (x + S))<VAR>A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)<GOAL>|↑y| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<VAR>y : ↑(Icc (x + R) (x + S))<VAR>A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)<GOAL>|↑y| = ↑y
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<VAR>y : ↑(Icc (x + R) (x + S))<VAR>A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)<GOAL>|x| = x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q f : R[X]<VAR>hf : ∀ (r : R), eval r f = 0<VAR>hfR : ↑f.natDegree < #R<GOAL>f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q f : R[X]<VAR>hf : ∀ (r : R), eval r f = 0<VAR>hfR : ↑f.natDegree < #R<VAR>hR : Finite R<GOAL>f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q f : R[X]<VAR>hf : ∀ (r : R), eval r f = 0<VAR>hfR : ↑f.natDegree < #R<VAR>hR : Infinite R<GOAL>f = 0
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ∈ slitPlane<GOAL>ContinuousAt (fun x => x.1 ^ x.2) p
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ∈ slitPlane<GOAL>ContinuousAt (fun x => cexp (Complex.log x.1 * x.2)) p
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ∈ slitPlane<GOAL>ContinuousAt (fun x => Complex.log x.1 * x.2) p
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>↑(norm (x % y)).natAbs < ↑(norm y).natAbs
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<GOAL>MinFacHelper n (k + 2)
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<GOAL>(k + 2) % 2 = 1
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<GOAL>k + 2 ≤ n.minFac
<VAR>n k' : ℕ<VAR>e : n.minFac + 2 = k'<VAR>h : MinFacHelper n n.minFac<VAR>np : n.minFac ≠ n.minFac<GOAL>n.minFac + 2 ≤ n.minFac
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<VAR>h2 : k < n.minFac<GOAL>k + 2 ≤ n.minFac
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<VAR>h2✝ : k < n.minFac<VAR>h2 : k.succ = n.minFac<GOAL>k + 2 ≤ n.minFac
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : MinFacHelper n k<VAR>np : n.minFac ≠ k<VAR>h2✝ : k < n.minFac<VAR>h2 : k.succ < n.minFac<GOAL>k + 2 ≤ n.minFac
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<GOAL>∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<VAR>hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀<GOAL>∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<VAR>hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀<GOAL>∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<VAR>hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀<VAR>n : ℕ<VAR>hn : n ≥ n₀<GOAL>n = n₀ + (n - n₀)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : CliffordAlgebra Q<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(ι Q) a * ((ι Q) b * x) = -((ι Q) b * ((ι Q) a * x))
<VAR>θ : Angle<GOAL>(θ + ↑(π / 2)).sin = θ.cos
<VAR>x✝ : ℝ<GOAL>(↑x✝ + ↑(π / 2)).sin = (↑x✝).cos
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy✝ : 0 ≤ y<VAR>hz : 0 ≤ z<VAR>hy : 0 < y<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<VAR>i : n<GOAL>(diagonal v *ᵥ Pi.single j x) i = Pi.single j (v j * x) i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<VAR>i : n<GOAL>v i * Pi.single j x i = Pi.single j (v j * x) i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<GOAL>Disjoint I (sSup ({I | IsAtom I} \ {I}))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<GOAL>sSup ({I | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<GOAL>∀ b ∈ {I | IsAtom I} \ {I}, b ≤ orthogonal Φ hΦ_inv I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<GOAL>∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<GOAL>J ≤ orthogonal Φ hΦ_inv I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<GOAL>⁅↑x, ↑y⁆ ∈ ↑(orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<GOAL>∀ n ∈ I, (Φ n) ⁅↑x, ↑y⁆ = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<VAR>z : L<VAR>hz : z ∈ I<GOAL>(Φ z) ⁅↑x, ↑y⁆ = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<VAR>z : L<VAR>hz : z ∈ I<GOAL>(Φ ⁅↑x, z⁆) ↑y = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<VAR>z : L<VAR>hz : z ∈ I<GOAL>⁅↑x, z⁆ = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<VAR>z : L<VAR>hz : z ∈ I<GOAL>⁅↑x, z⁆ ∈ J ⊓ I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : I ∈ {I | IsAtom I}<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : ¬J = I<VAR>x : ↥J<VAR>y : ↥J<VAR>z : L<VAR>hz : z ∈ I<GOAL>⁅↑x, z⁆ ∈ ⁅J, I⁆
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f (-x) = f (-x + x) - f x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f (-x) = f (-x) + f x - f x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f (-x + x) - f x = -f x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<GOAL>(latticeBasis K) i = (mixedEmbedding K) ((integralBasis K) i)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
<VAR>a b c : ℕ<VAR>P✝ : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P✝ (n + 1) → P✝ n<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>k : ℕ<VAR>hk : 1 < k<VAR>P : M → Prop<VAR>hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)<VAR>hpow : ∀ (x : M), P (x ^ k) → P x<VAR>n : ℕ<VAR>ih : ∀ (x : M), P (x ^ (n + 1)) → P x<VAR>x : M<VAR>hx : P (x ^ n)<VAR>h : P (x ^ n * x)<GOAL>P (x ^ (n + 1))
<VAR>a b c : ℕ<VAR>P✝ : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P✝ (n + 1) → P✝ n<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>k : ℕ<VAR>hk : 1 < k<VAR>P : M → Prop<VAR>hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)<VAR>hpow : ∀ (x : M), P (x ^ k) → P x<VAR>n : ℕ<VAR>ih : ∀ (x : M), P (x ^ (n + 1)) → P x<VAR>x : M<VAR>hx : P (x ^ n)<VAR>h : P (x * x ^ n)<GOAL>P (x ^ (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : v.restrict j ≤ w.restrict j<GOAL>v.restrict (i ∪ j) ≤ w.restrict (i ∪ j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : v.restrict j ≤ w.restrict j<GOAL>v.restrict (⋃ b, bif b then i else j) ≤ w.restrict (⋃ b, bif b then i else j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : v.restrict j ≤ w.restrict j<GOAL>∀ (b : Bool), MeasurableSet (bif b then i else j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : v.restrict j ≤ w.restrict j<GOAL>∀ (b : Bool), v.restrict (bif b then i else j) ≤ w.restrict (bif b then i else j)
<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>ι : Type u_3<VAR>hne : Nonempty ι<VAR>inst✝ : Finite ι<VAR>p : ι → P<VAR>ha : AffineIndependent ℝ p<GOAL>∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
<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>ι : Type u_3<VAR>hne : Nonempty ι<VAR>inst✝ : Finite ι<VAR>p : ι → P<VAR>ha : AffineIndependent ℝ p<VAR>val✝ : Fintype ι<GOAL>∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<VAR>hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)<GOAL>∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<VAR>hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)<VAR>t : R<VAR>ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹<VAR>ht' : inverse (1 - -↑x⁻¹ * t) = ∑ i ∈ range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)<GOAL>inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<VAR>hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)<VAR>t : R<VAR>ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹<VAR>ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)<GOAL>inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<VAR>hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)<VAR>t : R<VAR>ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹<VAR>ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)<GOAL>(∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasImage f✝<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>inst✝² : HasImage f<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasImage g<VAR>sq : Arrow.mk f ⟶ Arrow.mk g<VAR>inst✝ : HasImageMap sq<GOAL>imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ sq.right
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasImage f✝<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>inst✝² : HasImage f<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasImage g<VAR>sq : Arrow.mk f ⟶ Arrow.mk g<VAR>inst✝ : HasImageMap sq<GOAL>(imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = (imageSubobject f).arrow ≫ sq.right
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R (⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m})
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<VAR>z₁ : L'<VAR>h₁ : z₁ ∈ map f I₁<VAR>z₂ : L'<VAR>h₂ : z₂ ∈ map f I₂<GOAL>⁅↑⟨z₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<VAR>z₂ : L'<VAR>h₂ : z₂ ∈ map f I₂<VAR>y₁ : ↥I₁<VAR>h₁ : f ↑y₁ ∈ map f I₁<GOAL>⁅↑⟨f ↑y₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<VAR>y₁ : ↥I₁<VAR>h₁ : f ↑y₁ ∈ map f I₁<VAR>y₂ : ↥I₂<VAR>h₂ : f ↑y₂ ∈ map f I₂<GOAL>⁅↑⟨f ↑y₁, h₁⟩, ↑⟨f ↑y₂, h₂⟩⁆ ∈ ⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>Tendsto (fun n => x ^ n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>Tendsto (HPow.hPow ‖x‖) atTop (𝓝 0)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))<GOAL>Tendsto (fun a => s.sup fun x => f x a) l (𝓝 (s.sup g))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : 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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x y : L<VAR>hx : x ∈ H.normalizer<VAR>hy : y ∈ H<GOAL>⁅x, y⁆ ∈ H