ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>G.edgeFinset.card = 3 * (G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>G.edgeFinset.card ≤ 3 * (G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>G.edgeFinset.card * 1 ≤ (G.cliqueFinset 3).card * 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>∀ a ∈ G.edgeFinset, 1 ≤ (bipartiteAbove (fun e s => e ∈ s.sym2) (G.cliqueFinset 3) a).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>∀ b ∈ G.cliqueFinset 3, (bipartiteBelow (fun e s => e ∈ s.sym2) G.edgeFinset b).card ≤ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>∀ (b : Finset α) (x x_1 x_2 : α), G.Adj x x_1 → G.Adj x x_2 → G.Adj x_1 x_2 → b = {x, x_1, x_2} → (bipartiteBelow (fun e s => e ∈ s.sym2) G.edgeFinset b).card ≤ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<VAR>a b c : α<VAR>hab : G.Adj a b<VAR>hac : G.Adj a c<VAR>hbc : G.Adj b c<GOAL>(bipartiteBelow (fun e s => e ∈ s.sym2) G.edgeFinset {a, b, c}).card ≤ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<VAR>a b c : α<VAR>hab : G.Adj a b<VAR>hac : G.Adj a c<VAR>hbc : G.Adj b c<GOAL>bipartiteBelow (fun e s => e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.LocallyLinear<VAR>a b c : α<VAR>hab : G.Adj a b<VAR>hac : G.Adj a c<VAR>hbc : G.Adj b c<GOAL>∀ (x y : α), G.Adj x y → x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l L : List M<GOAL>Monotone fun i => (take i L).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l L : List M<VAR>n : ℕ<GOAL>(take n L).prod ≤ (take (n + 1) L).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l L : List M<VAR>n : ℕ<VAR>h : n < L.length<GOAL>(take n L).prod ≤ (take (n + 1) L).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l L : List M<VAR>n : ℕ<VAR>h : L.length ≤ n<GOAL>(take n L).prod ≤ (take (n + 1) L).prod
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|a| = a ↔ 0 ≤ a
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a.re * b.imI + a.imI * b.re - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I : Ideal A<GOAL>I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<GOAL>(fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne : (Multiset.map asIdeal Wx).prod ≠ ⊥<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥<VAR>Wy : Multiset (PrimeSpectrum A)<VAR>h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + span A {y}<VAR>h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥<VAR>Wy : Multiset (PrimeSpectrum A)<VAR>h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + span A {y}<VAR>h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥<GOAL>(Multiset.map asIdeal (Wx + Wy)).prod ≤ M ∧ (Multiset.map asIdeal (Wx + Wy)).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥<VAR>Wy : Multiset (PrimeSpectrum A)<VAR>h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + span A {y}<VAR>h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥<GOAL>(Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥<VAR>Wy : Multiset (PrimeSpectrum A)<VAR>h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + span A {y}<VAR>h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥<GOAL>(M + span A {x}) * (M + span A {y}) ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I M : Ideal A<VAR>hgt : ∀ J > M, (fun I => I ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥) J<VAR>h_nzM : M ≠ ⊥<VAR>hA_nont : Nontrivial A<VAR>h_topM : ¬M = ⊤<VAR>h_prM : ¬M.IsPrime<VAR>x : A<VAR>hx : x ∉ M<VAR>y : A<VAR>hy : y ∉ M<VAR>h_xy : x * y ∈ M<VAR>lt_add : ∀ z ∉ M, M < M + span A {z}<VAR>Wx : Multiset (PrimeSpectrum A)<VAR>h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + span A {x}<VAR>h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥<VAR>Wy : Multiset (PrimeSpectrum A)<VAR>h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + span A {y}<VAR>h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥<GOAL>¬((Multiset.map asIdeal Wx).prod = ⊥ ∨ (Multiset.map asIdeal Wy).prod = ⊥)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<GOAL>∃ p_1 ≤ p ^ k, ∃ k_1 ≤ p ^ k, Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<GOAL>p ≤ p ^ k
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<GOAL>p ^ 1 ≤ p ^ k
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>(hasseDeriv n) p = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<VAR>x : ℕ<VAR>hx : x ∈ p.support<GOAL>(monomial (x - n)) (↑(x.choose n) * p.coeff x) = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n m : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hn : n ≠ 0<GOAL>x ^ n + y ^ n ≤ (x + y) ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>m : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>k : ℕ<VAR>hn : k + 1 ≠ 0<GOAL>x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
<VAR>S : SSet<VAR>inst✝ : S.Quasicategory<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h0 : 0 < i<VAR>hn : i < Fin.last n<VAR>σ₀ : Λ[n, i] ⟶ S<GOAL>∃ σ, σ₀ = hornInclusion n i ≫ σ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<GOAL>toAffine W P = Affine.Point.some ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ∈ Iic b ∪ Icc c d ↔ x ∈ Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.isEmpty = true ↔ x✝.toString = ""
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g✝ : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g✝ : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g✝ : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε<VAR>i : ι<GOAL>eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp (𝟙 a) f).inv = (F.mapId a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom ≫ F.map₂ (λ_ f).inv
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<GOAL>a / (b * c) = a / c / b
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>I : Ideal ℤ<VAR>g : ↥I →ₗ[ℤ] A<GOAL>∃ g', ∀ (x : ℤ) (mem : x ∈ I), g' x = g ⟨x, mem⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>m : ℤ<VAR>g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A<GOAL>∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A<GOAL>∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {0}), g' x = g ⟨x, mem⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>m : ℤ<VAR>g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A<VAR>h0 : m ≠ 0<GOAL>∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>m : ℤ<VAR>g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A<VAR>h0 : m ≠ 0<VAR>gₘ : A := g ⟨m, ⋯⟩<GOAL>∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>m : ℤ<VAR>g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A<VAR>h0 : m ≠ 0<VAR>gₘ : A := g ⟨m, ⋯⟩<VAR>n : ℤ<VAR>hn : n ∈ Submodule.span ℤ {m}<GOAL>(LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) n = g ⟨n, hn⟩
<VAR>A : Type u<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisibleBy A ℤ<VAR>m : ℤ<VAR>g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A<VAR>h0 : m ≠ 0<VAR>gₘ : A := g ⟨m, ⋯⟩<VAR>n : ℤ<VAR>hn : n • m ∈ Submodule.span ℤ {m}<GOAL>(LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) (n • m) = g ⟨n • m, hn⟩
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.kahler x) y ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>¬(x = 0 ∨ y = 0)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ : ℕ<VAR>β : Type u_3<VAR>f : α → β<VAR>n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>List.sym (n + 1) (map f (x :: xs)) = map (Sym.map f) (List.sym (n + 1) (x :: xs))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ : ℕ<VAR>β : Type u_3<VAR>f : α → β<VAR>n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>map (fun p => f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ map (Sym.map f) (List.sym (n + 1) xs) = map (Sym.map f) (List.sym (n + 1) (x :: xs))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ : ℕ<VAR>β : Type u_3<VAR>f : α → β<VAR>n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>map ((fun p => f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)) = map (Sym.map f ∘ fun p => x ::ₛ p) (List.sym n (x :: xs))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ : ℕ<VAR>β : Type u_3<VAR>f : α → β<VAR>n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>s : Sym α n<GOAL>↑(((fun p => f x ::ₛ p) ∘ Sym.map f) s) = ↑((Sym.map f ∘ fun p => x ::ₛ p) s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>i : ι<GOAL>(hv.equiv hv (Equiv.refl ι)) (v i) = (LinearIsometryEquiv.refl 𝕜 E) (v i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a b✝ : α<VAR>b : ↑(Ici a)<GOAL>IsAtom b ↔ a ⋖ ↑b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a b✝ : α<VAR>b : ↑(Ici a)<GOAL>⊥ ⋖ b ↔ a ⋖ ↑b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a b✝ : α<VAR>b : ↑(Ici a)<GOAL>(range ⇑(OrderEmbedding.subtype fun c => a ≤ c)).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulZeroClass α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>0 < a • b ↔ 0 < b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = S.g ≫ x<GOAL>S.f ≫ k = 0