Theorem: Smt.Reconstruct.Prop.length_eraseIdx (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
i : Nat
α✝ : Type u_1
l : List α✝
h : i < l.length
⊢ (l.eraseIdx i).length = l.length - 1
Tactic:
revert i
State after:
α✝ : Type u_1
l : List α✝
⊢ ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1

State before:
α✝ : Type u_1
l : List α✝
⊢ ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
Tactic:
induction l with
| nil => simp
| cons t l ih =>
  intro i hi
  cases i with
  | zero => simp
  | succ i =>
    simp
    rw [length_cons, succ_lt_succ_iff] at hi
    rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
State after:
no goals

State before:
case nil
α✝ : Type u_1
⊢ ∀ {i : Nat}, i < [].length → ([].eraseIdx i).length = [].length - 1
Tactic:
simp
State after:
no goals

State before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
⊢ ∀ {i : Nat}, i < (t :: l).length → ((t :: l).eraseIdx i).length = (t :: l).length - 1
Tactic:
intro i hi
State after:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < (t :: l).length
⊢ ((t :: l).eraseIdx i).length = (t :: l).length - 1

State before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < (t :: l).length
⊢ ((t :: l).eraseIdx i).length = (t :: l).length - 1
Tactic:
cases i with
| zero => simp
| succ i =>
  simp
  rw [length_cons, succ_lt_succ_iff] at hi
  rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
State after:
no goals

State before:
case cons.zero
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
hi : 0 < (t :: l).length
⊢ ((t :: l).eraseIdx 0).length = (t :: l).length - 1
Tactic:
simp
State after:
no goals

State before:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i + 1 < (t :: l).length
⊢ ((t :: l).eraseIdx (i + 1)).length = (t :: l).length - 1
Tactic:
simp
State after:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i + 1 < (t :: l).length
⊢ (l.eraseIdx i).length + 1 = l.length

State before:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i + 1 < (t :: l).length
⊢ (l.eraseIdx i).length + 1 = l.length
Tactic:
rw [length_cons, succ_lt_succ_iff] at hi
State after:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

State before:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length
Tactic:
rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
State after:
no goals