[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)
[PROOFSTEP]
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val
  by
  rw [this]
  exact (measure _).wf
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
⊢ WellFounded (Upto.GT p)
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
⊢ WellFounded (InvImage (fun x x_1 => x < x_1) fun y => x - ↑y)
[PROOFSTEP]
exact (measure _).wf
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
[PROOFSTEP]
ext ⟨a, ha⟩ ⟨b, _⟩
[GOAL]
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p { val := a, property := ha } { val := b, property := property✝ } ↔
    InvImage (fun x x_1 => x < x_1) (fun y => x - ↑y) { val := a, property := ha } { val := b, property := property✝ }
[PROOFSTEP]
dsimp [InvImage, Upto.GT]
[GOAL]
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b
[PROOFSTEP]
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)]
[GOAL]
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < Nat.succ ↑x
⊢ ¬p j
[PROOFSTEP]
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]
[GOAL]
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < Nat.succ ↑x
⊢ ¬p j
[PROOFSTEP]
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)
[GOAL]
case inl
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h'✝ : j < Nat.succ ↑x
h' : j < ↑x
⊢ ¬p j
[PROOFSTEP]
exact x.2 _ h'
[GOAL]
case inr
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
h' : ↑x < Nat.succ ↑x
⊢ ¬p ↑x
[PROOFSTEP]
exact h


[GOAL]
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
k p n : ℕ
⊢ go k p n = if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k
[PROOFSTEP]
dsimp [go, go._unary]
[GOAL]
k p n : ℕ
⊢ WellFounded.fix go._unary.proof_1
      (fun _x a =>
        if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
          a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
            (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
        else _x.fst)
      { fst := k, snd := { fst := p, snd := n } } =
    if 1 < p ∧ 0 < n ∧ n % p = 0 then
      WellFounded.fix go._unary.proof_1
        (fun _x a =>
          if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
            a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
              (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
          else _x.fst)
        { fst := k + 1, snd := { fst := p, snd := n / p } }
    else k
[PROOFSTEP]
rw [WellFounded.fix_eq]
[GOAL]
k p n : ℕ
⊢ (if h :
        1 < { fst := k, snd := { fst := p, snd := n } }.snd.fst ∧
          0 < { fst := k, snd := { fst := p, snd := n } }.snd.snd ∧
            { fst := k, snd := { fst := p, snd := n } }.snd.snd % { fst := k, snd := { fst := p, snd := n } }.snd.fst =
              0 then
      (fun y x =>
          WellFounded.fix go._unary.proof_1
            (fun _x a =>
              if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
                a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
                  (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
              else _x.fst)
            y)
        { fst := { fst := k, snd := { fst := p, snd := n } }.fst + 1,
          snd :=
            { fst := { fst := k, snd := { fst := p, snd := n } }.snd.fst,
              snd :=
                { fst := k, snd := { fst := p, snd := n } }.snd.snd /
                  { fst := k, snd := { fst := p, snd := n } }.snd.fst } }
        (_ :
          { fst := k, snd := { fst := p, snd := n } }.snd.snd / { fst := k, snd := { fst := p, snd := n } }.snd.fst <
            { fst := k, snd := { fst := p, snd := n } }.snd.snd)
    else { fst := k, snd := { fst := p, snd := n } }.fst) =
    if 1 < p ∧ 0 < n ∧ n % p = 0 then
      WellFounded.fix go._unary.proof_1
        (fun _x a =>
          if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
            a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
              (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
          else _x.fst)
        { fst := k + 1, snd := { fst := p, snd := n / p } }
    else k
[PROOFSTEP]
simp
[GOAL]
k p n : ℕ
⊢ go (k + 1) p n = go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) = go k p n + 1
[PROOFSTEP]
conv_rhs => rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
case neg
k p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
swap
[GOAL]
case neg
k p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
simp only [if_neg h]
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
have : n / p < n := by apply Nat.div_lt_self <;> aesop
[GOAL]
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
simp only [if_pos h]
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ go (k + 1 + 1) p (n / p) = go (k + 1) p (n / p) + 1
[PROOFSTEP]
apply go_succ
[GOAL]
n : ℕ
⊢ maxPowDiv 0 n = 0
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
n : ℕ
⊢ go 0 0 n = 0
[PROOFSTEP]
rw [maxPowDiv.go_eq]
[GOAL]
n : ℕ
⊢ (if 1 < 0 ∧ 0 < n ∧ n % 0 = 0 then go (0 + 1) 0 (n / 0) else 0) = 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ maxPowDiv p 0 = 0
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p : ℕ
⊢ go 0 p 0 = 0
[PROOFSTEP]
rw [maxPowDiv.go_eq]
[GOAL]
p : ℕ
⊢ (if 1 < p ∧ 0 < 0 ∧ 0 % p = 0 then go (0 + 1) p (0 / p) else 0) = 0
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p * n) = maxPowDiv p n + 1
[PROOFSTEP]
have : 0 < p := lt_trans (b := 1) (by simp) hp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ 0 < 1
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ maxPowDiv p (p * n) = maxPowDiv p n + 1
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go 0 p (p * n) = go 0 p n + 1
[PROOFSTEP]
rw [maxPowDiv.go_eq, if_pos, mul_div_right _ this]
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go (0 + 1) p n = go 0 p n + 1
[PROOFSTEP]
apply go_succ
[GOAL]
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 1 < p ∧ 0 < p * n ∧ p * n % p = 0
[PROOFSTEP]
refine ⟨hp, ?_, by simp⟩
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ p * n % p = 0
[PROOFSTEP]
simp
[GOAL]
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 0 < p * n
[PROOFSTEP]
apply Nat.mul_pos this hn
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p ^ exp * n) = maxPowDiv p n + exp
[PROOFSTEP]
match exp with
| 0 => simp
| e + 1 =>
  rw [pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
  · ac_rfl
  · apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p ^ 0 * n) = maxPowDiv p n + 0
[PROOFSTEP]
simp
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ maxPowDiv p (p ^ (e + 1) * n) = maxPowDiv p n + (e + 1)
[PROOFSTEP]
rw [pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ maxPowDiv p n + e + 1 = maxPowDiv p n + (e + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ 0 < n * p ^ e
[PROOFSTEP]
apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e
[GOAL]
p n : ℕ
⊢ p ^ maxPowDiv p n ∣ n
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p n : ℕ
⊢ p ^ go 0 p n ∣ n
[PROOFSTEP]
rw [go_eq]
[GOAL]
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
have : n / p < n := by apply Nat.div_lt_self <;> aesop
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ p ^ go (0 + 1) p (n / p) ∣ n
[PROOFSTEP]
have ⟨c, hc⟩ := pow_dvd p (n / p)
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go (0 + 1) p (n / p) ∣ n
[PROOFSTEP]
rw [go_succ, pow_succ]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n
[PROOFSTEP]
nth_rw 2 [← mod_add_div' n p]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n % p + n / p * p
[PROOFSTEP]
rw [h.right.right, zero_add]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n / p * p
[PROOFSTEP]
exact ⟨c, by nth_rw 1 [hc]; ac_rfl⟩
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ n / p * p = p ^ go 0 p (n / p) * p * c
[PROOFSTEP]
nth_rw 1 [hc]
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ maxPowDiv p (n / p) * c * p = p ^ go 0 p (n / p) * p * c
[PROOFSTEP]
ac_rfl
[GOAL]
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
rw [if_neg h]
[GOAL]
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ p ^ 0 ∣ n
[PROOFSTEP]
simp
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
have ⟨c, hc⟩ := h
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
have : 0 < c := by
  apply Nat.pos_of_ne_zero
  intro h'
  rw [h', mul_zero] at hc
  exact not_eq_zero_of_lt hn hc
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ 0 < c
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ c ≠ 0
[PROOFSTEP]
intro h'
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
h' : c = 0
⊢ False
[PROOFSTEP]
rw [h', mul_zero] at hc
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = 0
h' : c = 0
⊢ False
[PROOFSTEP]
exact not_eq_zero_of_lt hn hc
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
this : 0 < c
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
simp [hc, base_pow_mul hp this]


[GOAL]
m n k : ℕ
⊢ gcd m (n + k * m) = gcd m n
[PROOFSTEP]
simp [gcd_rec m (n + k * m), gcd_rec m n]
[GOAL]
m n k : ℕ
⊢ gcd m (n + m * k) = gcd m n
[PROOFSTEP]
simp [gcd_rec m (n + m * k), gcd_rec m n]
[GOAL]
m n k : ℕ
⊢ gcd m (k * m + n) = gcd m n
[PROOFSTEP]
simp [add_comm _ n]
[GOAL]
m n k : ℕ
⊢ gcd m (m * k + n) = gcd m n
[PROOFSTEP]
simp [add_comm _ n]
[GOAL]
m n k : ℕ
⊢ gcd (m + k * n) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (m + n * k) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_mul_left_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (k * n + m) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_mul_right_add_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (n * k + m) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_mul_left_add_right, gcd_comm]
[GOAL]
m n : ℕ
⊢ gcd m (n + m) = gcd m (n + 1 * m)
[PROOFSTEP]
rw [one_mul]
[GOAL]
m n : ℕ
⊢ gcd (m + n) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_self_right, gcd_comm]
[GOAL]
m n : ℕ
⊢ gcd (m + n) m = gcd n m
[PROOFSTEP]
rw [add_comm, gcd_add_self_left]
[GOAL]
m n : ℕ
⊢ gcd m (m + n) = gcd m n
[PROOFSTEP]
rw [add_comm, gcd_add_self_right]
[GOAL]
m n : ℕ
⊢ 0 < m → 0 < n → 0 < lcm m n
[PROOFSTEP]
simp_rw [pos_iff_ne_zero]
[GOAL]
m n : ℕ
⊢ m ≠ 0 → n ≠ 0 → lcm m n ≠ 0
[PROOFSTEP]
exact lcm_ne_zero
[GOAL]
m n : ℕ
h : coprime m n
⊢ lcm m n = m * n
[PROOFSTEP]
rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
[GOAL]
m n : ℕ
⊢ coprime m (n + m) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_self_right]
[GOAL]
m n : ℕ
⊢ coprime m (m + n) ↔ coprime m n
[PROOFSTEP]
rw [add_comm, coprime_add_self_right]
[GOAL]
m n : ℕ
⊢ coprime (m + n) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_self_left]
[GOAL]
m n : ℕ
⊢ coprime (m + n) m ↔ coprime n m
[PROOFSTEP]
rw [coprime, coprime, gcd_self_add_left]
[GOAL]
m n k : ℕ
⊢ coprime m (n + k * m) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_right_right]
[GOAL]
m n k : ℕ
⊢ coprime m (n + m * k) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_left_right]
[GOAL]
m n k : ℕ
⊢ coprime m (k * m + n) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_right_add_right]
[GOAL]
m n k : ℕ
⊢ coprime m (m * k + n) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_left_add_right]
[GOAL]
m n k : ℕ
⊢ coprime (m + k * n) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_right_left]
[GOAL]
m n k : ℕ
⊢ coprime (m + n * k) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_left_left]
[GOAL]
m n k : ℕ
⊢ coprime (k * n + m) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_right_add_left]
[GOAL]
m n k : ℕ
⊢ coprime (n * k + m) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_left_add_left]
[GOAL]
n : ℕ
hn : 0 < n
a b : ℕ
⊢ coprime (a ^ n) b ↔ coprime a b
[PROOFSTEP]
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne'
[GOAL]
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ succ n) b ↔ coprime a b
[PROOFSTEP]
rw [pow_succ, Nat.coprime_mul_iff_left]
[GOAL]
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ n) b ∧ coprime a b ↔ coprime a b
[PROOFSTEP]
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩
[GOAL]
n : ℕ
hn : 0 < n
a b : ℕ
⊢ coprime a (b ^ n) ↔ coprime a b
[PROOFSTEP]
rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
[GOAL]
⊢ ¬coprime 0 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ coprime 1 n ↔ True
[PROOFSTEP]
simp [coprime]
[GOAL]
n : ℕ
⊢ coprime n 1 ↔ True
[PROOFSTEP]
simp [coprime]
[GOAL]
a b c : ℕ
hac : coprime a c
b_dvd_c : b ∣ c
⊢ gcd (a * b) c = b
[PROOFSTEP]
rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
[GOAL]
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd (a * b) (d * b) = b
[PROOFSTEP]
rw [gcd_mul_right]
[GOAL]
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d * b = b
[PROOFSTEP]
convert one_mul b
[GOAL]
case h.e'_2.h.e'_5
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d = 1
[PROOFSTEP]
exact coprime.coprime_mul_right_right hac
[GOAL]
m n k : ℕ
H : k ∣ m * n
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
cases h0 : gcd k m
[GOAL]
case zero
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
case succ m n k : ℕ H : k ∣ m * n n✝ : ℕ h0 : gcd k m = succ n✝ ⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case zero =>
  obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
  obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
  exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case zero =>
  obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
  obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
  exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
[GOAL]
m n : ℕ
H : 0 ∣ m * n
h0 : gcd 0 m = zero
⊢ { d // 0 = ↑d.fst * ↑d.snd }
[PROOFSTEP]
obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
[GOAL]
n : ℕ
H : 0 ∣ 0 * n
h0 : gcd 0 0 = zero
⊢ { d // 0 = ↑d.fst * ↑d.snd }
[PROOFSTEP]
exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
case succ
m n k : ℕ
H : k ∣ m * n
n✝ : ℕ
h0 : gcd k m = succ n✝
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case succ tmp =>
  have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _; clear h0 tmp
  have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
  refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
  apply Nat.dvd_of_mul_dvd_mul_left hpos
  rw [hd, ← gcd_mul_right]
  exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case succ tmp =>
  have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _; clear h0 tmp
  have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
  refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
  apply Nat.dvd_of_mul_dvd_mul_left hpos
  rw [hd, ← gcd_mul_right]
  exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
hpos : 0 < gcd k m
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
clear h0 tmp
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ k / gcd k m ∣ n
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_left hpos
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ gcd k m * (k / gcd k m) ∣ gcd k m * n
[PROOFSTEP]
rw [hd, ← gcd_mul_right]
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ k ∣ gcd (k * n) (m * n)
[PROOFSTEP]
exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
x m n : ℕ
⊢ x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
constructor
[GOAL]
case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
intro h
[GOAL]
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
obtain ⟨⟨⟨y, hy⟩, ⟨z, hz⟩⟩, rfl⟩ := prod_dvd_and_dvd_of_dvd_prod h
[GOAL]
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h :
  ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
      ↑({ val := y, property := hy }, { val := z, property := hz }).snd ∣
    m * n
⊢ ∃ y_1 z_1,
    y_1 ∣ m ∧
      z_1 ∣ n ∧
        y_1 * z_1 =
          ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
            ↑({ val := y, property := hy }, { val := z, property := hz }).snd
[PROOFSTEP]
exact ⟨y, z, hy, hz, rfl⟩
[GOAL]
case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n
[PROOFSTEP]
rintro ⟨y, z, hy, hz, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n
[PROOFSTEP]
exact mul_dvd_mul hy hz
[GOAL]
a b n : ℕ
n0 : 0 < n
⊢ a ^ n ∣ b ^ n ↔ a ∣ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => pow_dvd_pow_of_dvd h _⟩
[GOAL]
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
⊢ a ∣ b
[PROOFSTEP]
cases' Nat.eq_zero_or_pos (gcd a b) with g0 g0
[GOAL]
case inl
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b = 0
⊢ a ∣ b
[PROOFSTEP]
simp [eq_zero_of_gcd_eq_zero_right g0]
[GOAL]
case inr
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b > 0
⊢ a ∣ b
[PROOFSTEP]
rcases exists_coprime' g0 with ⟨g, a', b', g0', co, rfl, rfl⟩
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
[PROOFSTEP]
rw [mul_pow, mul_pow] at h
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
[PROOFSTEP]
replace h := Nat.dvd_of_mul_dvd_mul_right (pow_pos g0' _) h
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g
[PROOFSTEP]
have := pow_dvd_pow a' n0
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g
[PROOFSTEP]
rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g
[PROOFSTEP]
simp [eq_one_of_dvd_one this]
[GOAL]
a b k : ℕ
h_ab_coprime : coprime a b
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
[PROOFSTEP]
rw [coprime_iff_gcd_eq_one] at h_ab_coprime
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
[PROOFSTEP]
have h1 := dvd_gcd hka hkb
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ gcd a b
⊢ k = 1
[PROOFSTEP]
rw [h_ab_coprime] at h1
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ 1
⊢ k = 1
[PROOFSTEP]
exact Nat.dvd_one.mp h1
[GOAL]
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n
[PROOFSTEP]
intro h
[GOAL]
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
[PROOFSTEP]
obtain ⟨x, rfl⟩ : n ∣ a :=
  cop.symm.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
[GOAL]
case intro
m n b : ℕ
cop : coprime m n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False
[PROOFSTEP]
obtain ⟨y, rfl⟩ : m ∣ b :=
  cop.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
[PROOFSTEP]
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
[PROOFSTEP]
refine' mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) _)
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
[PROOFSTEP]
rw [← mul_assoc, ← h, add_mul, add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]


[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : P
⊢ ↑m = ↑m
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
rw [cast_succ, Nat.cast_zero, zero_add]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
⊢ ↑(m + n) = ↑m + ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ ↑(m + zero) = ↑m + ↑zero
[PROOFSTEP]
simp [add_succ, add_assoc, Nat.add_zero, Nat.cast_one, Nat.cast_zero, *]
[GOAL]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n✝ : ℕ
n_ih✝ : ↑(m + n✝) = ↑m + ↑n✝
⊢ ↑(m + succ n✝) = ↑m + ↑(succ n✝)
[PROOFSTEP]
simp [add_succ, add_assoc, Nat.add_zero, Nat.cast_one, Nat.cast_zero, *]
[GOAL]
n : ℕ
h✝ : (n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : (n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : ¬(n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : ¬(n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ Nat.binCast n = ↑n
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → Nat.binCast m = ↑m) → Nat.binCast n = ↑n
[PROOFSTEP]
intros k hk
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < k → Nat.binCast m = ↑m
⊢ Nat.binCast k = ↑k
[PROOFSTEP]
cases k with
| zero => rw [Nat.binCast, Nat.cast_zero]
| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < k → Nat.binCast m = ↑m
⊢ Nat.binCast k = ↑k
[PROOFSTEP]
cases k with
| zero => rw [Nat.binCast, Nat.cast_zero]
| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hk : ∀ (m : ℕ), m < zero → Nat.binCast m = ↑m
⊢ Nat.binCast zero = ↑zero
[PROOFSTEP]

| zero => rw [Nat.binCast, Nat.cast_zero]
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hk : ∀ (m : ℕ), m < zero → Nat.binCast m = ↑m
⊢ Nat.binCast zero = ↑zero
[PROOFSTEP]
rw [Nat.binCast, Nat.cast_zero]
[GOAL]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ Nat.binCast (succ k) = ↑(succ k)
[PROOFSTEP]

| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ Nat.binCast (succ k) = ↑(succ k)
[PROOFSTEP]
rw [Nat.binCast]
[GOAL]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
[PROOFSTEP]
by_cases h : (k + 1) % 2 = 0
[GOAL]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
[PROOFSTEP]
rw [← Nat.mod_add_div (succ k) 2]
[GOAL]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
[PROOFSTEP]
rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
[GOAL]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) = ↑(succ k % 2 + 2 * (succ k / 2))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
[PROOFSTEP]
rw [← Nat.mod_add_div (succ k) 2]
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
[PROOFSTEP]
rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
[PROOFSTEP]
have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
[PROOFSTEP]
rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k / 2 + succ k / 2 + 1)
[PROOFSTEP]
simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(bit1 n) = bit1 ↑n
[PROOFSTEP]
rw [bit1, cast_add_one, cast_bit0]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ bit0 ↑n + 1 = bit1 ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp only [Nat.binCast, Nat.cast]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
dsimp only [NatCast.natCast]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
⊢ Nat.binCast (n + 1) = Nat.binCast n + 1
[PROOFSTEP]
letI : AddMonoidWithOne R := AddMonoidWithOne.unary
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ Nat.binCast (n + 1) = Nat.binCast n + 1
[PROOFSTEP]
rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False
[PROOFSTEP]
exact h.out Nat.cast_zero
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1) = 2
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 2 + 1 = 3
[PROOFSTEP]
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1 + 1) = 3
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 + 1 = 3
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 3 + 1 = 4
[PROOFSTEP]
rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1 + 1 + 1) = 4
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 + 1 + 1 = 4
[PROOFSTEP]
decide


[GOAL]
a b x : ℕ
⊢ x ∈ (fun a b => { val := ↑(List.range' a (b + 1 - a)), nodup := (_ : List.Nodup (List.range' a (b + 1 - a))) }) a b ↔
    a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
⊢ x ∈ (fun a b => { val := ↑(List.range' a (b - a)), nodup := (_ : List.Nodup (List.range' a (b - a))) }) a b ↔
    a ≤ x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le h]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le h]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le h]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [add_tsub_cancel_of_le h]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a ↔ a ≤ x ∧ x < b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
a b x : ℕ
⊢ x ∈
      (fun a b => { val := ↑(List.range' (a + 1) (b - a)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a))) }) a
        b ↔
    a < x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]

| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 ↔ a < x ∧ x ≤ b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
a b x : ℕ
⊢ x ∈
      (fun a b =>
          { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a - 1))) })
        a b ↔
    a < x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1, ← tsub_add_eq_tsub_tsub]
[GOAL]
a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
cases le_or_lt (a + 1) b with
| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a + 1 ≤ b ∨ b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
cases le_or_lt (a + 1) b with
| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a + 1 ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
[GOAL]
case inl
a b x : ℕ
h : a + 1 ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 ↔ a < x ∧ x < b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b c : ℕ
⊢ Iio = range
[PROOFSTEP]
ext b x
[GOAL]
case h.a
a b✝ c b x : ℕ
⊢ x ∈ Iio b ↔ x ∈ range b
[PROOFSTEP]
rw [mem_Iio, mem_range]
[GOAL]
a b c : ℕ
⊢ Ico 0 = range
[PROOFSTEP]
rw [← bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]
[GOAL]
a b c : ℕ
⊢ card (uIcc a b) = Int.natAbs (↑b - ↑a) + 1
[PROOFSTEP]
refine' (card_Icc _ _).trans (Int.ofNat.inj _)
[GOAL]
a b c : ℕ
⊢ Int.ofNat (a ⊔ b + 1 - a ⊓ b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
change ((↑) : ℕ → ℤ) _ = _
[GOAL]
a b c : ℕ
⊢ ↑(a ⊔ b + 1 - a ⊓ b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
rw [sup_eq_max, inf_eq_min, Int.ofNat_sub]
[GOAL]
a b c : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
rw [add_comm, Int.ofNat_add, add_sub_assoc]
  -- porting note: `norm_cast` puts a `Int.subSubNat` in the goal
      -- norm_cast
[GOAL]
a b c : ℕ
⊢ ↑1 + (↑(max a b) - ↑(min a b)) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
change _ = ↑(Int.natAbs (b - a) + 1)
[GOAL]
a b c : ℕ
⊢ ↑1 + (↑(max a b) - ↑(min a b)) = ↑(Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
push_cast
[GOAL]
a b c : ℕ
⊢ 1 + (max ↑a ↑b - min ↑a ↑b) = |↑b - ↑a| + 1
[PROOFSTEP]
rw [max_sub_min_eq_abs, add_comm]
[GOAL]
a b c : ℕ
⊢ min a b ≤ max a b + 1
[PROOFSTEP]
exact min_le_max.trans le_self_add
[GOAL]
a b c : ℕ
⊢ card (Iic b) = b + 1
[PROOFSTEP]
rw [Iic_eq_Icc, card_Icc, bot_eq_zero, tsub_zero]
[GOAL]
a b c : ℕ
⊢ card (Iio b) = b
[PROOFSTEP]
rw [Iio_eq_Ico, card_Ico, bot_eq_zero, tsub_zero]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Icc a b) = b + 1 - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Icc]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ico a b) = b - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ico]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ioc a b) = b - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioc]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ioo a b) = b - a - 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioo]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Iic b) = b + 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iic]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Iio b) = b
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iio]
[GOAL]
a b c : ℕ
⊢ Icc (succ a) b = Ioc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
[PROOFSTEP]
rw [mem_Icc, mem_Ioc, succ_le_iff]
[GOAL]
a b c : ℕ
⊢ Ico a (succ b) = Icc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
[PROOFSTEP]
rw [mem_Ico, mem_Icc, lt_succ_iff]
[GOAL]
a b c : ℕ
⊢ Ico (succ a) b = Ioo a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
[PROOFSTEP]
rw [mem_Ico, mem_Ioo, succ_le_iff]
[GOAL]
a b✝ c b : ℕ
h : 0 < b
⊢ Icc a (b - 1) = Ico a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b✝ c b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b
[PROOFSTEP]
rw [mem_Icc, mem_Ico, lt_iff_le_pred h]
[GOAL]
a b c : ℕ
⊢ Ico (succ a) (succ b) = Ioc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) (succ b) ↔ x ∈ Ioc a b
[PROOFSTEP]
rw [mem_Ico, mem_Ioc, succ_le_iff, lt_succ_iff]
[GOAL]
a b c : ℕ
⊢ Ico a (a + 1) = {a}
[PROOFSTEP]
rw [Ico_succ_right, Icc_self]
[GOAL]
a✝ b c a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}
[PROOFSTEP]
rw [← Icc_pred_right _ h, Icc_self]
[GOAL]
a b c : ℕ
⊢ Ioc b (b + 1) = {b + 1}
[PROOFSTEP]
rw [← Nat.Icc_succ_left, Icc_self]
[GOAL]
a b c : ℕ
h : a ≤ b
⊢ Ico a (b + 1) = insert b (Ico a b)
[PROOFSTEP]
rw [Ico_succ_right, ← Ico_insert_right h]
[GOAL]
a b c : ℕ
h : a < b
⊢ insert a (Ico (succ a) b) = Ico a b
[PROOFSTEP]
rw [Ico_succ_left, ← Ioo_insert_left h]
[GOAL]
a b c : ℕ
h : c ≤ a
⊢ image (fun x => x - c) (Ico a b) = Ico (a - c) (b - c)
[PROOFSTEP]
ext x
[GOAL]
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rw [mem_image]
[GOAL]
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) ↔ x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
constructor
[GOAL]
case a.mp
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) → x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : x ∈ Ico a b
⊢ x - c ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rw [mem_Ico] at hx ⊢
[GOAL]
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c
[PROOFSTEP]
exact ⟨tsub_le_tsub_right hx.1 _, tsub_lt_tsub_right_of_le (h.trans hx.1) hx.2⟩
[GOAL]
case a.mpr
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ Ico (a - c) (b - c) → ∃ a_2, a_2 ∈ Ico a b ∧ a_2 - c = x
[PROOFSTEP]
rintro h
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x
[PROOFSTEP]
refine' ⟨x + c, _, add_tsub_cancel_right _ _⟩
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ x + c ∈ Ico a b
[PROOFSTEP]
rw [mem_Ico] at h ⊢
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ a ≤ x + c ∧ x + c < b
[PROOFSTEP]
exact ⟨tsub_le_iff_right.1 h.1, lt_tsub_iff_right.1 h.2⟩
[GOAL]
a b c : ℕ
hac : a ≤ c
⊢ image (fun x => c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)
[PROOFSTEP]
ext x
[GOAL]
case a
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ x ∈ image (fun x => c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
[PROOFSTEP]
rw [mem_image, mem_Ico]
[GOAL]
case a
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
[PROOFSTEP]
constructor
[GOAL]
case a.mp
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : x ∈ Ico a b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a
[PROOFSTEP]
rw [mem_Ico] at hx
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a
[PROOFSTEP]
refine' ⟨_, ((tsub_le_tsub_iff_left hac).2 hx.1).trans_lt ((tsub_lt_tsub_iff_right hac).2 (Nat.lt_succ_self _))⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
cases lt_or_le c b with
| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
x✝ : c < b ∨ b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
cases lt_or_le c b with
| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]

| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ 0 ≤ c - x
[PROOFSTEP]
exact zero_le _
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]

| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
rw [← succ_sub_succ c]
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ succ c - succ x
[PROOFSTEP]
exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mpr
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ c + 1 - b ≤ x ∧ x < c + 1 - a → ∃ a_2, a_2 ∈ Ico a b ∧ c - a_2 = x
[PROOFSTEP]
rintro ⟨hb, ha⟩
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha : x < c + 1 - a
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
rw [lt_tsub_iff_left, lt_succ_iff] at ha
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
have hx : x ≤ c := (Nat.le_add_left _ _).trans ha
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
refine' ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ c - x ∈ Ico a b
[PROOFSTEP]
rw [mem_Ico]
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ a ≤ c - x ∧ c - x < b
[PROOFSTEP]
exact ⟨le_tsub_of_add_le_right ha, (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
[GOAL]
a b c : ℕ
⊢ Ico (succ a) b = erase (Ico a b) a
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ erase (Ico a b) a
[PROOFSTEP]
rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm, @and_comm (a ≠ x), lt_iff_le_and_ne]
[GOAL]
a✝ b c n a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico zero (zero + a))
[PROOFSTEP]
simp only [zero_add, Nat.zero_eq, Ico_zero_eq_range]
[GOAL]
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)
[PROOFSTEP]
rintro k hk l hl (hkl : k % a = l % a)
[GOAL]
case zero
a✝ b c a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l
[PROOFSTEP]
simp only [Finset.mem_range, Finset.mem_coe] at hk hl
[GOAL]
case zero
a✝ b c a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l
[PROOFSTEP]
rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
[GOAL]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(Ico (succ n) (succ n + a))
[PROOFSTEP]
rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one, Ico_succ_right_eq_insert_Ico le_self_add]
[GOAL]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(erase (insert (n + a) (Ico n (n + a))) n)
[PROOFSTEP]
rintro k hk l hl (hkl : k % a = l % a)
[GOAL]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
⊢ k = l
[PROOFSTEP]
have ha : 0 < a := by
  by_contra ha
  simp only [not_lt, nonpos_iff_eq_zero] at ha
  simp [ha] at hk
[GOAL]
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
⊢ 0 < a
[PROOFSTEP]
by_contra ha
[GOAL]
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : ¬0 < a
⊢ False
[PROOFSTEP]
simp only [not_lt, nonpos_iff_eq_zero] at ha
[GOAL]
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : a = 0
⊢ False
[PROOFSTEP]
simp [ha] at hk
[GOAL]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : 0 < a
⊢ k = l
[PROOFSTEP]
simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
[GOAL]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
⊢ k = l
[PROOFSTEP]
rcases hk with ⟨hkn, rfl | hk⟩
[GOAL]
case succ.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
⊢ n + a = l
[PROOFSTEP]
rcases hl with ⟨hln, rfl | hl⟩
[GOAL]
case succ.intro.inr
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
⊢ k = l
[PROOFSTEP]
rcases hl with ⟨hln, rfl | hl⟩
[GOAL]
case succ.intro.inl.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a
[PROOFSTEP]
rfl
[GOAL]
case succ.intro.inl.intro.inr
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l
[PROOFSTEP]
rw [add_mod_right] at hkl
[GOAL]
case succ.intro.inl.intro.inr
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l
[PROOFSTEP]
refine' (hln <| ih hl _ hkl.symm).elim
[GOAL]
case succ.intro.inl.intro.inr
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
[GOAL]
case succ.intro.inr.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a
[PROOFSTEP]
rw [add_mod_right] at hkl
[GOAL]
case succ.intro.inr.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n + a
[PROOFSTEP]
suffices k = n by contradiction
[GOAL]
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
this : k = n
⊢ k = n + a
[PROOFSTEP]
contradiction
[GOAL]
case succ.intro.inr.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n
[PROOFSTEP]
refine' ih hk _ hkl
[GOAL]
case succ.intro.inr.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ n ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
[GOAL]
case succ.intro.inr.intro.inr
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l
[PROOFSTEP]
refine' ih _ _ hkl
[GOAL]
case succ.intro.inr.intro.inr.refine'_1
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [Finset.mem_coe, hk, hl]
[GOAL]
case succ.intro.inr.intro.inr.refine'_2
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ l ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [Finset.mem_coe, hk, hl]
[GOAL]
a✝ b c n a : ℕ
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 0
[GOAL]
case inl
a b c n : ℕ
⊢ image (fun x => x % 0) (Ico n (n + 0)) = range 0
[PROOFSTEP]
rw [range_zero, add_zero, Ico_self, image_empty]
[GOAL]
case inr
a✝ b c n a : ℕ
ha : a ≠ 0
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
[PROOFSTEP]
ext i
[GOAL]
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ range a
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_range, mem_Ico]
[GOAL]
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
[PROOFSTEP]
constructor
[GOAL]
case inr.a.mp
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case inr.a.mp.intro.intro
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
left✝ : n ≤ i ∧ i < n + a
⊢ i % a < a
[PROOFSTEP]
exact mod_lt i ha.bot_lt
[GOAL]
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
[PROOFSTEP]
intro hia
[GOAL]
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
have hn := Nat.mod_add_div n a
[GOAL]
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
obtain hi | hi := lt_or_le i (n % a)
[GOAL]
case inr.a.mpr.inl
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
refine' ⟨i + a * (n / a + 1), ⟨_, _⟩, _⟩
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
[PROOFSTEP]
rw [add_comm (n / a), mul_add, mul_one, ← add_assoc]
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)
[PROOFSTEP]
refine' hn.symm.le.trans (add_le_add_right _ _)
[GOAL]
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a
[PROOFSTEP]
simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
[GOAL]
case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
[PROOFSTEP]
refine' lt_of_lt_of_le (add_lt_add_right hi (a * (n / a + 1))) _
[GOAL]
case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a
[PROOFSTEP]
rw [mul_add, mul_one, ← add_assoc, hn]
[GOAL]
case inr.a.mpr.inl.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
[PROOFSTEP]
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
[GOAL]
case inr.a.mpr.inr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
refine' ⟨i + a * (n / a), ⟨_, _⟩, _⟩
[GOAL]
case inr.a.mpr.inr.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)
[PROOFSTEP]
exact hn.symm.le.trans (add_le_add_right hi _)
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a
[PROOFSTEP]
rw [add_comm n a]
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n
[PROOFSTEP]
refine' add_lt_add_of_lt_of_le hia (le_trans _ hn.le)
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
[PROOFSTEP]
simp only [zero_le, le_add_iff_nonneg_left]
[GOAL]
case inr.a.mpr.inr.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
[PROOFSTEP]
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
[GOAL]
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
[PROOFSTEP]
convert congr_arg Finset.val (image_Ico_mod n a)
[GOAL]
case h.e'_2
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val
[PROOFSTEP]
refine' ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| _).dedup.symm
[GOAL]
case h.e'_2
a✝ b c n a : ℕ
⊢ ∀ (x : ℕ), x ∈ (Finset.Ico n (n + a)).val → ∀ (y : ℕ), y ∈ (Finset.Ico n (n + a)).val → x % a = y % a → x = y
[PROOFSTEP]
exact mod_injOn_Ico _ _
[GOAL]
a b c n : ℕ
⊢ image (fun j => n - 1 - j) (range n) = range n
[PROOFSTEP]
cases n
[GOAL]
case zero
a b c : ℕ
⊢ image (fun j => zero - 1 - j) (range zero) = range zero
[PROOFSTEP]
rw [range_zero, image_empty]
[GOAL]
case succ
a b c n✝ : ℕ
⊢ image (fun j => succ n✝ - 1 - j) (range (succ n✝)) = range (succ n✝)
[PROOFSTEP]
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
[GOAL]
case succ
a b c n✝ : ℕ
⊢ Ico (succ n✝ - 1 + 1 - succ n✝) (succ n✝ - 1 + 1 - 0) = Ico 0 (succ n✝)
[PROOFSTEP]
simp_rw [succ_sub_succ, tsub_zero, tsub_self]
[GOAL]
a b c : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
[PROOFSTEP]
rw [Finset.range_eq_Ico, map_eq_image]
[GOAL]
a b c : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (↑(addLeftEmbedding a)) (Ico 0 b)
[PROOFSTEP]
convert (@Ico_union_Ico_eq_Ico _ _ _ _ _ (a + b) a.zero_le le_self_add).symm
[GOAL]
case h.e'_3.h.e'_4
a b c : ℕ
⊢ image (↑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
[PROOFSTEP]
exact image_add_left_Ico _ _ _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n
[PROOFSTEP]
apply Nat.decreasing_induction_of_infinite h fun hf => _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ Set.Finite {x | P x} → False
[PROOFSTEP]
intro hf
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
⊢ False
[PROOFSTEP]
obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩
[GOAL]
case intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
⊢ False
[PROOFSTEP]
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt fun hl => hl.ne <| hm seed hs hl.le) hP
[GOAL]
case intro.intro.intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False
[PROOFSTEP]
exact hl.ne (hm y hy hl.le)
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n
[PROOFSTEP]
apply Nat.cauchy_induction h _ hs ((· * ·) k) fun x hl hP => ⟨_, hm x hl hP⟩
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ ∀ (x : ℕ), succ seed ≤ x → P x → x < (fun x x_1 => x * x_1) k x
[PROOFSTEP]
intro _ hl _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x x_1 => x * x_1) k x✝
[PROOFSTEP]
convert (mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
[GOAL]
case h.e'_3
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝
[PROOFSTEP]
rw [one_mul]