Theorem: Fin.find?.loop_none (GMLInit/Data/Fin/Basic.lean)

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
⊢ i ≤ ↑k → loop p i hi = none → p k = false
Tactic:
intro hik h
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h : loop p i hi = none
⊢ p k = false

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h : loop p i hi = none
⊢ p k = false
Tactic:
unfold loop at h
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
split at h
State after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : i = n
h : none = none
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false

State before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : i = n
h : none = none
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
next heq =>
  absurd hik
  rw [heq]
  apply Nat.not_le_of_gt
  exact k.isLt
State after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false

State before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
next hne =>
  have hi : i < n := Nat.lt_of_le_of_ne hi hne
  simp only at h
  split at h
  next hp =>
    contradiction
  next hp =>
    by_cases i = k.val with
    | isTrue heq =>
      rw [Bool.eq_false_iff]
      intro hk
      apply hp
      rw [←hk]
      congr
    | isFalse hik' =>
      have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
      exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ p k = false
Tactic:
absurd hik
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬i ≤ ↑k

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬i ≤ ↑k
Tactic:
rw [heq]
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬n ≤ ↑k

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬n ≤ ↑k
Tactic:
apply Nat.not_le_of_gt
State after:
case h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ n > ↑k

State before:
case h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ n > ↑k
Tactic:
exact k.isLt
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
have hi : i < n := Nat.lt_of_le_of_ne hi hne
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
hi : i < n
⊢ p k = false

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
hi : i < n
⊢ p k = false
Tactic:
simp only at h
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = none
hi : i < n
⊢ p k = false

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = none
hi : i < n
⊢ p k = false
Tactic:
split at h
State after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false

State before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
next hp =>
  contradiction
State after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false

State before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
next hp =>
  by_cases i = k.val with
  | isTrue heq =>
    rw [Bool.eq_false_iff]
    intro hk
    apply hp
    rw [←hk]
    congr
  | isFalse hik' =>
    have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
    exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false
Tactic:
contradiction
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
by_cases i = k.val with
| isTrue heq =>
  rw [Bool.eq_false_iff]
  intro hk
  apply hp
  rw [←hk]
  congr
| isFalse hik' =>
  have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
  exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k = false
Tactic:
rw [Bool.eq_false_iff]
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k ≠ true

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k ≠ true
Tactic:
intro hk
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ False

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ False
Tactic:
apply hp
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = true

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = true
Tactic:
rw [←hk]
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = p k

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = p k
Tactic:
congr
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
⊢ p k = false
Tactic:
have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik✝ : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
hik : i < ↑k
⊢ p k = false

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik✝ : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
hik : i < ↑k
⊢ p k = false
Tactic:
exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
State after:
no goals