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

State before:
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
have H1 := orN_eraseIdx hj
State after:
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

State before:
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
have H2 := orN_eraseIdx hi
State after:
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

State before:
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
by_cases h : ps[i]
State after:
case pos
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
h : ps[i]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

case neg
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
h : ¬ps[i]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

State before:
case pos
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
h : ps[i]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
simp only [eq_iff_iff, true_iff, iff_true, h, hqs, hij, hps] at *
State after:
case pos
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i) ∨ True
h : True
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

State before:
case pos
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i) ∨ True
h : True
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
apply orN_append_right (by simp [*] at *; exact H1)
State after:
no goals

State before:
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i) ∨ True
h : True
⊢ orN (qs.eraseIdx j)
Tactic:
simp [*] at *
State after:
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
h : True
H1 : orN (qs.eraseIdx j)
H2 : True
⊢ orN (qs.eraseIdx j)

State before:
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
h : True
H1 : orN (qs.eraseIdx j)
H2 : True
⊢ orN (qs.eraseIdx j)
Tactic:
exact H1
State after:
no goals

State before:
case neg
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
h : ¬ps[i]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
simp only [hps, hqs, h, eq_iff_iff, false_iff, not_not, iff_true, or_false,
not_false_eq_true] at *
State after:
case neg
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i)
h : True
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)

State before:
case neg
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i)
h : True
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
Tactic:
apply orN_append_left H2
State after:
no goals