internlm/Lean-Github huggingface dataset:
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
hle : i < Nat.succ n
⊢ i < n
Tactic:
exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ (i ∈ if true = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
simp
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i = n ∨ i ∈ bitIndices.aux a n ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i = n ∨ i ∈ bitIndices.aux a n ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
. intro h
  cases h
  case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
  case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
. intro h
  cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
  case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
  case inr heq => cases heq; exact Or.inl rfl
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
intro h
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i = n ∨ i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i = n ∨ i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
cases h
Proof state after:
case mp.inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h✝ : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true

case mp.inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h✝ : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
cases h
Proof state after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
⊢ i < Nat.succ i ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
⊢ i < Nat.succ i ∧ UInt.getBit a i = true
Tactic:
exact ⟨i.lt_succ_self, hbit⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
intro h
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
⊢ i = n ∨ i ∈ bitIndices.aux a n
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
Proof state after:
case mpr.inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
h✝ : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n

case mpr.inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
h✝ : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
hlt : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
heq : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
case inr heq => cases heq; exact Or.inl rfl
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
hlt : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
heq : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
cases heq
Proof state after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
h : i < Nat.succ i ∧ UInt.getBit a i = true
⊢ i = i ∨ i ∈ bitIndices.aux a i
Theorem: UInt.Mem_bitIndices
Proof state before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
h : i < Nat.succ i ∧ UInt.getBit a i = true
⊢ i = i ∨ i ∈ bitIndices.aux a i
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: Subarray.castIndex_lt_stop
Proof state before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ ↑(castIndex x i) < x.stop
Tactic:
show x.start + i.1 < x.stop
Proof state after:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.start + ↑i < x.stop
Theorem: Subarray.castIndex_lt_stop
Proof state before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.start + ↑i < x.stop
Tactic:
suffices x.stop = x.start + x.size by
  rewrite [this]; exact Nat.add_lt_add_left i.2 x.start
Proof state after:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.stop = x.start + size x
Theorem: Subarray.castIndex_lt_stop
Proof state before:
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.stop = x.start + size x
Tactic:
exact (Nat.add_sub_cancel' x.h₁).symm
Proof state after:
no goals
Theorem: Subarray.castIndex_lt_stop
Proof state before:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.stop
Tactic:
rewrite [this]
Proof state after:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.start + size x
Theorem: Subarray.castIndex_lt_stop
Proof state before:
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.start + size x
Tactic:
exact Nat.add_lt_add_left i.2 x.start
Proof state after:
no goals
Theorem: Subarray.as_swap
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j).as = Array.swap x.as (castIndex x i) (castIndex x j)
Tactic:
rfl
Proof state after:
no goals
Theorem: Subarray.size_as_swap
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.size (swap x i j).as = Array.size x.as
Tactic:
rw [as_swap, Array.size_swap]
Proof state after:
no goals
Theorem: Subarray.getElem_swap
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (swap x i j)[k] = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
dsimp [swap, getElem]
Proof state after:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ get
      { as := Array.swap x.as (castIndex x i) (castIndex x j), start := x.start, stop := x.stop,
        h₁ := (_ : x.start ≤ x.stop),
        h₂ := (_ : x.stop ≤ Array.size (Array.swap x.as (castIndex x i) (castIndex x j))) }
      { val := k, isLt := hk } =
    if ↑j = k then get x { val := ↑i, isLt := (_ : ↑i < size x) }
    else if ↑i = k then get x { val := ↑j, isLt := (_ : ↑j < size x) } else get x { val := k, isLt := hk }
Theorem: Subarray.getElem_swap
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ get
      { as := Array.swap x.as (castIndex x i) (castIndex x j), start := x.start, stop := x.stop,
        h₁ := (_ : x.start ≤ x.stop),
        h₂ := (_ : x.stop ≤ Array.size (Array.swap x.as (castIndex x i) (castIndex x j))) }
      { val := k, isLt := hk } =
    if ↑j = k then get x { val := ↑i, isLt := (_ : ↑i < size x) }
    else if ↑i = k then get x { val := ↑j, isLt := (_ : ↑j < size x) } else get x { val := k, isLt := hk }
Tactic:
dsimp [get]
Proof state after:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (Array.swap x.as (castIndex x i) (castIndex x j))[x.start + k] =
    if ↑j = k then x.as[x.start + ↑i] else if ↑i = k then x.as[x.start + ↑j] else x.as[x.start + k]
Theorem: Subarray.getElem_swap
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (Array.swap x.as (castIndex x i) (castIndex x j))[x.start + k] =
    if ↑j = k then x.as[x.start + ↑i] else if ↑i = k then x.as[x.start + ↑j] else x.as[x.start + k]
Tactic:
simp only [Array.getElem_swap, castIndex, Nat.add_left_cancel_iff]
Proof state after:
no goals
Theorem: Subarray.getElem_swap_left
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑i] = x[↑j]
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
α : Type u
x : Subarray α
j : Fin (size x)
i : Nat
hi : i < size x
⊢ (swap x { val := i, isLt := hi } j)[↑{ val := i, isLt := hi }] = x[↑j]
Theorem: Subarray.getElem_swap_left
Proof state before:
case mk
α : Type u
x : Subarray α
j : Fin (size x)
i : Nat
hi : i < size x
⊢ (swap x { val := i, isLt := hi } j)[↑{ val := i, isLt := hi }] = x[↑j]
Tactic:
rcases j with ⟨j,hj⟩
Proof state after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (swap x { val := i, isLt := hi } { val := j, isLt := hj })[↑{ val := i, isLt := hi }] = x[↑{ val := j, isLt := hj }]
Theorem: Subarray.getElem_swap_left
Proof state before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (swap x { val := i, isLt := hi } { val := j, isLt := hj })[↑{ val := i, isLt := hi }] = x[↑{ val := j, isLt := hj }]
Tactic:
rewrite [getElem_swap]
Proof state after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if ↑{ val := j, isLt := hj } = ↑{ val := i, isLt := hi } then x[↑{ val := i, isLt := hi }]
    else
      if ↑{ val := i, isLt := hi } = ↑{ val := i, isLt := hi } then x[↑{ val := j, isLt := hj }]
      else x[↑{ val := i, isLt := hi }]) =
    x[↑{ val := j, isLt := hj }]
Theorem: Subarray.getElem_swap_left
Proof state before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if ↑{ val := j, isLt := hj } = ↑{ val := i, isLt := hi } then x[↑{ val := i, isLt := hi }]
    else
      if ↑{ val := i, isLt := hi } = ↑{ val := i, isLt := hi } then x[↑{ val := j, isLt := hj }]
      else x[↑{ val := i, isLt := hi }]) =
    x[↑{ val := j, isLt := hj }]
Tactic:
dsimp at *
Proof state after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Theorem: Subarray.getElem_swap_left
Proof state before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
if hji : j = i then
  cases hji; simp only [ite_true]
else
  rw [if_neg hji, if_pos rfl]
Proof state after:
no goals
Theorem: Subarray.getElem_swap_left
Proof state before:
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
hji : j = i
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
cases hji
Proof state after:
case refl
α : Type u
x : Subarray α
i : Nat
hi hj : i < size x
⊢ (if i = i then x[i] else if i = i then x[i] else x[i]) = x[i]
Theorem: Subarray.getElem_swap_left
Proof state before:
case refl
α : Type u
x : Subarray α
i : Nat
hi hj : i < size x
⊢ (if i = i then x[i] else if i = i then x[i] else x[i]) = x[i]
Tactic:
simp only [ite_true]
Proof state after:
no goals
Theorem: Subarray.getElem_swap_left
Proof state before:
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
hji : ¬j = i
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
rw [if_neg hji, if_pos rfl]
Proof state after:
no goals
Theorem: Subarray.getElem_swap_right
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑j] = x[↑i]
Tactic:
rewrite [getElem_swap]
Proof state after:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]) = x[↑i]
Theorem: Subarray.getElem_swap_right
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]) = x[↑i]
Tactic:
rw [if_pos rfl]
Proof state after:
no goals
Theorem: Subarray.getElem_swap_ne
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (swap x i j)[k] = x[k]
Tactic:
rw [getElem_swap, if_neg hjk, if_neg hik]
Proof state after:
no goals
Theorem: Subarray.swap_comm
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ swap x i j = swap x j i
Tactic:
simp [swap]
Proof state after:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.swap x.as (castIndex x i) (castIndex x j) = Array.swap x.as (castIndex x j) (castIndex x i)
Theorem: Subarray.swap_comm
Proof state before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.swap x.as (castIndex x i) (castIndex x j) = Array.swap x.as (castIndex x j) (castIndex x i)
Tactic:
exact x.as.swap_comm _ _
Proof state after:
no goals
Theorem: Subarray.size_shrinkOne'
Proof state before:
α : Type u
x : Subarray α
h : x.start < x.stop
⊢ x.stop - 1 - x.start = x.stop - x.start - 1
Tactic:
simp only [Nat.sub_sub, Nat.add_comm 1 x.start]
Proof state after:
no goals
Theorem: Subarray.getElem_shrinkOne'
Proof state before:
α : Type u
x : Subarray α
h : x.start < x.stop
i : Nat
hi : i < size (shrinkOne' x h)
⊢ (shrinkOne' x h)[i] = x[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.get_cons_zero
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x)[0] = a
Tactic:
show (cons a x).val[0]'((cons a x).size_eq.symm ▸ hi) = a
Proof state after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a
Theorem: SizedArray.get_cons_zero
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a
Tactic:
simp only [Array.getElem_eq_data_get]
Proof state after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ List.get (cons a x).val.data { val := 0, isLt := (_ : 0 < Array.size (cons a x).val) } = a
Theorem: SizedArray.get_cons_zero
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ List.get (cons a x).val.data { val := 0, isLt := (_ : 0 < Array.size (cons a x).val) } = a
Tactic:
dsimp [cons]
Proof state after:
no goals
Theorem: SizedArray.get_cons_succ
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ (cons a x)[i + 1] = x[i]
Tactic:
show (cons a x).val[i+1]'((cons a x).size_eq.symm ▸ hi₁) = x.val[i]'(x.size_eq.symm ▸ hi₂)
Proof state after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ (cons a x).val[i + 1] = x.val[i]
Theorem: SizedArray.get_cons_succ
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ (cons a x).val[i + 1] = x.val[i]
Tactic:
simp only [Array.getElem_eq_data_get]
Proof state after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ List.get (cons a x).val.data { val := i + 1, isLt := (_ : i + 1 < Array.size (cons a x).val) } =
    List.get x.val.data { val := i, isLt := (_ : i < Array.size x.val) }
Theorem: SizedArray.get_cons_succ
Proof state before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ List.get (cons a x).val.data { val := i + 1, isLt := (_ : i + 1 < Array.size (cons a x).val) } =
    List.get x.val.data { val := i, isLt := (_ : i < Array.size x.val) }
Tactic:
dsimp [cons]
Proof state after:
no goals
Theorem: SizedArray.back_eq_back'_val
Proof state before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ back x = Array.back' x.val (_ : Array.size x.val > 0)
Tactic:
dsimp [back, Array.back']
Proof state after:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[Array.size x.val - 1]
Theorem: SizedArray.back_eq_back'_val
Proof state before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[Array.size x.val - 1]
Tactic:
simp only [x.size_eq]
Proof state after:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[n + 1 - 1]
Theorem: SizedArray.back_eq_back'_val
Proof state before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[n + 1 - 1]
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.push_cons_eq_cons_push
Proof state before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ (push (cons a₁ x) a₂).val.data = (cons a₁ (push x a₂)).val.data
Tactic:
dsimp [push,cons, Array.push]
Proof state after:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ List.concat (a₁ :: x.val.data) a₂ = a₁ :: List.concat x.val.data a₂
Theorem: SizedArray.push_cons_eq_cons_push
Proof state before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ List.concat (a₁ :: x.val.data) a₂ = a₁ :: List.concat x.val.data a₂
Tactic:
simp only [List.concat_eq_append]
Proof state after:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ a₁ :: x.val.data ++ [a₂] = a₁ :: (x.val.data ++ [a₂])
Theorem: SizedArray.push_cons_eq_cons_push
Proof state before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ a₁ :: x.val.data ++ [a₂] = a₁ :: (x.val.data ++ [a₂])
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.mem_iff_get
Proof state before:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ a ∈ x ↔ ∃ i, x[↑i] = a
Tactic:
rewrite [mem_iff_mem_val, Array.mem_iff_get]
Proof state after:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) ↔ ∃ i, x[↑i] = a
Theorem: SizedArray.mem_iff_get
Proof state before:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) ↔ ∃ i, x[↑i] = a
Tactic:
constructor
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a

case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Theorem: SizedArray.mem_iff_get
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a

case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
. exact fun ⟨i,hi,hxi⟩ => ⟨⟨i, x.size_eq.symm ▸ hi⟩, hxi⟩
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a