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

State before:
j : Nat
qs : List Prop
hj : j < qs.length
⊢ (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
Tactic:
revert j
State after:
qs : List Prop
⊢ ∀ {j : Nat} (hj : j < qs.length), (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs

State before:
qs : List Prop
⊢ ∀ {j : Nat} (hj : j < qs.length), (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
Tactic:
induction qs with
| nil =>
  intro j hj
  simp at hj; exfalso
  exact not_succ_le_zero j hj
| cons t l ih =>
  intro j hj
  cases j with
  | zero =>
    simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
    rw [or_comm]
  | succ j =>
    simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
    congr
    rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
State after:
no goals

State before:
case nil

⊢ ∀ {j : Nat} (hj : j < [].length), (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
intro j hj
State after:
case nil
j : Nat
hj : j < [].length
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []

State before:
case nil
j : Nat
hj : j < [].length
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
simp at hj
State after:
case nil
j : Nat
hj : j < 0
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []

State before:
case nil
j : Nat
hj : j < 0
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
exfalso
State after:
case nil
j : Nat
hj : j < 0
⊢ False

State before:
case nil
j : Nat
hj : j < 0
⊢ False
Tactic:
exact not_succ_le_zero j hj
State after:
no goals

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
⊢ ∀ {j : Nat} (hj : j < (t :: l).length), (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
Tactic:
intro j hj
State after:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < (t :: l).length
⊢ (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < (t :: l).length
⊢ (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
Tactic:
cases j with
| zero =>
  simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
  rw [or_comm]
| succ j =>
  simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
  congr
  rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
State after:
no goals

State before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN ((t :: l).eraseIdx 0) ∨ (t :: l)[0]) = orN (t :: l)
Tactic:
simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
State after:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN l ∨ t) = (t ∨ orN l)

State before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN l ∨ t) = (t ∨ orN l)
Tactic:
rw [or_comm]
State after:
no goals

State before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN ((t :: l).eraseIdx (j + 1)) ∨ (t :: l)[j + 1]) = orN (t :: l)
Tactic:
simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
State after:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (t ∨ orN (l.eraseIdx j) ∨ l[j]) = (t ∨ orN l)

State before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (t ∨ orN (l.eraseIdx j) ∨ l[j]) = (t ∨ orN l)
Tactic:
congr
State after:
case cons.succ.e_b
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN (l.eraseIdx j) ∨ l[j]) = orN l

State before:
case cons.succ.e_b
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN (l.eraseIdx j) ∨ l[j]) = orN l
Tactic:
rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
State after:
no goals

State before:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ j < l.length
Tactic:
rw [length_cons, succ_lt_succ_iff] at hj
State after:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < l.length
⊢ j < l.length

State before:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < l.length
⊢ j < l.length
Tactic:
exact hj
State after:
no goals