mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ 0 < n + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
·

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
·

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ ↑n.properDivisors
⊢ k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

pp: case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∈ ↑n.properDivisors

Tactic:
·

Goal state after:
case neg.refine_1
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ ↑n.properDivisors
⊢ k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∈ ↑n.properDivisors

Tactic:
·

Goal state after:
case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∈ ↑n.properDivisors
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Tactic:
·

Goal state after:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ n ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 < n

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

pp: case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
·

Goal state after:
case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
·

Goal state after:
case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂

pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
·

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b

pp: case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
·

Goal state after:
case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
·

Goal state after:
case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n

pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Tactic:
·

Goal state after:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

pp: case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
·

Goal state after:
case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0

pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
·

Goal state after:
case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case pos
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
·

Goal state after:
case pos
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
·

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ 0 < n.greatestFib ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
·

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
·

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
·

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inl
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib

pp: case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
·

Goal state after:
case inl
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
this : multiplicity p n + 1 ≤ multiplicity p n
⊢ False

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n

pp: case hf
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ FiniteMultiplicity p n

Tactic:
·

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case hf
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ FiniteMultiplicity p n

Tactic:
·

Goal state after:
case hf
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ FiniteMultiplicity p n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) ≤ n - 1

pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))

Tactic:
·

Goal state after:
case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) ≤ n - 1
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))

Tactic:
·

Goal state after:
case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Finite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
·

Goal state after:
case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Finite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
·

Goal state after:
case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

pp: case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
·

Goal state after:
case pos
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
·

Goal state after:
case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n

pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
·

Goal state after:
case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
·

Goal state after:
case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Finite
⊢ a ≤ nth p k

pp: case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k

Tactic:
·

Goal state after:
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Finite
⊢ a ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
·

Goal state after:
case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
·

Goal state after:
case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k

Tactic:
·

Goal state after:
case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
·

Goal state after:
case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
·

Goal state after:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

pp: case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n ≤ f n

Tactic:
·

Goal state after:
case pos
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n ≤ f n

Tactic:
·

Goal state after:
case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n ≤ f n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ.refine_1
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ {x | p x ∧ ∀ k < n + 1, nth p k < x}.Nonempty

pp: case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ ∀ b ∈ {x | p x ∧ ∀ k < n + 1, nth p k < x}, f (n + 1) ≤ b

Tactic:
·

Goal state after:
case succ.refine_1
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ {x | p x ∧ ∀ k < n + 1, nth p k < x}.Nonempty
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case one
⊢ ↑one.minFac = (↑one).minFac

pp: case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac

pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
·

Goal state after:
case one
⊢ ↑one.minFac = (↑one).minFac
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac

pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
·

Goal state after:
case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

pp: case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

Tactic:
·

Goal state after:
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

pp: case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)

Tactic:
·

Goal state after:
case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
·

Goal state after:
case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑2 = 2

pp: case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0

Tactic:
·

Goal state after:
case bit0
a✝ : PosNum
⊢ ↑2 = 2
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit0

pp: case refine_2
n : PosNum
⊢ ↑n.bit0 = (↑n.bit0).minFac ↔ n = 1

Tactic:
·

Goal state after:
case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit0
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit1

pp: case refine_2
n : PosNum
⊢ (↑n.bit1).minFac = ↑n.bit1 ↔ n.bit1.minFacAux (↑n) 1 = n.bit1

Tactic:
·

Goal state after:
case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit1
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
·

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
·

Goal state after:
case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
·

Goal state after:
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
·

Goal state after:
case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α