Theorem: List.nodup_range' (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
start len step : Nat
hstep : step > 0
⊢ Nodup (range' start len step)
Tactic:
induction len generalizing start with
| zero => exact .nil
| succ len IH =>
  refine Pairwise.cons ?_ (IH _)
  intro n hn; let ⟨k,hk⟩ := mem_range'.mp hn
  suffices start < n from Nat.ne_of_lt this
  calc start
    _ < start + step := Nat.lt_add_of_pos_right hstep
    _ ≤ start + step + step * k := Nat.le_add_right ..
    _ = n := hk.2.symm
State after:
no goals

State before:
case zero
α : Type u
β : Type v
step : Nat
hstep : step > 0
start : Nat
⊢ Nodup (range' start Nat.zero step)
Tactic:
exact .nil
State after:
no goals

State before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ Nodup (range' start (Nat.succ len) step)
Tactic:
refine Pairwise.cons ?_ (IH _)
State after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ ∀ (a' : Nat), a' ∈ range' (start + step) len step → start ≠ a'

State before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ ∀ (a' : Nat), a' ∈ range' (start + step) len step → start ≠ a'
Tactic:
intro n hn
State after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
⊢ start ≠ n

State before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
⊢ start ≠ n
Tactic:
let ⟨k,hk⟩ := mem_range'.mp hn
State after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start ≠ n

State before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start ≠ n
Tactic:
suffices start < n from Nat.ne_of_lt this
State after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start < n

State before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start < n
Tactic:
calc start
  _ < start + step := Nat.lt_add_of_pos_right hstep
  _ ≤ start + step + step * k := Nat.le_add_right ..
  _ = n := hk.2.symm
State after:
no goals