ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<VAR>m n : ℕ<VAR>hm : m • x = 0<VAR>hn : n • x = 0<GOAL>m.gcd n • x = 0
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>a b : α<VAR>m n : ℕ<VAR>hab : Commute a b<VAR>hmn : m.Coprime n<GOAL>a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
<VAR>α : Type u_1<VAR>CommGroupWithZero α<VAR>a b : α<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
<VAR>α : Type u_1<VAR>CommGroupWithZero α<VAR>m n : ℕ<VAR>hmn : m.Coprime n<VAR>a : α<GOAL>(a ^ m ∈ Set.range fun x => x ^ n) ↔ a ∈ Set.range fun x => x ^ n
<VAR>a : ℤ<GOAL>0 < a ↔ 1 ≤ a
<VAR>a : ℤ<VAR>n : ℕ<GOAL>Int.succ^[n] a = a + ↑n
<VAR>a : ℤ<VAR>n : ℕ<GOAL>Int.pred^[n] a = a - ↑n
<VAR>m n : ℤ<GOAL>m ⋖ n ↔ m + 1 = n
<VAR>z : ℤ<GOAL>z ⋖ z + 1
<VAR>P : ℤ → Prop<VAR>Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z<VAR>Hinh : ∃ z, P z<GOAL>∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
<VAR>P : ℤ → Prop<VAR>DecidablePred P<VAR>b b' : ℤ<VAR>Hb : ∀ (z : ℤ), P z → b ≤ z<VAR>Hb' : ∀ (z : ℤ), P z → b' ≤ z<VAR>Hinh : ∃ z, P z<GOAL>↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)
<VAR>P : ℤ → Prop<VAR>Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b<VAR>Hinh : ∃ z, P z<GOAL>∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
<VAR>P : ℤ → Prop<VAR>DecidablePred P<VAR>b b' : ℤ<VAR>Hb : ∀ (z : ℤ), P z → z ≤ b<VAR>Hb' : ∀ (z : ℤ), P z → z ≤ b'<VAR>Hinh : ∃ z, P z<GOAL>↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : 1 ≤ r<GOAL>Int.log b r = ↑(Nat.log b ⌊r⌋₊)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 1<GOAL>Int.log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b n : ℕ<GOAL>Int.log b ↑n = ↑(Nat.log b n)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b n : ℕ<VAR>n.AtLeastTwo<GOAL>Int.log b (OfNat.ofNat n) = ↑(Nat.log b (OfNat.ofNat n))
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<GOAL>Int.log b r = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<GOAL>Int.log b r = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>↑b ^ Int.log b r ≤ r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<GOAL>r < ↑b ^ (Int.log b r + 1)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<GOAL>Int.log b 0 = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<GOAL>Int.log b 1 = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>z : ℤ<GOAL>Int.log b (↑b ^ z) = z
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<GOAL>Int.log b r₁ ≤ Int.log b r₂
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℤ<VAR>r : R<VAR>hr : 0 < r<GOAL>r < ↑b ^ x ↔ Int.log b r < x
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℤ<VAR>r : R<VAR>hr : 0 < r<GOAL>↑b ^ x ≤ r ↔ x ≤ Int.log b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : 1 ≤ r<GOAL>Int.clog b r = ↑(Nat.clog b ⌈r⌉₊)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 1<GOAL>Int.clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<GOAL>Int.clog b r = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>Int.clog b r⁻¹ = -Int.log b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>Int.log b r⁻¹ = -Int.clog b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>-Int.log b r⁻¹ = Int.clog b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>-Int.clog b r⁻¹ = Int.log b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b n : ℕ<GOAL>Int.clog b ↑n = ↑(Nat.clog b n)
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b n : ℕ<VAR>n.AtLeastTwo<GOAL>Int.clog b (OfNat.ofNat n) = ↑(Nat.clog b (OfNat.ofNat n))
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<GOAL>Int.clog b r = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<GOAL>r ≤ ↑b ^ Int.clog b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>↑b ^ (Int.clog b r - 1) < r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<GOAL>Int.clog b 0 = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<GOAL>Int.clog b 1 = 0
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>z : ℤ<GOAL>Int.clog b (↑b ^ z) = z
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<GOAL>Int.clog b r₁ ≤ Int.clog b r₂
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℤ<VAR>r : R<VAR>hr : 0 < r<GOAL>↑b ^ x < r ↔ x < Int.clog b r
<VAR>R : Type u_1<VAR>LinearOrderedSemifield R<VAR>FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℤ<VAR>r : R<VAR>hr : 0 < r<GOAL>r ≤ ↑b ^ x ↔ Int.clog b r ≤ x
<VAR>n : ℕ<VAR>hn : Even n<GOAL>AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℤ
<GOAL>AddSubmonoid.closure (Set.range fun x => x * x) = AddSubmonoid.nonneg ℤ
<VAR>k : Type u_3<VAR>DivisionRing k<VAR>CharZero k<VAR>m n : ℤ<VAR>n_dvd : n ∣ m<GOAL>↑(m / n) = ↑m / ↑n
<VAR>k : Type u_3<VAR>DivisionRing k<VAR>CharZero k<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<GOAL>↑(↑m / ↑n) = ↑m / ↑n
<VAR>α : Type u_3<VAR>NonAssocRing α<VAR>f : ℤ →+* α<VAR>CharZero α<GOAL>Function.Injective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroupWithOne β<VAR>CharZero β<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>Function.support ↑n = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroupWithOne β<VAR>CharZero β<VAR>n : ℤ<VAR>hn : n ≠ 1<GOAL>Function.mulSupport ↑n = Set.univ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ₂Sq.natDegree ≤ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ₂Sq.coeff 3 = 4
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq.coeff 3 ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq.natDegree = 3
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>0 < W.Ψ₂Sq.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq.leadingCoeff = 4
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ₃.natDegree ≤ 4
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ₃.coeff 4 = 3
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃.coeff 4 ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃.natDegree = 4
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>0 < W.Ψ₃.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃.leadingCoeff = 3
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃ ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ₄.natDegree ≤ 6
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ₄.coeff 6 = 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄.coeff 6 ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄.natDegree = 6
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>0 < W.preΨ₄.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄.leadingCoeff = 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄ ≠ 0
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>2 * ↑(WeierstrassCurve.expDegree n) = ↑n ^ 2 - if Even n then 4 else 1
<VAR>m : ℕ<GOAL>(WeierstrassCurve.expDegree (2 * (m + 3)) = 2 * WeierstrassCurve.expDegree (m + 2) + WeierstrassCurve.expDegree (m + 3) + WeierstrassCurve.expDegree (m + 5) ∧ WeierstrassCurve.expDegree (2 * (m + 3)) = WeierstrassCurve.expDegree (m + 1) + WeierstrassCurve.expDegree (m + 3) + 2 * WeierstrassCurve.expDegree (m + 4)) ∧ (WeierstrassCurve.expDegree (2 * (m + 2) + 1) = WeierstrassCurve.expDegree (m + 4) + 3 * WeierstrassCurve.expDegree (m + 2) + if Even m then 2 * 3 else 0) ∧ WeierstrassCurve.expDegree (2 * (m + 2) + 1) = WeierstrassCurve.expDegree (m + 1) + 3 * WeierstrassCurve.expDegree (m + 3) + if Even m then 0 else 2 * 3
<VAR>n : ℕ<GOAL>↑(WeierstrassCurve.expCoeff n) = if Even n then ↑n / 2 else ↑n
<VAR>m : ℕ<GOAL>WeierstrassCurve.expCoeff (2 * (m + 3)) = WeierstrassCurve.expCoeff (m + 2) ^ 2 * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 5) - WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 4) ^ 2 ∧ WeierstrassCurve.expCoeff (2 * (m + 2) + 1) = (WeierstrassCurve.expCoeff (m + 4) * WeierstrassCurve.expCoeff (m + 2) ^ 3 * if Even m then 4 ^ 2 else 1) - WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) ^ 3 * if Even m then 1 else 4 ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.preΨ' n).natDegree ≤ (n ^ 2 - if Even n then 4 else 1) / 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ' n).natDegree = (n ^ 2 - if Even n then 4 else 1) / 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : 2 < n<VAR>h : ↑n ≠ 0<GOAL>0 < (W.preΨ' n).natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>W.preΨ' n ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ n).natDegree = (n.natAbs ^ 2 - if Even n then 4 else 1) / 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>hn : 2 < n.natAbs<VAR>h : ↑n ≠ 0<GOAL>0 < (W.preΨ n).natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>W.preΨ n ≠ 0
<VAR>R : Type u<VAR>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>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.ΨSq n).natDegree = n.natAbs ^ 2 - 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>NoZeroDivisors R<VAR>n : ℤ<VAR>hn : 1 < n.natAbs<VAR>h : ↑n ≠ 0<GOAL>0 < (W.ΨSq n).natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.ΨSq n).leadingCoeff = ↑n ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>W.ΨSq n ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.Φ n).natDegree ≤ n.natAbs ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.Φ n).coeff (n.natAbs ^ 2) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<GOAL>(W.Φ n).coeff (n.natAbs ^ 2) ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<GOAL>(W.Φ n).natDegree = n.natAbs ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>0 < (W.Φ n).natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<GOAL>(W.Φ n).leadingCoeff = 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>n : ℤ<GOAL>W.Φ n ≠ 0
<VAR>n : ℤ<GOAL>Int.sqrt (n * n) = ↑n.natAbs
<VAR>x : ℤ<GOAL>(∃ n, n * n = x) ↔ Int.sqrt x * Int.sqrt x = x
<VAR>n : ℤ<GOAL>0 ≤ Int.sqrt n
<VAR>n : ℕ<GOAL>Int.sqrt ↑n = ↑n.sqrt
<VAR>n : ℕ<GOAL>Int.sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))
<VAR>p : Prop<VAR>a : Erased p<GOAL>p
<VAR>α : Sort u_1<VAR>a : α<GOAL>(Erased.mk a).out = a
<VAR>α : Sort u_1<VAR>a : Erased α<GOAL>Erased.mk a.out = a
<VAR>α : Sort u_1<VAR>a b : Erased α<VAR>h : a.out = b.out<GOAL>a = b
<VAR>α : Sort u_1<GOAL>Nonempty (Erased α) ↔ Nonempty α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>a : Erased α<VAR>f : α → Erased β<GOAL>a.bind f = f a.out
<VAR>α : Sort u_1<VAR>a : Erased (Erased α)<GOAL>a.join = a.out
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>a : Erased α<GOAL>(Erased.map f a).out = f a.out
<VAR>α : Type u_1<GOAL>pure = Erased.mk
<VAR>α β : Type u_1<GOAL>(fun x x_1 => x >>= x_1) = Erased.bind
<VAR>α β : Type u_1<GOAL>(fun x x_1 => x <$> x_1) = Erased.map
<VAR>S : Type u_2<VAR>LinearOrderedCommRing S<VAR>abv : AbsoluteValue ℤ S<VAR>x : ℤˣ<GOAL>abv ↑x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>LinearOrderedCommRing S<VAR>Nontrivial R<VAR>abv : AbsoluteValue R S<VAR>x : ℤˣ<GOAL>abv ↑↑x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>x : ℤˣ<VAR>y : R<GOAL>abv (x • y) = abv y
<VAR>m : ℤ<GOAL>Int.natAbsHom m = m.natAbs
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f : α₁ → β₁ → Finset γ₁<VAR>g : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<GOAL>c ∈ Finset.sumLift₂ f g a b ↔ (∃ a₁ b₁ c₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c = Sum.inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨ ∃ a₂ b₂ c₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ g a₂ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f : α₁ → β₁ → Finset γ₁<VAR>g : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c₁ : γ₁<GOAL>Sum.inl c₁ ∈ Finset.sumLift₂ f g a b ↔ ∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c₁ ∈ f a₁ b₁
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f : α₁ → β₁ → Finset γ₁<VAR>g : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c₂ : γ₂<GOAL>Sum.inr c₂ ∈ Finset.sumLift₂ f g a b ↔ ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c₂ ∈ g a₂ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f : α₁ → β₁ → Finset γ₁<VAR>g : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>Finset.sumLift₂ f g a b = ∅ ↔ (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ → b = Sum.inl b₁ → f a₁ b₁ = ∅) ∧ ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ → b = Sum.inr b₂ → g a₂ b₂ = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f : α₁ → β₁ → Finset γ₁<VAR>g : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>(Finset.sumLift₂ f g a b).Nonempty ↔ (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ (f a₁ b₁).Nonempty) ∨ ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ (g a₂ b₂).Nonempty
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>h₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ g₁ a b<VAR>h₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ g₂ a b<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>Finset.sumLift₂ f₁ f₂ a b ⊆ Finset.sumLift₂ g₁ g₂ a b
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁<VAR>b : β₁<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f₁ a b)
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁<VAR>b : β₂<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inr b) = (g₁ a b).disjSum (g₂ a b)
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₂<VAR>b : β₁<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inl b) = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₂<VAR>b : β₂<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = Finset.map { toFun := Sum.inr, inj' := ⋯ } (f₂ a b)
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<GOAL>c ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔ (∃ a₁ b₁ c₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c = Sum.inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ (∃ a₁ b₂ c₁, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c = Sum.inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨ (∃ a₁ b₂ c₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂ c₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c₁ : γ₁<GOAL>Sum.inl c₁ ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔ (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ ∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c₁ ∈ g₁ a₁ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c₂ : γ₂<GOAL>Sum.inr c₂ ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔ (∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c₂ ∈ f₂ a₂ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b<VAR>hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b<VAR>hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b<VAR>hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ a b ⊆ Finset.sumLexLift f₁' f₂' g₁' g₂' a b
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>Finset.sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔ (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ → b = Sum.inl b₁ → f₁ a₁ b₁ = ∅) ∧ (∀ (a₁ : α₁) (b₂ : β₂), a = Sum.inl a₁ → b = Sum.inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧ ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ → b = Sum.inr b₂ → f₂ a₂ b₂ = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ : α₁ → β₁ → Finset γ₁<VAR>f₂ : α₂ → β₂ → Finset γ₂<VAR>g₁ : α₁ → β₂ → Finset γ₁<VAR>g₂ : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<GOAL>(Finset.sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔ (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨ (∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨ ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ (f₂ a₂ b₂).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Icc (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Icc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ico (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ico a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ioc (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ioc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ioo (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ioo a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ : α<VAR>b₂ : β<GOAL>Finset.Icc (Sum.inl a₁) (Sum.inr b₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ : α<VAR>b₂ : β<GOAL>Finset.Ico (Sum.inl a₁) (Sum.inr b₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ : α<VAR>b₂ : β<GOAL>Finset.Ioc (Sum.inl a₁) (Sum.inr b₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ : α<VAR>b₂ : β<GOAL>Finset.Ioo (Sum.inl a₁) (Sum.inr b₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₂ : α<VAR>b₁ : β<GOAL>Finset.Icc (Sum.inr b₁) (Sum.inl a₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₂ : α<VAR>b₁ : β<GOAL>Finset.Ico (Sum.inr b₁) (Sum.inl a₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₂ : α<VAR>b₁ : β<GOAL>Finset.Ioc (Sum.inr b₁) (Sum.inl a₂) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₂ : α<VAR>b₁ : β<GOAL>Finset.Ioo (Sum.inr b₁) (Sum.inl a₂) = ∅