Theorem: List.getF_rangeF (MLIR/Util/List.lean)

State before:
n i : ℕ
h : i < length (rangeF n)
⊢ i < n
Tactic:
simp at h
State after:
n i : ℕ
h : i < n
⊢ i < n

State before:
n i : ℕ
h : i < n
⊢ i < n
Tactic:
apply h
State after:
no goals

State before:
n : ℕ
⊢ ∀ (i : ℕ) (h : i < length (rangeF n)), getF (rangeF n) i h = { val := i, isLt := (_ : i < n) }
Tactic:
induction n with
| zero =>
    intro i h;
    simp;
| succ m ih =>
    intro i
    exact match i with
    | 0 => by simp [getF]
    | j+1 => by simp [rangeF, getF, ih]
State after:
no goals

State before:
case zero

⊢ ∀ (i : ℕ) (h : i < length (rangeF Nat.zero)), getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }
Tactic:
intro i h
State after:
case zero
i : ℕ
h : i < length (rangeF Nat.zero)
⊢ getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }

State before:
case zero
i : ℕ
h : i < length (rangeF Nat.zero)
⊢ getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }
Tactic:
simp
State after:
no goals

State before:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
⊢ ∀ (i : ℕ) (h : i < length (rangeF (Nat.succ m))),
    getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }
Tactic:
intro i
State after:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : i < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }

State before:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : i < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }
Tactic:
exact match i with
| 0 => by simp [getF]
| j+1 => by simp [rangeF, getF, ih]
State after:
no goals

State before:
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : 0 < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) 0 h = { val := 0, isLt := (_ : 0 < Nat.succ m) }
Tactic:
simp [getF]
State after:
no goals

State before:
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i j : ℕ
⊢ ∀ (h : j + 1 < length (rangeF (Nat.succ m))),
    getF (rangeF (Nat.succ m)) (j + 1) h = { val := j + 1, isLt := (_ : j + 1 < Nat.succ m) }
Tactic:
simp [rangeF, getF, ih]
State after:
no goals