Theorem: randNat_range (Fifteen/Data/Permutation/Random.lean)

State before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤ (randNat g lo hi).fst ∧ (randNat g lo hi).fst ≤ hi
Tactic:
dsimp [randNat]
State after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ∧
    (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ≤
      hi

State before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ∧
    (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ≤
      hi
Tactic:
simp only [if_neg (Nat.not_lt_of_le h)]
State after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ∧
    lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ≤
      hi

State before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ∧
    lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ≤
      hi
Tactic:
generalize (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1) ((hi - lo + 1) * 1000) (0, g)).fst = x
State after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1) ∧ lo + x % (hi - lo + 1) ≤ hi

State before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1) ∧ lo + x % (hi - lo + 1) ≤ hi
Tactic:
apply And.intro
State after:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)

case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi

State before:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)

case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
. show lo ≤ _
  exact Nat.le_add_right lo _
State after:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi

State before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
. show _ ≤ hi
  conv =>
    rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
  refine Nat.add_le_add_left ?_ lo
  apply Nat.le_of_lt_succ
  exact x.mod_lt (hi - lo).zero_lt_succ
State after:
no goals

State before:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)
Tactic:
exact Nat.le_add_right lo _
State after:
no goals

State before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
conv =>
  rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
State after:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ lo + (hi - lo)

State before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ lo + (hi - lo)
Tactic:
refine Nat.add_le_add_left ?_ lo
State after:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ x % (hi - lo + 1) ≤ hi - lo

State before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ x % (hi - lo + 1) ≤ hi - lo
Tactic:
apply Nat.le_of_lt_succ
State after:
case right.a
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ x % (hi - lo + 1) < Nat.succ (hi - lo)

State before:
case right.a
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ x % (hi - lo + 1) < Nat.succ (hi - lo)
Tactic:
exact x.mod_lt (hi - lo).zero_lt_succ
State after:
no goals