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

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
⊢ loop p i hi = some k → p k = true
Tactic:
intro h
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h : loop p i hi = some k
⊢ p k = true

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h : loop p i hi = some k
⊢ p k = true
Tactic:
unfold loop at h
State after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
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) ⋯) =
    some k
⊢ p k = true

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
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) ⋯) =
    some k
⊢ p k = true
Tactic:
split at h
State after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true

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

State before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
next => contradiction
State after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true

State before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
next hne =>
  have hi : i < n := Nat.lt_of_le_of_ne hi hne
  simp only at h
  split at h
  next hp =>
    cases h
    exact hp
  next =>
    exact loop_some (i+1) (Nat.succ_le_of_lt hi) k h
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true
Tactic:
contradiction
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
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
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
hi : i < n
⊢ p k = true

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

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

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

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

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

State before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Tactic:
next =>
  exact loop_some (i+1) (Nat.succ_le_of_lt hi) k h
State after:
no goals

State before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
h : some ⟨i, ⋯⟩ = some k
⊢ p k = true
Tactic:
cases h
State after:
case refl
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
⊢ p ⟨i, ⋯⟩ = true

State before:
case refl
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
⊢ p ⟨i, ⋯⟩ = true
Tactic:
exact hp
State after:
no goals

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