Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty (Runtime/Utilities/Extensions.lean)

State before:
α : Type u_1
as : Array α
⊢ Option.isSome as[0]? = true ↔ ¬isEmpty as = true
Tactic:
simp [Array.isEmpty, Option.isSome_iff_exists, getElem?]
State after:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) ↔ ¬size as = 0

State before:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) ↔ ¬size as = 0
Tactic:
constructor
State after:
case mp
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0

case mpr
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a

State before:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0
Tactic:
case mp =>
  intro ⟨_, h⟩
  split at h
  case inl hs => exact Nat.not_eq_zero_of_lt hs
  case inr => contradiction
State after:
no goals

State before:
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
case mpr =>
  intro h
  split
  case inl => exists as[0]
  case inr hs => exact absurd (Nat.zero_lt_of_ne_zero h) hs
State after:
no goals

State before:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0
Tactic:
intro ⟨_, h⟩
State after:
α : Type u_1
as : Array α
w✝ : α
h : (if h : 0 < size as then some as[0] else none) = some w✝
⊢ ¬size as = 0

State before:
α : Type u_1
as : Array α
w✝ : α
h : (if h : 0 < size as then some as[0] else none) = some w✝
⊢ ¬size as = 0
Tactic:
split at h
State after:
case inl
α : Type u_1
as : Array α
w✝ : α
h✝ : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0

case inr
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0

State before:
α : Type u_1
as : Array α
w✝ : α
hs : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0
Tactic:
case inl hs => exact Nat.not_eq_zero_of_lt hs
State after:
no goals

State before:
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0
Tactic:
case inr => contradiction
State after:
no goals

State before:
α : Type u_1
as : Array α
w✝ : α
hs : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0
Tactic:
exact Nat.not_eq_zero_of_lt hs
State after:
no goals

State before:
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
intro h
State after:
α : Type u_1
as : Array α
h : ¬size as = 0
⊢ ∃ a, (if h : 0 < size as then some as[0] else none) = some a

State before:
α : Type u_1
as : Array α
h : ¬size as = 0
⊢ ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
split
State after:
case inl
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a

case inr
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : ¬0 < size as
⊢ ∃ a, False

State before:
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a
Tactic:
case inl => exists as[0]
State after:
no goals

State before:
α : Type u_1
as : Array α
h : ¬size as = 0
hs : ¬0 < size as
⊢ ∃ a, False
Tactic:
case inr hs => exact absurd (Nat.zero_lt_of_ne_zero h) hs
State after:
no goals

State before:
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a
Tactic:
exists as[0]
State after:
no goals

State before:
α : Type u_1
as : Array α
h : ¬size as = 0
hs : ¬0 < size as
⊢ ∃ a, False
Tactic:
exact absurd (Nat.zero_lt_of_ne_zero h) hs
State after:
no goals