ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>Hnext : ∀ (n : ℕ), Function.Injective next<GOAL>Function.Injective (Nat.leRecOn hnm fun {k} => next)
<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>Hnext : ∀ (n : ℕ), Function.Surjective next<GOAL>Function.Surjective (Nat.leRecOn hnm fun {k} => next)
<VAR>n : ℕ<VAR>P : ℕ → Sort u_1<VAR>h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n<GOAL>n.strongRecOn' h = h n fun m x => m.strongRecOn' h
<VAR>m : ℕ<VAR>P : (n : ℕ) → m ≤ n → Prop<VAR>base : P m ⋯<VAR>succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯<VAR>n : ℕ<VAR>hmn : m ≤ n<GOAL>P n hmn
<VAR>n : ℕ<VAR>motive : (m : ℕ) → m ≤ n → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯<VAR>self : motive n ⋯<GOAL>Nat.decreasingInduction of_succ self ⋯ = self
<VAR>m n : ℕ<VAR>motive : (m : ℕ) → m ≤ n + 1 → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯<VAR>self : motive (n + 1) ⋯<VAR>mn : m ≤ n<VAR>msn : m ≤ n + 1<GOAL>Nat.decreasingInduction of_succ self msn = Nat.decreasingInduction (fun i hi => of_succ i ⋯) (of_succ n ⋯ self) mn
<VAR>n : ℕ<VAR>motive : (m : ℕ) → m ≤ n + 1 → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯<VAR>self : motive (n + 1) ⋯<GOAL>Nat.decreasingInduction of_succ self ⋯ = of_succ n ⋯ self
<VAR>m n k : ℕ<VAR>motive : (m : ℕ) → m ≤ k → Sort u_1<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<VAR>of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯<VAR>self : motive k ⋯<GOAL>Nat.decreasingInduction of_succ self ⋯ = Nat.decreasingInduction (fun n_1 ih => of_succ n_1 ⋯) (Nat.decreasingInduction of_succ self hnk) hmn
<VAR>m n : ℕ<VAR>motive : (m : ℕ) → m ≤ n → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯<VAR>self : motive n ⋯<VAR>smn : m + 1 ≤ n<VAR>mn : m ≤ n<GOAL>Nat.decreasingInduction of_succ self mn = of_succ m smn (Nat.decreasingInduction of_succ self smn)
<VAR>P : ℕ → ℕ → Prop<VAR>ha : ∀ (a : ℕ), P (a + 1) (a + 1)<VAR>hb : ∀ (b : ℕ), P 0 (b + 1)<VAR>hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)<VAR>a b : ℕ<GOAL>a < b → P a b
<VAR>n k : ℕ<VAR>S : Set ℕ<VAR>hk : k ∈ S<VAR>h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S<VAR>hnk : k ≤ n<GOAL>n ∈ S
<VAR>S : Set ℕ<VAR>hb : 0 ∈ S<VAR>h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S<VAR>n : ℕ<GOAL>n ∈ S
<VAR>n : ℕ<GOAL>¬n % 2 = 1 ↔ n % 2 = 0
<VAR>n : ℕ<GOAL>¬n % 2 = 0 ↔ n % 2 = 1
<VAR>a b c : ℕ<GOAL>a / b % c = a % (b * c) / b
<VAR>d n : ℕ<VAR>hdn : d ∣ n<VAR>a : ℕ<GOAL>a < n / d ↔ d * a < n
<VAR>n d : ℕ<GOAL>d * (n / d) = n ↔ d ∣ n
<VAR>d n : ℕ<GOAL>d * (n / d) < n ↔ ¬d ∣ n
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ∣ n<VAR>hb : b ∣ n<GOAL>n / a = n / b ↔ a = b
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>a / b = 0 ↔ a < b
<VAR>a b : ℕ<VAR>hb : b ≠ 0<GOAL>a / b ≠ 0 ↔ b ≤ a
<VAR>a b : ℕ<VAR>hb : b ≠ 0<GOAL>0 < a / b ↔ b ≤ a
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hab : a ∣ b<GOAL>a ≤ b ↔ b ≠ 0
<VAR>a b : ℕ<VAR>hba : b ∣ a<GOAL>a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
<VAR>a b c : ℕ<GOAL>a * (b % c) % c = a * b % c
<VAR>a b c : ℕ<GOAL>a % c * b % c = a * b % c
<VAR>a b n : ℕ<GOAL>a ^ b % n = (a % n) ^ b % n
<VAR>a n : ℕ<GOAL>1 < a → 1 < n → ¬a ^ n ∣ a
<VAR>a b n : ℕ<VAR>hb : b ≠ 0<VAR>ha : 2 ≤ a<VAR>h : a ^ n ∣ b<GOAL>n < b
<VAR>m n : ℕ<VAR>h : n ∣ m<GOAL>m / n ∣ m
<VAR>m n : ℕ<VAR>h : n ∣ m<VAR>hm : m ≠ 0<GOAL>m / (m / n) = n
<VAR>m n : ℕ<VAR>h1 : 0 < n<VAR>h2 : n < m<GOAL>¬m ∣ n
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hdvd : b ∣ a<VAR>hlt : a < 2 * b<GOAL>a = b
<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>m % n = m ↔ m < n
<VAR>m n : ℕ<GOAL>m % n.succ = m ↔ m < n.succ
<VAR>n : ℕ<GOAL>n % n.succ = n
<VAR>a b : ℕ<GOAL>a % b + a / b * b = a
<VAR>a b : ℕ<GOAL>a / b * b + a % b = a
<VAR>a b c d : ℕ<VAR>h : 0 < b<GOAL>a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b
<VAR>m n k : ℕ<VAR>h : m % k = n % k<GOAL>(m - n) % k = 0
<VAR>n : ℕ<GOAL>1 % (n + 2) = 1
<VAR>n : ℕ<GOAL>n ≠ 1 → 1 % n = 1
<VAR>n : ℕ<VAR>k : ℕ<GOAL>n ∣ k - k % n
<VAR>m n k : ℕ<GOAL>(m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k
<VAR>m n k : ℕ<VAR>h1 : n * k < m<VAR>h2 : m < n * (k + 1)<GOAL>¬n ∣ m
<VAR>a b c : ℕ<VAR>h : a ∣ c<GOAL>a ∣ b + c ↔ a ∣ b
<VAR>a b c : ℕ<VAR>h : a ∣ b<GOAL>a ∣ b + c ↔ a ∣ c
<VAR>a b c : ℕ<VAR>ha : 0 < a<GOAL>a * b ∣ a * c ↔ b ∣ c
<VAR>a b c : ℕ<VAR>hc : 0 < c<GOAL>a * c ∣ b * c ↔ a ∣ b
<VAR>a b d : ℕ<VAR>c : ℕ<VAR>H : a % d = b % d<GOAL>(a + c) % d = (b + c) % d
<VAR>a b d : ℕ<VAR>c : ℕ<VAR>H : a % d = b % d<GOAL>(c + a) % d = (c + b) % d
<VAR>a b c : ℕ<VAR>hcb : c ∣ b<VAR>h : a ∣ b / c<GOAL>c * a ∣ b
<VAR>a b : ℕ<VAR>hab : a ∣ b<VAR>h : b / a = 1<GOAL>a = b
<VAR>a b : ℕ<VAR>hab : a ∣ b<VAR>h : b / a = 0<GOAL>b = 0
<VAR>a b c d : ℕ<VAR>h1 : a ≤ b<VAR>h2 : d ≤ c<VAR>h3 : d ≠ 0<GOAL>a / c ≤ b / d
<VAR>b : ℕ<VAR>a : ℕ<VAR>hb : 0 < b<GOAL>a < b * (a / b + 1)
<VAR>a b c : ℕ<GOAL>(a * b + c) % b = c % b
<VAR>a b c : ℕ<VAR>h : c < b<GOAL>(a * b + c) % b = c
<VAR>m n : ℕ<GOAL>m ∣ m + n ↔ m ∣ n
<VAR>m n : ℕ<GOAL>m ∣ n + m ↔ m ∣ n
<VAR>m n k : ℕ<VAR>h₁ : k ∣ m<VAR>h₂ : k ∣ n<GOAL>k ∣ m - n
<VAR>a b : ℕ<GOAL>(a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
<VAR>a b : ℕ<VAR>hba : b ∣ a + 1<GOAL>(a + 1) / b = a / b + 1
<VAR>a b : ℕ<VAR>hba : ¬b ∣ a + 1<GOAL>(a + 1) / b = a / b
<VAR>n d : ℕ<GOAL>d ∣ n ↔ n / d * d = n
<VAR>n d : ℕ<GOAL>d ∣ n ↔ n ≤ n / d * d
<VAR>n d : ℕ<GOAL>d ∣ n ↔ ∀ (k : ℕ), k ∣ d → k ∣ n
<VAR>a b c : ℕ<VAR>h : a * b ∣ c<GOAL>b ∣ c / a
<VAR>a b c : ℕ<VAR>hbc : c ∣ b<GOAL>a ∣ b / c ↔ c * a ∣ b
<VAR>a b c : ℕ<VAR>h : b ∣ a<VAR>hdiv : a / b ∣ c<GOAL>a ∣ b * c
<VAR>a b c : ℕ<VAR>h : b ∣ a<VAR>hb : b ≠ 0<GOAL>a / b ∣ c ↔ a ∣ b * c
<VAR>a b c : ℕ<VAR>dvd : b ∣ a<VAR>dvd2 : a ∣ c<GOAL>c / (a / b) / b = c / a
<VAR>a b : ℕ<VAR>w : a ∣ b<VAR>h : b < a<GOAL>b = 0
<VAR>a b n : ℕ<VAR>h : a < b + n<GOAL>n ∣ a → n ∣ b → a ≤ b
<VAR>n : ℕ<VAR>a : ℕ<VAR>ha : 0 < a<GOAL>(∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n
<VAR>m n : ℕ<GOAL>(∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n
<VAR>m n : ℕ<GOAL>(∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n
<GOAL>Function.Injective fun x x_1 => x ∣ x_1
<VAR>a b d : ℕ<VAR>hdb : d ∣ b<VAR>h : a < b<GOAL>a / d < b / d
<VAR>n k : ℕ<GOAL>let iter_next := fun n guess => (guess + n / guess) / 2;
Nat.sqrt.iter n k ≤ iter_next n (Nat.sqrt.iter n k)
<VAR>a b : ℕ<GOAL>4 * a * b ≤ (a + b) * (a + b)
<VAR>n guess : ℕ<GOAL>Nat.sqrt.iter n guess * Nat.sqrt.iter n guess ≤ n
<VAR>n guess : ℕ<VAR>hn : n < (guess + 1) * (guess + 1)<GOAL>n < (Nat.sqrt.iter n guess + 1) * (Nat.sqrt.iter n guess + 1)
<VAR>n : ℕ<GOAL>Nat.IsSqrt n n.sqrt
<VAR>n : ℕ<GOAL>n.sqrt * n.sqrt ≤ n
<VAR>n : ℕ<GOAL>n.sqrt ^ 2 ≤ n
<VAR>n : ℕ<GOAL>n < n.sqrt.succ * n.sqrt.succ
<VAR>n : ℕ<GOAL>n < n.sqrt.succ ^ 2
<VAR>n : ℕ<GOAL>n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
<VAR>m n : ℕ<GOAL>m ≤ n.sqrt ↔ m * m ≤ n
<VAR>m n : ℕ<GOAL>m ≤ n.sqrt ↔ m ^ 2 ≤ n
<VAR>m n : ℕ<GOAL>m.sqrt < n ↔ m < n * n
<VAR>m n : ℕ<GOAL>m.sqrt < n ↔ m < n ^ 2
<VAR>n : ℕ<GOAL>n.sqrt ≤ n
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.sqrt ≤ n.sqrt
<VAR>n : ℕ<GOAL>n.sqrt = 0 ↔ n = 0
<VAR>a n : ℕ<GOAL>a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)
<VAR>a n : ℕ<GOAL>a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2
<VAR>n : ℕ<VAR>h : n.sqrt = 1<GOAL>n ≤ 3
<VAR>n : ℕ<VAR>h : 1 < n<GOAL>n.sqrt < n
<VAR>n : ℕ<GOAL>0 < n.sqrt ↔ 0 < n
<VAR>a : ℕ<VAR>n : ℕ<VAR>h : a ≤ n + n<GOAL>(n * n + a).sqrt = n
<VAR>a : ℕ<VAR>n : ℕ<VAR>h : a ≤ n + n<GOAL>(n ^ 2 + a).sqrt = n
<VAR>n : ℕ<GOAL>(n * n).sqrt = n
<VAR>n : ℕ<GOAL>(n ^ 2).sqrt = n
<VAR>n : ℕ<GOAL>n.succ.sqrt ≤ n.sqrt.succ
<VAR>x : ℕ<GOAL>(∃ n, n * n = x) ↔ x.sqrt * x.sqrt = x
<VAR>x : ℕ<GOAL>(∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x
<VAR>n : ℕ<GOAL>n.sqrt * n.sqrt < n + 1
<VAR>n : ℕ<GOAL>n.sqrt ^ 2 < n + 1
<VAR>n : ℕ<GOAL>n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)
<VAR>n : ℕ<GOAL>n + 1 ≤ (n.sqrt + 1) ^ 2
<VAR>m n : ℕ<VAR>hl : m * m < n<VAR>hr : n < (m + 1) * (m + 1)<GOAL>¬∃ t, t * t = n
<VAR>m n : ℕ<GOAL>m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n
<GOAL>Function.LeftInverse WType.ofNat WType.toNat
<GOAL>Function.RightInverse WType.ofNat WType.toNat
<VAR>c : WType.Natα<GOAL>WType.NatαEquivPUnitSumPUnit c = match c with | WType.Natα.zero => Sum.inl PUnit.unit | WType.Natα.succ => Sum.inr PUnit.unit
<VAR>b : PUnit.{u + 1} ⊕ PUnit.{u_1 + 1}<GOAL>WType.NatαEquivPUnitSumPUnit.symm b = match b with | Sum.inl val => WType.Natα.zero | Sum.inr val => WType.Natα.succ
<VAR>γ : Type u<GOAL>Function.LeftInverse (WType.ofList γ) (WType.toList γ)
<VAR>γ : Type u<GOAL>Function.RightInverse (WType.ofList γ) (WType.toList γ)
<VAR>n : ℕ<GOAL>n.totient = (Finset.filter n.Coprime (Finset.range n)).card
<VAR>n : ℕ<GOAL>n.totient = Nat.card ↑{m | m < n ∧ n.Coprime m}
<VAR>n : ℕ<GOAL>n.totient ≤ n
<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>n.totient < n
<VAR>n : ℕ<GOAL>n.totient = 0 ↔ n = 0
<VAR>n : ℕ<GOAL>0 < n.totient ↔ 0 < n
<VAR>a n : ℕ<GOAL>(Finset.filter a.Coprime (Finset.Ico n (n + a))).card = a.totient
<VAR>a : ℕ<VAR>k n : ℕ<VAR>a_pos : 0 < a<GOAL>(Finset.filter a.Coprime (Finset.Ico k (k + n))).card ≤ a.totient * (n / a + 1)
<VAR>n : ℕ<VAR>NeZero n<VAR>Fintype (ZMod n)ˣ<GOAL>Fintype.card (ZMod n)ˣ = n.totient
<VAR>n : ℕ<VAR>hn : 2 < n<GOAL>Even n.totient
<VAR>m n : ℕ<VAR>h : m.Coprime n<GOAL>(m * n).totient = m.totient * n.totient
<VAR>n d : ℕ<VAR>hnd : d ∣ n<GOAL>(n / d).totient = (Finset.filter (fun k => n.gcd k = d) (Finset.range n)).card
<VAR>n : ℕ<GOAL>n.divisors.sum Nat.totient = n
<VAR>n : ℕ<GOAL>∑ m ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ), m.totient = n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℕ<GOAL>(p ^ (n + 1)).totient = p ^ n * (p - 1)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(p ^ n).totient = p ^ (n - 1) * (p - 1)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.totient = p - 1
<VAR>p : ℕ<VAR>hp : 0 < p<GOAL>p.totient = p - 1 ↔ Nat.Prime p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>Fintype (ZMod p)ˣ<GOAL>Fintype.card (ZMod p)ˣ ≤ p - 1
<VAR>p : ℕ<VAR>Fintype (ZMod p)ˣ<GOAL>Nat.Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
<VAR>n : ℕ<GOAL>n.totient = 1 ↔ n = 1 ∨ n = 2
<VAR>a : ℕ<VAR>han : 0 < a<VAR>ha : a.totient ≤ 1<GOAL>a ∣ 2
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n.totient = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
<VAR>n : ℕ<GOAL>n.totient * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<GOAL>n.totient = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<GOAL>↑n.totient = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
<VAR>a b : ℕ<GOAL>(a.gcd b).totient * (a * b).totient = a.totient * b.totient * a.gcd b
<VAR>a b : ℕ<GOAL>a.totient * b.totient ≤ (a * b).totient
<VAR>a b : ℕ<VAR>h : a ∣ b<GOAL>a.totient ∣ b.totient
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>h : p ∣ n<GOAL>(p * n).totient = p * n.totient
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>h : ¬p ∣ n<GOAL>(p * n).totient = (p - 1) * n.totient
<VAR>p q : ℝ<VAR>self : p.IsConjExponent q<GOAL>p⁻¹ + q⁻¹ = 1
<VAR>p q : ℝ<VAR>self : p.IsConjExponent q<GOAL>1 < p
<VAR>p q : ℝ<GOAL>p.IsConjExponent q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 < p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 ≤ p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p ≠ 0
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 < p - 1
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p - 1 ≠ 0
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 < p⁻¹
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 ≤ p⁻¹
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p⁻¹ ≠ 0
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 < 1 / p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>0 ≤ 1 / p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>1 / p ≠ 0
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>q = p / (p - 1)
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p.conjExponent = q
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>1 - p⁻¹ = q⁻¹
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p⁻¹ - 1 = -q⁻¹
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>(p - 1) * q = p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p * q = p + q
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>q.IsConjExponent p
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p / q = p - 1
<VAR>p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>(ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a⁻¹.IsConjExponent b⁻¹
<VAR>a : ℝ<VAR>ha₀ : 0 < a<VAR>ha₁ : a < 1<GOAL>a⁻¹.IsConjExponent (1 - a)⁻¹
<VAR>a : ℝ<VAR>ha₀ : 0 < a<VAR>ha₁ : a < 1<GOAL>(1 - a)⁻¹.IsConjExponent a⁻¹
<VAR>p q : ℝ<VAR>hp : 1 < p<GOAL>p.IsConjExponent q ↔ q = p / (p - 1)
<VAR>p : ℝ<VAR>h : 1 < p<GOAL>p.IsConjExponent p.conjExponent
<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>(1 / a).IsConjExponent (1 / b)
<VAR>p q : NNReal<GOAL>p.IsConjExponent q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
<VAR>p q : NNReal<VAR>self : p.IsConjExponent q<GOAL>p⁻¹ + q⁻¹ = 1
<VAR>p q : NNReal<VAR>self : p.IsConjExponent q<GOAL>1 < p
<VAR>p q : NNReal<GOAL>(↑p).IsConjExponent ↑q ↔ p.IsConjExponent q
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>1 ≤ p
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>0 < p
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p ≠ 0
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>0 < p - 1
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p - 1 ≠ 0
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>0 < p⁻¹
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p⁻¹ ≠ 0
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>1 - p⁻¹ = q⁻¹
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>q = p / (p - 1)
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p.conjExponent = q
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>(p - 1) * q = p
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p * q = p + q
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>q.IsConjExponent p
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>p / q = p - 1
<VAR>p q : NNReal<VAR>h : p.IsConjExponent q<GOAL>↑p⁻¹ + ↑q⁻¹ = 1
<VAR>a b : NNReal<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : a + b = 1<GOAL>a⁻¹.IsConjExponent b⁻¹
<VAR>a : NNReal<VAR>ha₀ : a ≠ 0<VAR>ha₁ : a < 1<GOAL>a⁻¹.IsConjExponent (1 - a)⁻¹
<VAR>a : NNReal<VAR>ha₀ : a ≠ 0<VAR>ha₁ : a < 1<GOAL>(1 - a)⁻¹.IsConjExponent a⁻¹
<VAR>p q : NNReal<VAR>h : 1 < p<GOAL>p.IsConjExponent q ↔ q = p / (p - 1)
<VAR>p : NNReal<VAR>h : 1 < p<GOAL>p.IsConjExponent p.conjExponent
<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>p.toNNReal.IsConjExponent q.toNNReal
<VAR>α : Type u<VAR>β : α → Type v<GOAL>Cardinal.mk (WType β) = Cardinal.sum fun a => Cardinal.mk (WType β) ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))
<VAR>α : Type u<VAR>β : α → Type v<VAR>κ : Cardinal.{max u v}<VAR>hκ : (Cardinal.sum fun a => κ ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))) ≤ κ<GOAL>Cardinal.mk (WType β) ≤ κ
<VAR>α : Type u<VAR>β : α → Type v<VAR>∀ (a : α), Finite (β a)<GOAL>Cardinal.mk (WType β) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk α)) Cardinal.aleph0
<VAR>α : Type u<VAR>β : α → Type u<GOAL>Cardinal.mk (WType β) = Cardinal.sum fun a => Cardinal.mk (WType β) ^ Cardinal.mk (β a)
<VAR>α : Type u<VAR>β : α → Type u<VAR>κ : Cardinal.{u}<VAR>hκ : (Cardinal.sum fun a => κ ^ Cardinal.mk (β a)) ≤ κ<GOAL>Cardinal.mk (WType β) ≤ κ
<VAR>α : Type u<VAR>β : α → Type u<VAR>∀ (a : α), Finite (β a)<GOAL>Cardinal.mk (WType β) ≤ max (Cardinal.mk α) Cardinal.aleph0
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>w : WType β<GOAL>WType.ofSigma w.toSigma = w
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>s : (a : α) × (β a → WType β)<GOAL>(WType.ofSigma s).toSigma = s
<VAR>α : Type u_1<VAR>β : α → Type u_2<GOAL>∀ (a : WType β), (WType.equivSigma β) a = a.toSigma
<VAR>α : Type u_1<VAR>β : α → Type u_2<GOAL>∀ (a : (a : α) × (β a → WType β)), (WType.equivSigma β).symm a = WType.ofSigma a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>fγ : (a : α) × (β a → γ) → γ<VAR>fγ_injective : Function.Injective fγ<GOAL>Function.Injective (WType.elim γ fγ)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>a b : α<VAR>ha : Nonempty (β a)<VAR>he : IsEmpty (β b)<GOAL>Infinite (WType β)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → Fintype (β a)<VAR>t : WType β<GOAL>0 < t.depth
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → Fintype (β a)<VAR>a : α<VAR>f : β a → WType β<VAR>i : β a<GOAL>(f i).depth < (WType.mk a f).depth
<VAR>a b : String<GOAL>a ++ b = { data := a.data ++ b.data }
<VAR>n : ℕ<VAR>c : Char<GOAL>(String.replicate n c).length = n
<VAR>l : List Char<GOAL>{ data := l }.length = l.length
<VAR>n : ℕ<VAR>c : Char<VAR>s : String<GOAL>(String.leftpad n c s).length = max n s.length
<VAR>n : ℕ<VAR>c : Char<VAR>s : String<GOAL>(String.replicate (n - s.length) c).IsPrefix (String.leftpad n c s)
<VAR>n : ℕ<VAR>c : Char<VAR>s : String<GOAL>s.IsSuffix (String.leftpad n c s)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<GOAL>sInf (a • s) = a • sInf s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>f : ι → ℝ<GOAL>a • ⨅ i, f i = ⨅ i, a • f i
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<GOAL>sSup (a • s) = a • sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>f : ι → ℝ<GOAL>a • ⨆ i, f i = ⨆ i, a • f i
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>Module α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<GOAL>sInf (a • s) = a • sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>Module α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>f : ι → ℝ<GOAL>a • ⨆ i, f i = ⨅ i, a • f i
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>Module α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<GOAL>sSup (a • s) = a • sInf s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>Module α ℝ<VAR>OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>f : ι → ℝ<GOAL>a • ⨅ i, f i = ⨆ i, a • f i
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>r * ⨅ i, f i = ⨅ i, r * f i
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>r * ⨆ i, f i = ⨆ i, r * f i
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>r * ⨅ i, f i = ⨆ i, r * f i
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>r * ⨆ i, f i = ⨅ i, r * f i
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>(⨅ i, f i) * r = ⨅ i, f i * r
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>(⨆ i, f i) * r = ⨆ i, f i * r
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>(⨅ i, f i) * r = ⨆ i, f i * r
<VAR>ι : Sort u_1<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>(⨆ i, f i) * r = ⨅ i, f i * r
<VAR>R : Type u<VAR>P : Fin 3 → R<GOAL>![P x, P y, P z] = P
<VAR>R : Type u<VAR>X Y Z : R<GOAL>![X, Y, Z] x = X ∧ ![X, Y, Z] y = Y ∧ ![X, Y, Z] z = Z
<VAR>R : Type u<VAR>S : Type u_1<VAR>f : R → S<VAR>X Y Z : R<GOAL>f ∘ ![X, Y, Z] = ![f X, f Y, f Z]
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z]
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>(u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<GOAL>u • P ≈ P
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<GOAL>⟦u • P⟧ = ⟦P⟧
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hz : P z = Q z<VAR>mem : Q z ∈ nonZeroDivisors R<GOAL>P ≈ Q ↔ P = Q
<VAR>R : Type u<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hz : P z = Q z<VAR>hQz : Q z ≠ 0<GOAL>P ≈ Q ↔ P = Q
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>P z = 0 ↔ Q z = 0
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>P x * Q z ^ 2 = Q x * P z ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>P y * Q z ^ 3 = Q y * P z ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hPz : P z = 0<VAR>hQz : Q z ≠ 0<GOAL>¬P ≈ Q
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hPz : P z ≠ 0<VAR>hQz : Q z = 0<GOAL>¬P ≈ Q
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>¬P ≈ Q
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>¬P ≈ Q
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<GOAL>P ≈ Q
<VAR>F : Type v<VAR>Field F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1]
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>P x * Q z ^ 2 = Q x * P z ^ 2 ↔ P x / P z ^ 2 = Q x / Q z ^ 2
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>P y * Q z ^ 3 = Q y * P z ^ 3 ↔ P y / P z ^ 3 = Q y / Q z ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W'.polynomial = P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>(MvPolynomial.eval P) W.polynomial / P z ^ 6 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.Equation P ↔ P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<GOAL>W'.Equation (u • P) ↔ W'.Equation P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>W'.Equation P ↔ W'.Equation Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.Equation P ↔ P y ^ 2 = P x ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<GOAL>W'.Equation ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>X Y : R<GOAL>W'.Equation ![X, Y, 1] ↔ W'.toAffine.Equation X Y
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.Equation P ↔ W.toAffine.Equation (P x / P z ^ 2) (P y / P z ^ 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<GOAL>W'.polynomialX = MvPolynomial.C W'.a₁ * MvPolynomial.X y * MvPolynomial.X z - (MvPolynomial.C 3 * MvPolynomial.X x ^ 2 + MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X x * MvPolynomial.X z ^ 2 + MvPolynomial.C W'.a₄ * MvPolynomial.X z ^ 4)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>(MvPolynomial.eval P) W.polynomialX / P z ^ 4 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialX
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<GOAL>W'.polynomialY = MvPolynomial.C 2 * MvPolynomial.X y + MvPolynomial.C W'.a₁ * MvPolynomial.X x * MvPolynomial.X z + MvPolynomial.C W'.a₃ * MvPolynomial.X z ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>(MvPolynomial.eval P) W.polynomialY / P z ^ 3 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<GOAL>W'.polynomialZ = MvPolynomial.C W'.a₁ * MvPolynomial.X x * MvPolynomial.X y + MvPolynomial.C (3 * W'.a₃) * MvPolynomial.X y * MvPolynomial.X z ^ 2 - (MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X x ^ 2 * MvPolynomial.X z + MvPolynomial.C (4 * W'.a₄) * MvPolynomial.X x * MvPolynomial.X z ^ 3 + MvPolynomial.C (6 * W'.a₆) * MvPolynomial.X z ^ 5)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W'.polynomialZ = W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)