[GOAL]
b : Bool
⊢ (b::zero b) = zero b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ (false::zero false) = zero false
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ (true::zero true) = zero true
[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ (b::zero (decide ¬b = true)) = nz (msb b)
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ (false::zero (decide ¬false = true)) = nz (msb false)
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ (true::zero (decide ¬true = true)) = nz (msb true)
[PROOFSTEP]
rfl
[GOAL]
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (nz (msb b))
[PROOFSTEP]
rw [← bit_one]
[GOAL]
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))
[PROOFSTEP]
exact s b (SNum.zero (Not b)) (z (Not b))


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t x : Multiset α
⊢ x ∈ (fun s t => Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (Finset.Icc (↑toDFinsupp s) (↑toDFinsupp t))) s t ↔
    s ≤ x ∧ x ≤ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (Finset.Icc (↑toDFinsupp (s ⊓ t)) (↑toDFinsupp (s ⊔ t))) =
    Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (uIcc (↑toDFinsupp s) (↑toDFinsupp t))
[PROOFSTEP]
simp [uIcc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Icc s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s)
[PROOFSTEP]
simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply, toDFinsupp_support]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ico s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ioc s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ioo s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (uIcc s t) = ∏ i in toFinset s ∪ toFinset t, (Int.natAbs (↑(count i t) - ↑(count i s)) + 1)
[PROOFSTEP]
simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply, toDFinsupp_support]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Iic s) = ∏ i in toFinset s, (count i s + 1)
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]


[GOAL]
b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
[PROOFSTEP]
rw [log, dite_eq_right_iff]
[GOAL]
b n : ℕ
⊢ (∀ (h : b ≤ n ∧ 1 < b),
      (let_fun this := (_ : n / b < n);
        log b (n / b) + 1) =
        0) ↔
    n < b ∨ b ≤ 1
[PROOFSTEP]
simp only [Nat.succ_ne_zero, imp_false, not_and_or, not_le, not_lt]
[GOAL]
b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, log_eq_zero_iff, not_or, not_lt, not_le]
[GOAL]
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1
[PROOFSTEP]
rw [log]
[GOAL]
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then
      let_fun this := (_ : n / b < n);
      log b (n / b) + 1
    else 0) =
    log b (n / b) + 1
[PROOFSTEP]
exact if_pos ⟨hn, h⟩
[GOAL]
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
induction' y using Nat.strong_induction_on with y ih generalizing x
[GOAL]
case h
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
cases x with
| zero => exact iff_of_true hy.bot_lt (zero_le _)
| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
cases x with
| zero => exact iff_of_true hy.bot_lt (zero_le _)
| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
x y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ zero ≤ y ↔ zero ≤ log b y
[PROOFSTEP]

| zero => exact iff_of_true hy.bot_lt (zero_le _)
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
x y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ zero ≤ y ↔ zero ≤ log b y
[PROOFSTEP]
exact iff_of_true hy.bot_lt (zero_le _)
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔ succ x ≤ log b y
[PROOFSTEP]

| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔ succ x ≤ log b y
[PROOFSTEP]
rw [log]
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      if h : b ≤ y ∧ 1 < b then
        let_fun this := (_ : y / b < y);
        log b (y / b) + 1
      else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
[PROOFSTEP]
have b_pos : 0 < b := zero_le_one.trans_lt hb
[GOAL]
case pos
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
[PROOFSTEP]
rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
  le_div_iff_mul_le b_pos, pow_succ', mul_comm]
[GOAL]
case neg
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ succ x ≤ y ↔ succ x ≤ 0
[PROOFSTEP]
exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y
[PROOFSTEP]
refine' (le_or_lt b 1).elim (fun hb => _) fun hb => (pow_le_iff_le_log hb hy).2 h
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y
[PROOFSTEP]
rw [log_of_left_le_one hb, nonpos_iff_eq_zero] at h
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
[PROOFSTEP]
rwa [h, pow_zero, one_le_iff_ne_zero]
[GOAL]
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y
[PROOFSTEP]
rcases ne_or_eq y 0 with (hy | rfl)
[GOAL]
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y
case inr b x : ℕ hb : 1 < b h : b ^ x ≤ 0 ⊢ x ≤ log b 0
[PROOFSTEP]
exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim]
[GOAL]
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
[GOAL]
case inl.intro
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rw [le_antisymm_iff, ← lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and_comm]
[GOAL]
case inl.intro.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
have hm : m ≠ 0 := h.resolve_right hbn
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rw [not_and_or, not_lt, Ne.def, not_not] at hbn
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rcases hbn with (hb | rfl)
[GOAL]
case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
simpa only [log_of_left_le_one hb, hm.symm, false_iff_iff, not_and, not_lt] using
  le_trans (pow_le_pow_of_le_one' hb m.le_succ)
[GOAL]
case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
[PROOFSTEP]
simpa only [log_zero_right, hm.symm, nonpos_iff_eq_zero, false_iff, not_and, not_lt, add_pos_iff, or_true,
  pow_eq_zero_iff] using pow_eq_zero
[GOAL]
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hm)
[GOAL]
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0
[PROOFSTEP]
rw [pow_one] at h₂
[GOAL]
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0
[PROOFSTEP]
exact log_of_lt h₂
[GOAL]
case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m
[PROOFSTEP]
exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩
[GOAL]
b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b
[PROOFSTEP]
rw [log_eq_iff (Or.inl one_ne_zero), pow_add, pow_one]
[GOAL]
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1
[PROOFSTEP]
apply log_eq_of_pow_le_of_lt_pow
[GOAL]
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b
case h₂ b n : ℕ hb : 1 < b hn : n ≠ 0 ⊢ n * b < b ^ (log b n + 1) * b
[PROOFSTEP]
exacts [mul_le_mul_right' (pow_log_le_self _ hn) _,
  (mul_lt_mul_right (zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]
[GOAL]
b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1
[PROOFSTEP]
rw [log_zero_right, pow_zero]
[GOAL]
b : ℕ
⊢ Monotone (log b)
[PROOFSTEP]
refine' monotone_nat_of_le_succ fun n => _
[GOAL]
b n : ℕ
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
rw [log_of_left_le_one hb]
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0
[PROOFSTEP]
rw [log_zero_right, log_zero_right]
[GOAL]
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
[PROOFSTEP]
apply le_log_of_pow_le hc
[GOAL]
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n
[PROOFSTEP]
calc
  c ^ log b n ≤ b ^ log b n := pow_le_pow_of_le_left' hb _
  _ ≤ n := pow_log_le_self _ hn
[GOAL]
b n : ℕ
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
cases' lt_or_le n b with h h
[GOAL]
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
[GOAL]
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]
[GOAL]
b n : ℕ
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb]
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
cases' lt_or_le n b with h h
[GOAL]
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [div_eq_of_lt h, zero_mul, log_zero_right, log_of_lt h]
[GOAL]
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [log_mul_base hb (Nat.div_pos h (zero_le_one.trans_lt hb)).ne', log_div_base,
  tsub_add_cancel_of_le (succ_le_iff.2 <| log_pos hb h)]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n
[PROOFSTEP]
rw [div_lt_iff_lt_mul (zero_lt_one.trans hb), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
[PROOFSTEP]
exact add_le_mul hn hb
[GOAL]
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ clog b n = 0
[PROOFSTEP]
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.1.not_le hb]
[GOAL]
n : ℕ
hn : n ≤ 1
b : ℕ
⊢ clog b n = 0
[PROOFSTEP]
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.2.not_le hn]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ clog b n = clog b ((n + b - 1) / b) + 1
[PROOFSTEP]
rw [clog, dif_pos (⟨hb, hn⟩ : 1 < b ∧ 1 < n)]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b n
[PROOFSTEP]
rw [clog_of_two_le hb hn]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1
[PROOFSTEP]
exact zero_lt_succ _
[GOAL]
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1
[PROOFSTEP]
rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
[PROOFSTEP]
have n_pos : 0 < n := (zero_lt_two' ℕ).trans_le hn
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ (n + b - 1) / b ≤ 1
[PROOFSTEP]
rw [← lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul]
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ n + b ≤ b + b
[PROOFSTEP]
exact add_le_add_right h _
[GOAL]
b : ℕ
hb : 1 < b
x y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
[PROOFSTEP]
induction' x using Nat.strong_induction_on with x ih generalizing y
[GOAL]
case h
b : ℕ
hb : 1 < b
y✝ x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
[PROOFSTEP]
cases y
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ zero ↔ clog b x ≤ zero
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ zero
[PROOFSTEP]
refine' ⟨fun h => (clog_of_right_le_one h b).le, _⟩
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ zero → x ≤ 1
[PROOFSTEP]
simp_rw [← not_lt]
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬zero < clog b x → ¬1 < x
[PROOFSTEP]
contrapose!
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → zero < clog b x
[PROOFSTEP]
exact clog_pos hb
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
[PROOFSTEP]
have b_pos : 0 < b := (zero_lt_one' ℕ).trans hb
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
[PROOFSTEP]
rw [clog]
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔
    (if h : 1 < b ∧ 1 < x then
        let_fun this := (_ : (x + b - 1) / b < x);
        clog b ((x + b - 1) / b) + 1
      else 0) ≤
      succ n✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : 1 < b ∧ 1 < x
⊢ x ≤ b ^ succ n✝ ↔
    (let_fun this := (_ : (x + b - 1) / b < x);
      clog b ((x + b - 1) / b) + 1) ≤
      succ n✝
[PROOFSTEP]
rw [succ_eq_add_one, add_le_add_iff_right, ← ih ((x + b - 1) / b) (add_pred_div_lt hb h.2),
  Nat.div_le_iff_le_mul_add_pred b_pos, mul_comm b, ← pow_succ, add_tsub_assoc_of_le (Nat.succ_le_of_lt b_pos),
  add_le_add_iff_right]
[GOAL]
case neg
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : ¬(1 < b ∧ 1 < x)
⊢ x ≤ b ^ succ n✝ ↔ 0 ≤ succ n✝
[PROOFSTEP]
exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| pow_pos b_pos _) (zero_le _)
[GOAL]
b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z
[PROOFSTEP]
rw [← le_pow_iff_clog_le hb]
[GOAL]
b x : ℕ
hb : 1 < b
z : ℕ
⊢ b ^ x ≤ b ^ z ↔ x ≤ z
[PROOFSTEP]
exact (pow_right_strictMono hb).le_iff_le
[GOAL]
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ pred (clog b x) < x
[PROOFSTEP]
rw [← not_le, le_pow_iff_clog_le hb, not_le]
[GOAL]
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ pred (clog b x) < clog b x
[PROOFSTEP]
exact pred_lt (clog_pos hb hx).ne'
[GOAL]
b n m : ℕ
h : n ≤ m
⊢ clog b n ≤ clog b m
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m
[PROOFSTEP]
rw [clog_of_left_le_one hb]
[GOAL]
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m
[PROOFSTEP]
rw [← le_pow_iff_clog_le hb]
[GOAL]
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m
[PROOFSTEP]
exact h.trans (le_pow_clog hb _)
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n
[PROOFSTEP]
rw [← le_pow_iff_clog_le (lt_of_lt_of_le hc hb)]
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
[PROOFSTEP]
calc
  n ≤ c ^ clog c n := le_pow_clog hc _
  _ ≤ b ^ clog c n := pow_le_pow_of_le_left hb _
[GOAL]
b n : ℕ
⊢ log b n ≤ clog b n
[PROOFSTEP]
obtain hb | hb := le_or_lt b 1
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n
[PROOFSTEP]
rw [log_of_left_le_one hb]
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
[PROOFSTEP]
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
[PROOFSTEP]
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b zero ≤ clog b zero
[PROOFSTEP]

| zero =>
  rw [log_zero_right]
  exact zero_le _
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b zero ≤ clog b zero
[PROOFSTEP]
rw [log_zero_right]
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b zero
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (succ n) ≤ clog b (succ n)
[PROOFSTEP]

| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (succ n) ≤ clog b (succ n)
[PROOFSTEP]
exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)


[GOAL]
a : ℕ
ha : a ≤ pred a
⊢ IsMin a
[PROOFSTEP]
cases a
[GOAL]
case zero
ha : zero ≤ pred zero
⊢ IsMin zero
[PROOFSTEP]
exact isMin_bot
[GOAL]
case succ
n✝ : ℕ
ha : succ n✝ ≤ pred (succ n✝)
⊢ IsMin (succ n✝)
[PROOFSTEP]
exact (not_succ_le_self _ ha).elim
[GOAL]
a b : ℕ
h : a < b
⊢ a ≤ pred b
[PROOFSTEP]
cases b
[GOAL]
case zero
a : ℕ
h : a < zero
⊢ a ≤ pred zero
[PROOFSTEP]
exact (a.not_lt_zero h).elim
[GOAL]
case succ
a n✝ : ℕ
h : a < succ n✝
⊢ a ≤ pred (succ n✝)
[PROOFSTEP]
exact le_of_succ_le_succ h
[GOAL]
a b : ℕ
h : pred a < b
⊢ a ≤ b
[PROOFSTEP]
cases a
[GOAL]
case zero
b : ℕ
h : pred zero < b
⊢ zero ≤ b
[PROOFSTEP]
exact b.zero_le
[GOAL]
case succ
b n✝ : ℕ
h : pred (succ n✝) < b
⊢ succ n✝ ≤ b
[PROOFSTEP]
exact h
[GOAL]
a n : ℕ
⊢ succ^[n + 1] a = a + (n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', add_succ]
[GOAL]
a n : ℕ
⊢ (succ ∘ succ^[n]) a = succ (a + n)
[PROOFSTEP]
exact congr_arg _ (succ_iterate a n)
[GOAL]
a n : ℕ
⊢ pred^[n + 1] a = a - (n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', sub_succ]
[GOAL]
a n : ℕ
⊢ (pred ∘ pred^[n]) a = pred (a - n)
[PROOFSTEP]
exact congr_arg _ (pred_iterate a n)
[GOAL]
a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b
[PROOFSTEP]
rw [succ_eq_succ, succ_iterate, add_tsub_cancel_of_le h]
[GOAL]
a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a
[PROOFSTEP]
rw [pred_eq_pred, pred_iterate, tsub_tsub_cancel_of_le h]


[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0
[PROOFSTEP]
rw [count, List.range_zero, List.countp, List.countp.go]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Fintype { i // i < n ∧ p i }
[PROOFSTEP]
apply Fintype.ofFinset ((Finset.range n).filter p)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ filter p (range n) ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
intro x
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n x : ℕ
⊢ x ∈ filter p (range n) ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
rw [mem_filter, mem_range]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n x : ℕ
⊢ x < n ∧ p x ↔ x ∈ fun x => x < n ∧ p x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = card (filter p (range n))
[PROOFSTEP]
rw [count, List.countp_eq_length_filter]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.length (List.filter (fun b => decide (p b)) (List.range n)) = card (filter p (range n))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }
[PROOFSTEP]
rw [count_eq_card_filter_range, ← Fintype.card_ofFinset, ← CountSet.fintype]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (Fintype.card ↑fun x => x < n ∧ p x) = Fintype.card { k // k < n ∧ p k }
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n + 1
[PROOFSTEP]
simp [count, List.range_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n + 0
[PROOFSTEP]
simp [count, List.range_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p n ≤ count p (n + 1)
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b
[PROOFSTEP]
have : Disjoint ((range a).filter p) (((range b).map <| addLeftEmbedding a).filter p) :=
  by
  apply disjoint_filter_filter
  rw [Finset.disjoint_left]
  simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
  rintro x hx ⟨c, _, rfl⟩
  exact (self_le_add_right _ _).not_lt hx
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
[PROOFSTEP]
apply disjoint_filter_filter
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) (range b))
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → ¬a_1 ∈ map (addLeftEmbedding a) (range b)
[PROOFSTEP]
simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3, a_3 < b ∧ a + a_3 = a_1
[PROOFSTEP]
rintro x hx ⟨c, _, rfl⟩
[GOAL]
case a.intro.intro
p : ℕ → Prop
inst✝ : DecidablePred p
a b c : ℕ
left✝ : c < b
hx : a + c < a
⊢ False
[PROOFSTEP]
exact (self_le_add_right _ _).not_lt hx
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b
[PROOFSTEP]
simp_rw [count_eq_card_filter_range, range_add, filter_union, card_disjoint_union this, filter_map, addLeftEmbedding,
  card_map]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))
⊢ card (filter p (range a)) +
      card
        (filter (p ∘ ↑{ toFun := fun h => a + h, inj' := (_ : Function.Injective ((fun x x_1 => x + x_1) a)) })
          (range b)) =
    card (filter p (range a)) + card (filter (fun k => p (a + k)) (range b))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k => p (k + b)) a + count p b
[PROOFSTEP]
rw [add_comm, count_add, add_comm]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k => p (b + k)) a + count p b = count (fun k => p (k + b)) a + count p b
[PROOFSTEP]
simp_rw [add_comm b]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0
[PROOFSTEP]
simp [count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun k => p (k + 1)) n + if p 0 then 1 else 0
[PROOFSTEP]
rw [count_add', count_one]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p n < count p (n + 1) ↔ p n
[PROOFSTEP]
simp [count_succ, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n + 1 ↔ p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
by_cases h : p n
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : p n
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : ¬p n
⊢ count p (n + 1) = count p n ↔ ¬p n
[PROOFSTEP]
simp [h, count_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}
[PROOFSTEP]
rw [count_eq_card_fintype, ← Cardinal.mk_fintype]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k // k < n ∧ p k } ≤ Cardinal.mk ↑{k | p k}
[PROOFSTEP]
exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n
[PROOFSTEP]
by_contra' h : m ≠ n
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False
[PROOFSTEP]
wlog hmn : m < n
[GOAL]
case inr
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ False
[PROOFSTEP]
exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn)
[GOAL]
p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False
[PROOFSTEP]
simpa [heq] using count_strict_mono hm hmn
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ count p n ≤ card (Set.Finite.toFinset hp)
[PROOFSTEP]
rw [count_eq_card_filter_range]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ card (filter p (range n)) ≤ card (Set.Finite.toFinset hp)
[PROOFSTEP]
exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2
[GOAL]
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ count p n ≤ count q n
[PROOFSTEP]
simp only [count_eq_card_filter_range]
[GOAL]
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ card (filter p (range n)) ≤ card (filter q (range n))
[PROOFSTEP]
exact card_le_of_subset ((range n).monotone_filter_right hpq)