[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
⊢ multiplicity m n = ↑(card (Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1)))
[PROOFSTEP]
simp
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ i ∈ Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1) ↔ i ∈ filter (fun i => m ^ i ∣ n) (Ico 1 b)
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ← @PartENat.coe_le_coe i, PartENat.natCast_get, ←
  pow_dvd_iff_le_multiplicity, and_right_comm]
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ 1 ≤ i ∧ m ^ i ∣ n ↔ (1 ≤ i ∧ m ^ i ∣ n) ∧ i < b
[PROOFSTEP]
refine' (and_iff_left_of_imp fun h => lt_of_le_of_lt _ hb).symm
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
h : 1 ≤ i ∧ m ^ i ∣ n
⊢ i ≤ log m n
[PROOFSTEP]
cases' m with m
[GOAL]
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ zero ^ i ∣ n
⊢ i ≤ log zero n
[PROOFSTEP]
rw [zero_eq, zero_pow, zero_dvd_iff] at h
[GOAL]
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ n = 0
⊢ i ≤ log zero n
case zero n b : ℕ hn : 0 < n i : ℕ hm : zero ≠ 1 hb : log zero n < b h : 1 ≤ i ∧ 0 ^ i ∣ n ⊢ 0 < i
[PROOFSTEP]
exacts [(hn.ne' h.2).elim, h.1]
[GOAL]
case succ
n b : ℕ
hn : 0 < n
i m : ℕ
hm : succ m ≠ 1
hb : log (succ m) n < b
h : 1 ≤ i ∧ succ m ^ i ∣ n
⊢ i ≤ log (succ m) n
[PROOFSTEP]
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩) (le_of_dvd hn h.2)
[GOAL]
p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ multiplicity p 0! = ↑(∑ i in Ico 1 b, 0 / p ^ i)
[PROOFSTEP]
simp [Ico, hp.multiplicity_one]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p (n + 1)! = multiplicity p n ! + multiplicity p (n + 1)
[PROOFSTEP]
rw [factorial_succ, hp.multiplicity_mul, add_comm]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p n ! + multiplicity p (n + 1) =
    ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b)))
[PROOFSTEP]
rw [multiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
  multiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ i in Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))
[PROOFSTEP]
rw [sum_add_distrib, sum_boole]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x in Ico 1 b, n / p ^ x + ↑(card (filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))
[PROOFSTEP]
simp
[GOAL]
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have hp' := hp.prime
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h0 : 2 ≤ p := hp.two_le
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h2 : p * n + 1 ≤ p * (n + 1)
[GOAL]
case h2
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)
[PROOFSTEP]
linarith
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h3 : p * n + 1 ≤ p * (n + 1) + 1
[GOAL]
case h3
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1
[PROOFSTEP]
linarith
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have hm : multiplicity p (p * n)! ≠ ⊤ :=
  by
  rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
  exact ⟨hp.ne_one, factorial_pos _⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * n)! ≠ ⊤
[PROOFSTEP]
rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ p ≠ 1 ∧ 0 < (p * n)!
[PROOFSTEP]
exact ⟨hp.ne_one, factorial_pos _⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
hm : multiplicity p (p * n)! ≠ ⊤
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
revert hm
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0 :=
  by
  intro m hm
  rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
  rw [mem_Ico] at hm
  exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
[PROOFSTEP]
intro m hm
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ multiplicity p m = 0
[PROOFSTEP]
rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
[PROOFSTEP]
rw [mem_Ico] at hm
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
[PROOFSTEP]
exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
simp_rw [← prod_Ico_id_eq_factorial, multiplicity.Finset.prod hp', ← sum_Ico_consecutive _ h1 h3, add_assoc]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤ →
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
      ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
[PROOFSTEP]
intro h
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
h : ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
[PROOFSTEP]
rw [PartENat.add_left_cancel_iff h, sum_Ico_succ_top h2, multiplicity.mul hp', hp.multiplicity_self, sum_congr rfl h4,
  sum_const_zero, zero_add, add_comm (1 : PartENat)]
[GOAL]
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * n)! = multiplicity p n ! + ↑n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
p : ℕ
hp : Prime p
⊢ multiplicity p (p * zero)! = multiplicity p zero ! + ↑zero
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p (p * succ n)! = multiplicity p (succ n)! + ↑(succ n)
[PROOFSTEP]
simp only [succ_eq_add_one, multiplicity.mul, hp, hp.prime, ih, multiplicity_factorial_mul_succ, ← add_assoc,
  Nat.cast_one, Nat.cast_add, factorial_succ]
[GOAL]
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) + 1 = multiplicity p (n + 1) + multiplicity p n ! + ↑n + 1
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) = multiplicity p (n + 1) + multiplicity p n ! + ↑n
[PROOFSTEP]
rw [add_comm, add_assoc]
[GOAL]
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i in Ico 1 b, n / p ^ i
[PROOFSTEP]
rw [← PartENat.coe_le_coe, ← hp.multiplicity_factorial hbn, ← pow_dvd_iff_le_multiplicity]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ multiplicity p n ! ≤ ↑(n / (p - 1))
[PROOFSTEP]
rw [hp.multiplicity_factorial (lt_succ_self _), PartENat.coe_le_coe]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i in Ico 1 (succ (log p n)), n / p ^ i ≤ n / (p - 1)
[PROOFSTEP]
exact Nat.geom_sum_Ico_le hp.two_le _ _
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, n / p ^ i = ∑ i in Ico 1 b, (k + (n - k)) / p ^ i
[PROOFSTEP]
simp only [add_tsub_cancel_of_le hkn]
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k + (n - k)) / p ^ i =
    ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)
[PROOFSTEP]
simp only [Nat.add_div (pow_pos hp.pos _)]
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    ∑ i in Ico 1 b, k / p ^ i + ∑ i in Ico 1 b, (n - k) / p ^ i +
      card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))
[PROOFSTEP]
simp [sum_add_distrib, sum_boole]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ multiplicity p (choose n k) = ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))
[PROOFSTEP]
have h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card + multiplicity p (k ! * (n - k)!) :=
  by
  rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn, hp.multiplicity_factorial hnb,
    hp.multiplicity_mul, hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
    hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb), multiplicity_choose_aux hp hkn]
  simp [add_comm]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
[PROOFSTEP]
rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn, hp.multiplicity_factorial hnb,
  hp.multiplicity_mul, hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
  hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb), multiplicity_choose_aux hp hkn]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ ↑(∑ i in Ico 1 b, k / p ^ i + ∑ i in Ico 1 b, (n - k) / p ^ i +
        card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) +
      (↑(∑ i in Ico 1 b, k / p ^ i) + ↑(∑ i in Ico 1 b, (n - k) / p ^ i))
[PROOFSTEP]
simp [add_comm]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ multiplicity p (choose n k) = ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))
[PROOFSTEP]
refine (PartENat.add_right_cancel_iff ?_).1 h₁
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ multiplicity p (k ! * (n - k)!) ≠ ⊤
[PROOFSTEP]
apply PartENat.ne_top_iff_dom.2
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ (multiplicity p (k ! * (n - k)!)).Dom
[PROOFSTEP]
exact finite_nat_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩
[GOAL]
p : ℕ
hp : Prime p
x✝ : ℕ
⊢ multiplicity p x✝ ≤ multiplicity p (choose x✝ 0) + multiplicity p 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n✝ : ℕ
⊢ multiplicity p 0 ≤ multiplicity p (choose 0 (n✝ + 1)) + multiplicity p (n✝ + 1)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ multiplicity p (n + 1) ≤ multiplicity p (choose (n + 1) (k + 1)) + multiplicity p (k + 1)
[PROOFSTEP]
rw [← hp.multiplicity_mul]
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ multiplicity p (n + 1) ≤ multiplicity p (choose (n + 1) (k + 1) * (k + 1))
[PROOFSTEP]
refine' multiplicity_le_multiplicity_of_dvd_right _
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ choose (n + 1) (k + 1) * (k + 1)
[PROOFSTEP]
rw [← succ_mul_choose_eq]
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ succ n * choose n k
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p (choose (p ^ n) k) + multiplicity p k ≤ ↑n
[PROOFSTEP]
have hdisj :
  Disjoint ((Ico 1 n.succ).filter fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i)
    ((Ico 1 n.succ).filter fun i => p ^ i ∣ k) :=
  by simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
[PROOFSTEP]
simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
⊢ multiplicity p (choose (p ^ n) k) + multiplicity p k ≤ ↑n
[PROOFSTEP]
rw [multiplicity_choose hp hkn (lt_succ_self _),
  multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt (lt_succ_of_le (log_mono_right hkn)), ← Nat.cast_add,
  PartENat.coe_le_coe, log_pow hp.one_lt, ← card_disjoint_union hdisj, filter_union_right]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
⊢ card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ n
[PROOFSTEP]
have filter_le_Ico := (Ico 1 n.succ).card_filter_le fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
filter_le_Ico :
  card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ card (Ico 1 (succ n))
⊢ card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ n
[PROOFSTEP]
rwa [card_Ico 1 n.succ] at filter_le_Ico
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑n ≤ multiplicity p (choose (p ^ n) k) + multiplicity p k
[PROOFSTEP]
rw [← hp.multiplicity_pow_self]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p (p ^ n) ≤ multiplicity p (choose (p ^ n) k) + multiplicity p k
[PROOFSTEP]
exact multiplicity_le_multiplicity_choose_add hp _ _
[GOAL]
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
obtain hkp | hkp := hkp.symm.lt_or_lt
[GOAL]
case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
simp [choose_eq_zero_of_lt hkp]
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
refine' multiplicity_ne_zero.1 fun h => hkp.not_le <| Nat.le_of_dvd hk.bot_lt _
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
⊢ p ^ n ∣ k
[PROOFSTEP]
have H := hp.multiplicity_choose_prime_pow_add_multiplicity hkp.le hk
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
H : multiplicity p (choose (p ^ n) k) + multiplicity p k = ↑n
⊢ p ^ n ∣ k
[PROOFSTEP]
rw [h, zero_add, eq_coe_iff] at H
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k
[PROOFSTEP]
exact H.1
[GOAL]
p n k : ℕ
hp : Prime p
⊢ p ∣ choose (p ^ n) k ↔ k ≠ 0 ∧ k ≠ p ^ n
[PROOFSTEP]
refine' ⟨fun h => ⟨_, _⟩, fun h => dvd_choose_pow hp h.1 h.2⟩
[GOAL]
case refine'_1
p n k : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) k
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
p n k : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) k
⊢ k ≠ p ^ n
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
p n : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) 0
⊢ False
[PROOFSTEP]
simp [hp.ne_one] at h
[GOAL]
case refine'_2
p n : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) (p ^ n)
⊢ False
[PROOFSTEP]
simp [hp.ne_one] at h
[GOAL]
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
[PROOFSTEP]
have h2 := prime_two.prime
[GOAL]
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
[PROOFSTEP]
refine' binaryRec _ _
[GOAL]
case refine'_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → multiplicity 2 0! < ↑0
[PROOFSTEP]
exact fun h => False.elim <| h rfl
[GOAL]
case refine'_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → multiplicity 2 n ! < ↑n) → bit b n ≠ 0 → multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
intro b n ih h
[GOAL]
case refine'_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
subst hn
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
[PROOFSTEP]
simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
[PROOFSTEP]
simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (succ 0) < 1
[PROOFSTEP]
rw [Prime.multiplicity_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ 0 < 1
case pos h2 : _root_.Prime 2 b : Bool ih : 0 ≠ 0 → multiplicity 2 0! < ↑0 h : b = true ⊢ Prime 2
[PROOFSTEP]
simp only [zero_lt_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
[PROOFSTEP]
decide
[GOAL]
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
have : multiplicity 2 (2 * n)! < (2 * n : ℕ) :=
  by
  rw [prime_two.multiplicity_factorial_mul]
  refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
  rw [two_mul]
  norm_cast
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n)
[PROOFSTEP]
rw [prime_two.multiplicity_factorial_mul]
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 n ! + ↑n < ↑(2 * n)
[PROOFSTEP]
refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(2 * n)
[PROOFSTEP]
rw [two_mul]
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(n + n)
[PROOFSTEP]
norm_cast
[GOAL]
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
cases b
[GOAL]
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ multiplicity 2 (bit false n)! < ↑(bit false n)
[PROOFSTEP]
simpa [bit0_eq_two_mul n]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
[PROOFSTEP]
suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
  simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0, bit0_eq_two_mul n]
[GOAL]
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
[PROOFSTEP]
simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0, bit0_eq_two_mul n]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
[PROOFSTEP]
rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n) + 1
[PROOFSTEP]
refine' this.trans _
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1
[PROOFSTEP]
exact_mod_cast lt_succ_self _


[GOAL]
x✝¹ x✝ : ℕ
⊢ (fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝
[PROOFSTEP]
dsimp only
[GOAL]
x✝¹ x✝ : ℕ
⊢ (x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
[PROOFSTEP]
rw [Nat.add_comm, Nat.right_distrib, Nat.one_mul]
[GOAL]
m n k : ℕ
p : ℕ → Prop
⊢ (∃ n, p n) → p 0 ∨ ∃ n, p (n + 1)
[PROOFSTEP]
rintro ⟨_ | n, hn⟩
[GOAL]
case intro.zero
m n k : ℕ
p : ℕ → Prop
hn : p zero
⊢ p 0 ∨ ∃ n, p (n + 1)
case intro.succ m n✝ k : ℕ p : ℕ → Prop n : ℕ hn : p (succ n) ⊢ p 0 ∨ ∃ n, p (n + 1)
[PROOFSTEP]
exacts [Or.inl hn, Or.inr ⟨n, hn⟩]
[GOAL]
m✝ n✝ k m n : ℕ
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
by_cases h1 : m ≤ n
[GOAL]
case pos
m✝ n✝ k m n : ℕ
h1 : m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
case neg m✝ n✝ k m n : ℕ h1 : ¬m ≤ n ⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [max_eq_right h1, max_eq_right (succ_le_succ h1)]
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [not_le] at h1
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
have h2 := le_of_lt h1
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
h2 : n ≤ m
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [max_eq_left h2, max_eq_left (succ_le_succ h2)]
[GOAL]
m✝ n✝ k m n : ℕ
⊢ m < n ↔ m + 1 ≤ n
[PROOFSTEP]
rw [succ_le_iff]
[GOAL]
m n k a b : ℕ
⊢ a < 1 + b ↔ a ≤ b
[PROOFSTEP]
simp only [add_comm, lt_succ_iff]
[GOAL]
m n k a b : ℕ
⊢ 1 + a ≤ b ↔ a < b
[PROOFSTEP]
simp only [add_comm, add_one_le_iff]
[GOAL]
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m / n ≤ k ↔ m ≤ n * k + (n - 1)
[PROOFSTEP]
rw [← lt_succ_iff, div_lt_iff_lt_mul n0, succ_mul, mul_comm]
[GOAL]
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m < n * k + n ↔ m ≤ n * k + (n - 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
m✝ n k✝ m k : ℕ
n0 : 0 < zero
⊢ m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)
[PROOFSTEP]
cases n0
[GOAL]
case succ
m✝ n k✝ m k n✝ : ℕ
n0 : 0 < succ n✝
⊢ m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)
[PROOFSTEP]
exact lt_succ_iff
[GOAL]
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 < n + 3
[PROOFSTEP]
rw [Nat.lt_iff_add_one_le]
[GOAL]
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 + 1 ≤ n + 3
[PROOFSTEP]
convert Nat.le_add_left 3 n
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n
[PROOFSTEP]
simp only [lt_succ_iff, Decidable.le_iff_eq_or_lt, forall_eq_or_imp, and_comm]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)
[PROOFSTEP]
push_neg
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → ¬P m) ↔ (∀ (m : ℕ), m < n → ¬P m) ∧ ¬P n
[PROOFSTEP]
exact forall_lt_succ
[GOAL]
m n k : ℕ
h : m < n
⊢ n = m + (n - (m + 1)) + 1
[PROOFSTEP]
rw [add_right_comm, add_sub_of_le h]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ n + succ m - 1 = n + m
[PROOFSTEP]
rw [add_succ, succ_sub_one]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ succ n + m - 1 = n + m
[PROOFSTEP]
rw [succ_add, succ_sub_one]
[GOAL]
m✝ n✝ k m n : ℕ
H : m = succ n
⊢ pred m = n
[PROOFSTEP]
simp [H]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ pred n = succ m ↔ n = m + 2
[PROOFSTEP]
cases n
[GOAL]
case zero
m✝ n k m : ℕ
⊢ pred zero = succ m ↔ zero = m + 2
[PROOFSTEP]
constructor
[GOAL]
case succ
m✝ n k m n✝ : ℕ
⊢ pred (succ n✝) = succ m ↔ succ n✝ = m + 2
[PROOFSTEP]
constructor
[GOAL]
case zero.mp
m✝ n k m : ℕ
⊢ pred zero = succ m → zero = m + 2
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case zero.mpr
m✝ n k m : ℕ
⊢ zero = m + 2 → pred zero = succ m
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mp
m✝ n k m n✝ : ℕ
⊢ pred (succ n✝) = succ m → succ n✝ = m + 2
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mpr
m✝ n k m n✝ : ℕ
⊢ succ n✝ = m + 2 → pred (succ n✝) = succ m
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mp.refl
m✝ n k m : ℕ
⊢ succ (succ m) = m + 2
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr.refl
m✝ n k m : ℕ
⊢ pred (succ (Nat.add m 1)) = succ m
[PROOFSTEP]
rfl
[GOAL]
m✝ n✝ k n m : ℕ
⊢ pred n - m = pred (n - m)
[PROOFSTEP]
rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]
[GOAL]
m n✝ k n : ℕ
⊢ pred (1 + n) = n
[PROOFSTEP]
rw [add_comm, add_one, Nat.pred_succ]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2
[PROOFSTEP]
rw [add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ ¬0 = 1
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ k n m : ℕ
⊢ 1 < 2
[PROOFSTEP]
simp
[GOAL]
m n k a b : ℕ
ha : 0 < a
this : a * b = a * 1 ↔ b = 1
⊢ a * b = a ↔ b = 1
[PROOFSTEP]
rwa [mul_one] at this
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a * b = b ↔ a = 1
[PROOFSTEP]
rw [mul_comm, Nat.mul_right_eq_self_iff hb]
[GOAL]
m n✝ k : ℕ
C : ℕ → Sort u
n : ℕ
h : n ≤ n
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
cases n
[GOAL]
case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
unfold leRecOn Eq.recOn
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
unfold leRecOn Eq.recOn
[GOAL]
case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ (_ : zero = 0) ▸ x = x
[PROOFSTEP]
simp
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
      fun h => h ▸ x) =
    x
[PROOFSTEP]
unfold Or.by_cases
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
    else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =
    x
[PROOFSTEP]
rw [dif_neg (Nat.not_succ_le_self _)]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
conv =>
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
lhs
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x
[PROOFSTEP]
rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m n✝ k : ℕ
C : ℕ → Sort u
n : ℕ
h : n ≤ n + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h (fun {k} => next) x = next x
[PROOFSTEP]
rw [leRecOn_succ (le_refl n), leRecOn_self]
[GOAL]
m✝ n✝ k✝ : ℕ
C : ℕ → Sort u
n m k : ℕ
hnm : n ≤ m
hmk : m ≤ k
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)
[PROOFSTEP]
induction' hmk with k hmk ih
[GOAL]
case refl
m✝ n✝ k✝ : ℕ
C : ℕ → Sort u
n m k : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
case step
m✝ n✝ k✝¹ : ℕ
C : ℕ → Sort u
n m k✝ : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
k : ℕ
hmk : Nat.le m k
ih : leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)
⊢ leRecOn (_ : n ≤ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)
[PROOFSTEP]
rw [leRecOn_succ (le_trans hnm hmk), ih, leRecOn_succ]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 (fun {k} => next) (next x) = leRecOn h1 (fun {k} => next) x
[PROOFSTEP]
rw [Subsingleton.elim h1 (le_trans (le_succ n) h2), leRecOn_trans (le_succ n) h2, leRecOn_succ']
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn hnm fun {k} => next)
[PROOFSTEP]
induction' hnm with m hnm ih
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn (_ : Nat.le n n) fun {k} => next)
[PROOFSTEP]
intro x y H
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
x y : C n
H : leRecOn (_ : Nat.le n n) (fun {k} => next) x = leRecOn (_ : Nat.le n n) (fun {k} => next) y
⊢ x = y
[PROOFSTEP]
rwa [leRecOn_self, leRecOn_self] at H
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
⊢ Function.Injective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
[PROOFSTEP]
intro x y H
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) y
⊢ x = y
[PROOFSTEP]
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y
[PROOFSTEP]
exact ih (Hnext _ H)
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn hnm fun {k} => next)
[PROOFSTEP]
induction' hnm with m hnm ih
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn (_ : Nat.le n n) fun {k} => next)
[PROOFSTEP]
intro x
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n n) (fun {k} => next) a = x
[PROOFSTEP]
use x
[GOAL]
case h
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ leRecOn (_ : Nat.le n n) (fun {k} => next) x = x
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
⊢ Function.Surjective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
[PROOFSTEP]
intro x
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C (succ m)
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = x
[PROOFSTEP]
rcases Hnext _ x with ⟨w, rfl⟩
[GOAL]
case step.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
w : C m
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next w
[PROOFSTEP]
rcases ih w with ⟨x, rfl⟩
[GOAL]
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)
[PROOFSTEP]
use x
[GOAL]
case h
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)
[PROOFSTEP]
rw [leRecOn_succ]
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
n : ℕ
⊢ strongRecOn' n h = h n fun m x => strongRecOn' m h
[PROOFSTEP]
simp only [strongRecOn']
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
n : ℕ
⊢ Nat.strongRec' h n = h n fun m x => Nat.strongRec' h m
[PROOFSTEP]
rw [Nat.strongRec']
[GOAL]
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ (n : ℕ) (hn : m ≤ n), P n hn
[PROOFSTEP]
apply Nat.le.rec
[GOAL]
case refl
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ P m (_ : Nat.le m m)
[PROOFSTEP]
exact base
[GOAL]
case step
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ {m_1 : ℕ} (a : Nat.le m m_1), P m_1 a → P (Nat.succ m_1) (_ : Nat.le m (Nat.succ m_1))
[PROOFSTEP]
intros n hn
[GOAL]
case step
m✝ n✝ k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
n : ℕ
hn : Nat.le m n
⊢ P n hn → P (Nat.succ n) (_ : Nat.le m (Nat.succ n))
[PROOFSTEP]
apply succ n hn
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
n : ℕ
nn : n ≤ n
hP : P n
⊢ decreasingInduction h nn hP = hP
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
n : ℕ
nn : n ≤ n
hP : P n
⊢ leRecOn nn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP = hP
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ decreasingInduction h msn hP = decreasingInduction h mn (h n hP)
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ leRecOn msn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP =
    leRecOn mn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) (h n hP)
[PROOFSTEP]
rw [leRecOn_succ]
[GOAL]
m✝ n k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m : ℕ
msm : m ≤ m + 1
hP : P (m + 1)
⊢ decreasingInduction h msm hP = h m hP
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m✝ n k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m : ℕ
msm : m ≤ m + 1
hP : P (m + 1)
⊢ leRecOn msm (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP = h m hP
[PROOFSTEP]
rw [leRecOn_succ']
[GOAL]
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
nk : n ≤ k
hP : P k
⊢ decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
[PROOFSTEP]
induction' nk with k nk ih
[GOAL]
case refl
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
hP✝ : P k
hP : P n
⊢ decreasingInduction h (_ : m ≤ n) hP = decreasingInduction h mn (decreasingInduction h (_ : Nat.le n n) hP)
[PROOFSTEP]
rw [decreasingInduction_self]
[GOAL]
case step
m✝ n✝ k✝¹ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k✝ : ℕ
mn : m ≤ n
hP✝ : P k✝
k : ℕ
nk : Nat.le n k
ih : ∀ (hP : P k), decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
hP : P (succ k)
⊢ decreasingInduction h (_ : m ≤ succ k) hP =
    decreasingInduction h mn (decreasingInduction h (_ : Nat.le n (succ k)) hP)
[PROOFSTEP]
rw [decreasingInduction_succ h (le_trans mn nk), ih, decreasingInduction_succ]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
smn : m + 1 ≤ n
mn : m ≤ n
hP : P n
⊢ decreasingInduction h mn hP = h m (decreasingInduction h smn hP)
[PROOFSTEP]
rw [Subsingleton.elim mn (le_trans (le_succ m) smn), decreasingInduction_trans, decreasingInduction_succ']
[GOAL]
case msm
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
smn : m + 1 ≤ n
mn : m ≤ n
hP : P n
⊢ m ≤ m + 1
[PROOFSTEP]
apply Nat.le_succ
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m
[PROOFSTEP]
revert h hP
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
[PROOFSTEP]
refine' leRecOn' mn _ _
[GOAL]
case refine'_1
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ⦃k : ℕ⦄ →
    m ≤ k →
      (((k_1 : ℕ) → k_1 < k → m ≤ k_1 → P (k_1 + 1) → P k_1) → P k → P m) →
        ((k_1 : ℕ) → k_1 < k + 1 → m ≤ k_1 → P (k_1 + 1) → P k_1) → P (k + 1) → P m
[PROOFSTEP]
intro n mn ih h hP
[GOAL]
case refine'_1
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ P m
[PROOFSTEP]
apply ih
[GOAL]
case refine'_1.h
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
[PROOFSTEP]
exact fun k hk => h k (Nat.lt.step hk)
[GOAL]
case refine'_1.hP
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ P n
[PROOFSTEP]
exact h n (lt_succ_self n) mn hP
[GOAL]
case refine'_2
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ((k : ℕ) → k < m → m ≤ k → P (k + 1) → P k) → P m → P m
[PROOFSTEP]
intro _ hP
[GOAL]
case refine'_2
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
h✝ : (k : ℕ) → k < m → m ≤ k → P (k + 1) → P k
hP : P m
⊢ P m
[PROOFSTEP]
exact hP
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a
[PROOFSTEP]
rw [le_div_iff_mul_le hb, one_mul]
[GOAL]
m✝ n✝ k✝ n m : ℕ
h : n ≤ m
k : ℕ
k0 : k = 0
⊢ n / k ≤ m / k
[PROOFSTEP]
simp [k0]
[GOAL]
m n k a b : ℕ
hba : b ≤ a
hb : 0 < b
h : a / b = 0
⊢ a = a % b
[PROOFSTEP]
simpa [h] using (mod_add_div a b).symm
[GOAL]
m n k a b c : ℕ
hc0 : c = 0
⊢ a * (b / c) ≤ a * b / c
[PROOFSTEP]
simp [hc0]
[GOAL]
m n k a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c) * c ≤ a * b
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
m n k a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c * c) ≤ a * b
[PROOFSTEP]
exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _)
[GOAL]
m n k a b c : ℕ
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c
[PROOFSTEP]
rw [← H2, Nat.mul_div_cancel' H1]
[GOAL]
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c
[PROOFSTEP]
exact Nat.div_eq_iff_eq_mul_right H H'
[GOAL]
m n k a b c : ℕ
H1 : b ∣ a
H2 : a / b = c
⊢ a = c * b
[PROOFSTEP]
rw [mul_comm, Nat.eq_mul_of_div_eq_right H1 H2]
[GOAL]
m n k a b : ℕ
Hd : a ∣ b
⊢ a * (b / a) = b
[PROOFSTEP]
rw [mul_comm, Nat.div_mul_cancel Hd]
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a < a / b * b + b
[PROOFSTEP]
rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a / b < succ (a / b)
[PROOFSTEP]
exact Nat.lt_succ_self _
[GOAL]
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
⊢ a / d = b / d ↔ a = b
[PROOFSTEP]
refine ⟨fun h => ?_, congr_arg fun n => n / d⟩
[GOAL]
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b
[PROOFSTEP]
rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]
[GOAL]
m n k a b : ℕ
h : b ≠ 0
⊢ a % b = a ↔ a < b
[PROOFSTEP]
cases b
[GOAL]
case zero
m n k a : ℕ
h : zero ≠ 0
⊢ a % zero = a ↔ a < zero
case succ m n k a n✝ : ℕ h : succ n✝ ≠ 0 ⊢ a % succ n✝ = a ↔ a < succ n✝
[PROOFSTEP]
contradiction
[GOAL]
case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
[PROOFSTEP]
exact ⟨fun h => h.ge.trans_lt (mod_lt _ (succ_pos _)), mod_eq_of_lt⟩
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m % k + m / k * k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m % k + k * (m / k) = m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m / k * k + m % k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m✝ n k✝ m k : ℕ
⊢ k * (m / k) + m % k = m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
m✝ n✝ k✝ n k m d : ℕ
h : 0 < k
x✝ : m + k * d = n ∧ m < k
h₁ : m + k * d = n
h₂ : m < k
⊢ (m + k * d) / k = d ∧ (m + k * d) % k = m
[PROOFSTEP]
rw [add_mul_div_left _ _ h, add_mul_mod_self_left]
[GOAL]
m✝ n✝ k✝ n k m d : ℕ
h : 0 < k
x✝ : m + k * d = n ∧ m < k
h₁ : m + k * d = n
h₂ : m < k
⊢ m / k + d = d ∧ m % k = m
[PROOFSTEP]
simp [div_eq_of_lt, mod_eq_of_lt, h₂]
[GOAL]
m n k a b c : ℕ
ha : 0 < a
d : ℕ
⊢ a * c = a * b * d ↔ c = b * d
[PROOFSTEP]
rw [mul_assoc, mul_right_inj' ha.ne']
[GOAL]
m n k a b c : ℕ
hc : 0 < c
d : ℕ
⊢ b * c = a * c * d ↔ b = a * d
[PROOFSTEP]
rw [mul_right_comm, mul_left_inj' hc.ne']
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = n % m
[PROOFSTEP]
conv =>
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
rhs
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % m
[PROOFSTEP]
rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
[PROOFSTEP]
rcases h with ⟨t, rfl⟩
[GOAL]
case intro
m✝ n✝ k n m t : ℕ
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m
[PROOFSTEP]
rw [mul_assoc, add_mul_mod_self_left]
[GOAL]
m✝ n✝ k✝ m n k i : ℕ
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n
[PROOFSTEP]
rw [← mod_add_mod, ← mod_add_mod k, H]
[GOAL]
m✝ n✝ k✝ m n k i : ℕ
H : m % n = k % n
⊢ (i + m) % n = (i + k) % n
[PROOFSTEP]
rw [add_comm, add_mod_eq_add_mod_right _ H, add_comm]
[GOAL]
m n k a b c : ℕ
hab : c ∣ b
h : a ∣ b / c
h1 : ∃ d, b / c = a * d
d : ℕ
hd : b / c = a * d
h3 : b = a * d * c
⊢ b = c * a * d
[PROOFSTEP]
rwa [mul_comm, ← mul_assoc] at h3
[GOAL]
m n k a b : ℕ
w : a ∣ b
h : b / a = 1
⊢ a = b
[PROOFSTEP]
rw [← Nat.div_mul_cancel w, h, one_mul]
[GOAL]
m n k a b : ℕ
w : a ∣ b
h : b / a = 0
⊢ b = 0
[PROOFSTEP]
rw [← Nat.div_mul_cancel w, h, zero_mul]
[GOAL]
m✝ n✝ k m n : ℕ
n0 : 0 < n
⊢ m < n * (m / n + 1)
[PROOFSTEP]
rw [mul_comm, ← Nat.div_lt_iff_lt_mul' n0]
[GOAL]
m✝ n✝ k m n : ℕ
n0 : 0 < n
⊢ m / n < m / n + 1
[PROOFSTEP]
exact lt_succ_self _
[GOAL]
m n k a b c : ℕ
⊢ (a * b + c) % b = c % b
[PROOFSTEP]
simp [Nat.add_mod]
[GOAL]
m n k a b c : ℕ
h : c < b
⊢ (a * b + c) % b = c
[PROOFSTEP]
rw [Nat.mul_add_mod, Nat.mod_eq_of_lt h]
[GOAL]
m n✝ k n : ℕ
⊢ pred n = n ↔ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
m n k : ℕ
⊢ pred zero = zero ↔ zero = 0
[PROOFSTEP]
simp [(Nat.succ_ne_self _).symm]
[GOAL]
case succ
m n k n✝ : ℕ
⊢ pred (succ n✝) = succ n✝ ↔ succ n✝ = 0
[PROOFSTEP]
simp [(Nat.succ_ne_self _).symm]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
[PROOFSTEP]
constructor
[GOAL]
case mp
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ p (Nat.find h) ∧ ∀ (n : ℕ), n < Nat.find h → ¬p n
[PROOFSTEP]
exact ⟨Nat.find_spec h, fun _ => Nat.find_min h⟩
[GOAL]
case mpr
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m
[PROOFSTEP]
rintro ⟨hm, hlt⟩
[GOAL]
case mpr.intro
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find h = m
[PROOFSTEP]
exact le_antisymm (Nat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| Nat.find_spec h)
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m
[PROOFSTEP]
simp only [exists_prop, ← lt_succ_iff, find_lt_iff]
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
[PROOFSTEP]
simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
[PROOFSTEP]
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = 0 ↔ p 0
[PROOFSTEP]
simp [find_eq_iff]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
⊢ Nat.find h₁ = Nat.find h₂ + 1
[PROOFSTEP]
refine' (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn => _⟩
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
hn : zero < Nat.find h₂ + 1
⊢ ¬p zero
case succ
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : succ n < Nat.find h₂ + 1
⊢ ¬p (succ n)
[PROOFSTEP]
exacts [h0, @Nat.find_min (fun n => p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]
[GOAL]
m n✝ k : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
b n : ℕ
h : P (n + 1)
⊢ Nat.findGreatest P (n + 1) = n + 1
[PROOFSTEP]
simp [Nat.findGreatest, h]
[GOAL]
m n k : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
b : ℕ
h : ¬P (b + 1)
⊢ Nat.findGreatest P (b + 1) = Nat.findGreatest P b
[PROOFSTEP]
simp [Nat.findGreatest, h]
[GOAL]
m n✝ k : ℕ
P : (k : ℕ) → k < 0 → Prop
x✝ : (n : ℕ) → (h : n < 0) → Decidable (P n h)
n : ℕ
h : n < 0
⊢ P n h
[PROOFSTEP]
cases h
[GOAL]
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
cases' decidableBallLT n fun k h => P k (lt_succ_of_lt h) with h h
[GOAL]
case isFalse
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
refine' isFalse (mt _ h)
[GOAL]
case isFalse
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h) → ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
[PROOFSTEP]
intro hn k h
[GOAL]
case isFalse
m n✝ k✝ n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h✝ : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
hn : ∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h
k : ℕ
h : k < n
⊢ P k (_ : k < succ n)
[PROOFSTEP]
apply hn
[GOAL]
case isTrue
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
by_cases p : P n (lt_succ_self n)
[GOAL]
case pos
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
p : P n (_ : n < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
exact
  isTrue fun k h' =>
    (le_of_lt_succ h').lt_or_eq_dec.elim (h _) fun e =>
      match k, e, h' with
      | _, rfl, _ => p
[GOAL]
case neg
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
p : ¬P n (_ : n < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
exact isFalse (mt (fun hn => hn _ _) p)
[GOAL]
m n k : ℕ
P : ℕ → Prop
h : DecidablePred P
⊢ ¬(fun n => ∃ m, m < n ∧ P m) 0
[PROOFSTEP]
simp
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
h : DecidablePred P
n : ℕ
⊢ (fun n_1 => ∃ m, m < n_1 ∧ ?m.69545 n m) n ∨ P n ↔ (fun n => ∃ m, m < n ∧ P m) (n + 1)
[PROOFSTEP]
simp only [lt_succ_iff_lt_or_eq, or_and_right, exists_or, exists_eq_left]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
h : DecidablePred P
n : ℕ
⊢ (∃ m, m < n ∧ ?m.69545 n m) ∨ P n ↔ (∃ x, x < n ∧ P x) ∨ P n
[PROOFSTEP]
apply Iff.refl


[GOAL]
n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 0 ↔ none = 0 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 0 ↔ none = 0 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
case some.some val✝¹ val✝ : ℕ ⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
[GOAL]
case none.none
⊢ none + none = 0 ↔ none = 0 ∧ none = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 0 ↔ none = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 0 ↔ some val✝ = 0 ∧ none = 0
case some.some val✝¹ val✝ : ℕ ⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ some val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 0 ↔ val✝¹ = 0 ∧ val✝ = 0
[PROOFSTEP]
exact add_eq_zero_iff' (zero_le _) (zero_le _)
[GOAL]
n m : WithBot ℕ
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 1 ↔ none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 1 ↔ none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 1 ↔ some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 1 ↔ none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 1 ∨ none = 1 ∧ none = 0
⊢ none + none = 1
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 1 ↔ none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 1 ∨ none = 1 ∧ some val✝ = 0
⊢ none + some val✝ = 1
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 1 ↔ some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 1 ∨ some val✝ = 1 ∧ none = 0
⊢ some val✝ + none = 1
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ some val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ some val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ some val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = 1 ↔ val✝¹ = 0 ∧ val✝ = 1 ∨ val✝¹ = 1 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_one_iff
[GOAL]
n m : WithBot ℕ
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 2 ↔ none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 2 ↔ none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 2 ↔ some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 2 ↔ none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 2 ∨ none = 1 ∧ none = 1 ∨ none = 2 ∧ none = 0
⊢ none + none = 2
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 2 ↔ none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 2 ∨ none = 1 ∧ some val✝ = 1 ∨ none = 2 ∧ some val✝ = 0
⊢ none + some val✝ = 2
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 2 ↔ some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 2 ∨ some val✝ = 1 ∧ none = 1 ∨ some val✝ = 2 ∧ none = 0
⊢ some val✝ + none = 2
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    some val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ some val✝ = 2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ val✝ = ↑2 ∨ some val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔
    val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ some val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ some val✝¹ = 2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑2 ↔ val✝¹ = 0 ∧ val✝ = ↑2 ∨ val✝¹ = 1 ∧ val✝ = 1 ∨ val✝¹ = ↑2 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_two_iff
[GOAL]
n m : WithBot ℕ
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
[PROOFSTEP]
rcases n, m with ⟨_ | _, _ | _⟩
[GOAL]
case none.none
⊢ none + none = 3 ↔ none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
case none.some
val✝ : ℕ
⊢ none + some val✝ = 3 ↔
    none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
case some.none
val✝ : ℕ
⊢ some val✝ + none = 3 ↔
    some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop
[GOAL]
case none.none
⊢ none + none = 3 ↔ none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.none
h : none = 0 ∧ none = 3 ∨ none = 1 ∧ none = 2 ∨ none = 2 ∧ none = 1 ∨ none = 3 ∧ none = 0
⊢ none + none = 3
[PROOFSTEP]
aesop
[GOAL]
case none.some
val✝ : ℕ
⊢ none + some val✝ = 3 ↔
    none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case none.some
val✝ : ℕ
h : none = 0 ∧ some val✝ = 3 ∨ none = 1 ∧ some val✝ = 2 ∨ none = 2 ∧ some val✝ = 1 ∨ none = 3 ∧ some val✝ = 0
⊢ none + some val✝ = 3
[PROOFSTEP]
aesop
[GOAL]
case some.none
val✝ : ℕ
⊢ some val✝ + none = 3 ↔
    some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ = 0 ∧ none = 3 ∨ some val✝ = 1 ∧ none = 2 ∨ some val✝ = 2 ∧ none = 1 ∨ some val✝ = 3 ∧ none = 0
⊢ some val✝ + none = 3
[PROOFSTEP]
aesop
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
repeat' erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ some val✝¹ + some val✝ = 3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    some val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ some val✝ = 3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨
      some val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ some val✝ = 2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ some val✝¹ = 2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ some val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ some val✝¹ = 3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ some val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ val✝ = 0
[PROOFSTEP]
erw [WithBot.coe_eq_coe]
[GOAL]
case some.some
val✝¹ val✝ : ℕ
⊢ (fun x x_1 => x + x_1) val✝¹ val✝ = ↑3 ↔
    val✝¹ = 0 ∧ val✝ = ↑3 ∨ val✝¹ = 1 ∧ val✝ = ↑2 ∨ val✝¹ = ↑2 ∧ val✝ = 1 ∨ val✝¹ = ↑3 ∧ val✝ = 0
[PROOFSTEP]
exact Nat.add_eq_three_iff
[GOAL]
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
rw [← WithBot.coe_zero]
[GOAL]
n : ℕ
⊢ ↑0 ≤ ↑n
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr (Nat.zero_le n)
[GOAL]
n : WithBot ℕ
⊢ n < 0 ↔ n = ⊥
[PROOFSTEP]
refine' Option.casesOn n _ _
[GOAL]
case refine'_1
n : WithBot ℕ
⊢ none < 0 ↔ none = ⊥
case refine'_2 n : WithBot ℕ ⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
[PROOFSTEP]
exact of_eq_true (eq_true_of_decide (Eq.refl true))
[GOAL]
case refine'_2
n : WithBot ℕ
⊢ ∀ (val : ℕ), some val < 0 ↔ some val = ⊥
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
n✝ : WithBot ℕ
n : ℕ
⊢ some n < 0 ↔ some n = ⊥
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_2.refine'_1
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ some n = ⊥
case refine'_2.refine'_2 n✝ : WithBot ℕ n : ℕ h : some n = ⊥ ⊢ some n < 0
[PROOFSTEP]
exfalso
[GOAL]
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : some n < 0
⊢ False
[PROOFSTEP]
rw [WithBot.some_eq_coe] at h
[GOAL]
case refine'_2.refine'_1.h
n✝ : WithBot ℕ
n : ℕ
h : ↑n < 0
⊢ False
[PROOFSTEP]
exact not_le_of_lt h WithBot.coe_nonneg
[GOAL]
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ some n < 0
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_2.refine'_2
n✝ : WithBot ℕ
n : ℕ
h : some n = ⊥
⊢ ⊥ < 0
[PROOFSTEP]
exact of_eq_true (eq_true_of_decide (Eq.refl true))
[GOAL]
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x
[PROOFSTEP]
refine' ⟨fun h => lt_of_lt_of_le (WithBot.coe_lt_coe.mpr zero_lt_one) h, fun h => _⟩
[GOAL]
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
[PROOFSTEP]
induction x using WithBot.recBotCoe
[GOAL]
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥
[PROOFSTEP]
exact (not_lt_bot h).elim
[GOAL]
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
[PROOFSTEP]
exact WithBot.coe_le_coe.mpr (Nat.succ_le_iff.mpr (WithBot.coe_lt_coe.mp h))
[GOAL]
x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0
[PROOFSTEP]
simpa using one_le_iff_zero_lt
[GOAL]
n m : WithBot ℕ
h : n < m
⊢ n + 1 ≤ m
[PROOFSTEP]
cases n
[GOAL]
case none
m : WithBot ℕ
h : none < m
⊢ none + 1 ≤ m
[PROOFSTEP]
exact bot_le
[GOAL]
case some
m : WithBot ℕ
val✝ : ℕ
h : some val✝ < m
⊢ some val✝ + 1 ≤ m
[PROOFSTEP]
cases m
[GOAL]
case some.none
val✝ : ℕ
h : some val✝ < none
⊢ some val✝ + 1 ≤ none
case some.some val✝¹ val✝ : ℕ h : some val✝¹ < some val✝ ⊢ some val✝¹ + 1 ≤ some val✝
[PROOFSTEP]
exacts [(not_lt_bot h).elim, WithBot.some_le_some.2 (WithBot.some_lt_some.1 h)]