ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>f g : ℕ → R<VAR>hf : ∀ (n : ℕ), 0 < n → f n ≠ 0<VAR>hg : ∀ (n : ℕ), 0 < n → g n ≠ 0<VAR>n : ℕ<VAR>hn : n > 0<GOAL>(∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 = if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔ ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ √(2 * ↑n) * 4 ^ (2 * ↑n / 3)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>h1 : IsWeaklyRegular M [a, b]<VAR>h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥<GOAL>IsWeaklyRegular M [b, a]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>h1 : IsSMulRegular M a ∧ IsSMulRegular (QuotSMulTop a M) b<VAR>h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥<GOAL>IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥<VAR>ha : IsSMulRegular M a<VAR>hb : IsSMulRegular (QuotSMulTop a M) b<GOAL>IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b<VAR>ha : IsSMulRegular M a<VAR>hb : IsSMulRegular (QuotSMulTop a M) b<GOAL>IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b<VAR>ha : IsSMulRegular M a<VAR>hb : IsSMulRegular (QuotSMulTop a M) b<GOAL>torsionBy R M b ≤ a • torsionBy R M b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>a b : R<VAR>ha : IsSMulRegular M a<VAR>hb : IsSMulRegular (QuotSMulTop a M) b<VAR>h2 : IsSMulRegular M b<GOAL>IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>2 ^ (n + 1) = 2 ^ n + 2 ^ n
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∃ P, IsAssociatedPrime P M ∧ (Submodule.span R {x}).annihilator ≤ P
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<GOAL>∃ P, IsAssociatedPrime P M ∧ (Submodule.span R {x}).annihilator ≤ P
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<GOAL>∃ P, IsAssociatedPrime P M ∧ (Submodule.span R {x}).annihilator ≤ P
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : a * b ∈ (Submodule.span R {y}).annihilator<GOAL>a ∈ (Submodule.span R {y}).annihilator ∨ b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : a * b ∈ (Submodule.span R {y}).annihilator<GOAL>a ∉ (Submodule.span R {y}).annihilator → b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : a * b ∈ (Submodule.span R {y}).annihilator<VAR>ha : a ∉ (Submodule.span R {y}).annihilator<GOAL>b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : (a * b) • y = 0<VAR>ha : ¬a • y = 0<GOAL>b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : (a * b) • y = 0<VAR>ha : ¬a • y = 0<VAR>H₁ : (Submodule.span R {y}).annihilator ≤ (Submodule.span R {a • y}).annihilator<GOAL>b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<VAR>this : (Submodule.span R {x}).annihilator ≠ ⊤<VAR>y : M<VAR>h₃ : ∀ I ∈ {P | (Submodule.span R {x}).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = (Submodule.span R {y}).annihilator}, ¬(Submodule.span R {y}).annihilator < I<VAR>l : (Submodule.span R {x}).annihilator ≤ (Submodule.span R {y}).annihilator<VAR>h₁ : (Submodule.span R {y}).annihilator ≠ ⊤<VAR>a b : R<VAR>hab : (a * b) • y = 0<VAR>ha : ¬a • y = 0<VAR>H₁ : (Submodule.span R {y}).annihilator ≤ (Submodule.span R {a • y}).annihilator<VAR>H₂ : (Submodule.span R {a • y}).annihilator ≠ ⊤<GOAL>b ∈ (Submodule.span R {y}).annihilator
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<GOAL>IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<GOAL>∀ (P : Ideal S), P.IsPrime → P.jacobson = P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP' : P'.IsPrime<GOAL>P'.jacobson ≤ P'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<GOAL>P'.jacobson ≤ P'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<GOAL>P'.jacobson ≤ P'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<GOAL>comap (algebraMap R S) P'.jacobson ≤ comap (algebraMap R S) P'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<VAR>this : sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P'<GOAL>comap (algebraMap R S) P'.jacobson ≤ comap (algebraMap R S) P'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<VAR>this : sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P'<GOAL>comap (algebraMap R S) P'.jacobson ≤ sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<VAR>this : sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P'<GOAL>⨅ I ∈ comap (algebraMap R S) '' {J | P' ≤ J ∧ J.IsMaximal}, I ≤ ⨅ a ∈ {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}, a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I✝ : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<VAR>this : sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P'<VAR>I : Ideal R<VAR>hI : I ∈ {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}<GOAL>map (algebraMap R S) I ∈ {J | P' ≤ J ∧ J.IsMaximal}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I✝ : Ideal R<VAR>y : R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Away y S<VAR>H : IsJacobson R<VAR>P' : Ideal S<VAR>hP'✝ : P'.IsPrime<VAR>hP' : (comap (algebraMap R S) P').IsPrime<VAR>hPM : Disjoint ↑(powers y) ↑(comap (algebraMap R S) P')<VAR>hP : (comap (algebraMap R S) P').jacobson = comap (algebraMap R S) P'<VAR>this : sInf {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P'<VAR>I : Ideal R<VAR>hI : I ∈ {I | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}<GOAL>comap (algebraMap R S) (map (algebraMap R S) I) = I
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>(corec (fun s => s.head) (fun s => s.tail.tail) s).tail = corec (fun s => s.head) (fun s => s.tail.tail) s.tail.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>(s.head :: corec (fun s => s.head) (fun s => s.tail.tail) s.tail.tail).tail = corec (fun s => s.head) (fun s => s.tail.tail) s.tail.tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<GOAL>edist x y ≤ ↑1 * edist (id x) (id y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝² : HasBinaryCoproduct X Y<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<GOAL>IsPushout 0 0 coprod.inl coprod.inr
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>S : Finset Λ<VAR>k : K<VAR>s : StAct k<VAR>q : Stmt₂<GOAL>TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>x : n → 𝕜<GOAL>(((toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ (toLin' A) x = 0
<VAR>α : Type u_1<VAR>s✝ t✝ : Set α<VAR>a : α<VAR>inst✝ : InvolutiveStar α<VAR>s t : Set α<GOAL>s⋆ ⊆ t ↔ s ⊆ t⋆
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c - c')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>Memℒp.toLp ((s.indicator fun x => c) - s.indicator fun x => c') ⋯ = Memℒp.toLp (fun a => s.indicator (fun x => c) a - s.indicator (fun x => c') a) ⋯
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>X Y : D<VAR>f f' : X ⟶ Y<GOAL>f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝 x<GOAL>↑(f.extend I).symm ⁻¹' t ∈ 𝓝 (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝 x<GOAL>t ∈ 𝓝 (↑(f.extend I).symm (↑(f.extend I) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝 x<GOAL>x ∈ (f.extend I).source
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra K 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.Finite K L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x y : L<GOAL>(LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).natDegree = finrank R M
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<GOAL>supported M R (s ∪ t) = supported M R s ⊔ supported M R t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s1<VAR>hp2 : p2 ∈ s2<GOAL>(s1 ⊔ s2).direction = s1.direction ⊔ s2.direction ⊔ Submodule.span k {p2 -ᵥ p1}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s1<VAR>hp2 : p2 ∈ s2<GOAL>(s1 ⊔ s2).direction ≤ s1.direction ⊔ s2.direction ⊔ Submodule.span k {p2 -ᵥ p1}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s1<VAR>hp2 : p2 ∈ s2<GOAL>s1.direction ⊔ s2.direction ⊔ Submodule.span k {p2 -ᵥ p1} ≤ (s1 ⊔ s2).direction
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y<VAR>y : α<GOAL>p y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y<VAR>y : α<VAR>R : ℝ<VAR>hR : R ≥ dist y x<VAR>h : ∀ z ∈ closedBall x R, p z<GOAL>p y
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : gcd a b = 0<GOAL>a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : gcd a b = 0<VAR>ca : α<VAR>ha : a = gcd a b * ca<GOAL>a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : gcd a b = 0<VAR>ca : α<VAR>ha : a = gcd a b * ca<VAR>cb : α<VAR>hb : b = gcd a b * cb<GOAL>a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : gcd a b = 0<VAR>ca : α<VAR>ha : a = 0<VAR>cb : α<VAR>hb : b = 0<GOAL>a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>x✝ : a = 0 ∧ b = 0<VAR>ha : a = 0<VAR>hb : b = 0<GOAL>gcd a b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>x✝ : a = 0 ∧ b = 0<VAR>ha : a = 0<VAR>hb : b = 0<GOAL>0 ∣ gcd 0 0
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : ℕ<VAR>x : M<GOAL>c • x = 0 → c = 0 ∨ x = 0
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : ℕ<VAR>x : M<GOAL>↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal