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

State before:
ps qs : List Prop
i j : Nat
hps : orN ps
hpq : ps = subList' qs i j
⊢ orN qs
Tactic:
revert i j ps
State after:
qs : List Prop
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' qs i j → orN qs

State before:
qs : List Prop
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' qs i j → orN qs
Tactic:
induction qs with
| nil =>
  intro ps i j hp hps
  simp [subList', *] at *; assumption
| cons t l ih =>
  simp only [subList'] at *
  intro ps i j hp hps
  rw [orN_cons]
  cases j with
  | zero =>
    simp [*, orN] at *
  | succ j =>
    simp only [take_cons_succ] at hps
    cases i with
    | zero =>
      simp only [hps, orN_cons, drop_zero] at hp
      exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
    | succ i =>
      apply Or.inr
      apply @ih ps i j hp
      simp [hps]
State after:
no goals

State before:
case nil

⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' [] i j → orN []
Tactic:
intro ps i j hp hps
State after:
case nil
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = subList' [] i j
⊢ orN []

State before:
case nil
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = subList' [] i j
⊢ orN []
Tactic:
simp [subList', *] at *
State after:
case nil
ps : List Prop
i j : Nat
hp : orN []
hps : ps = []
⊢ orN []

State before:
case nil
ps : List Prop
i j : Nat
hp : orN []
hps : ps = []
⊢ orN []
Tactic:
assumption
State after:
no goals

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' l i j → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' (t :: l) i j → orN (t :: l)
Tactic:
simp only [subList'] at *
State after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j (t :: l)) → orN (t :: l)

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j (t :: l)) → orN (t :: l)
Tactic:
intro ps i j hp hps
State after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ orN (t :: l)

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ orN (t :: l)
Tactic:
rw [orN_cons]
State after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ t ∨ orN l

State before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ t ∨ orN l
Tactic:
cases j with
| zero =>
  simp [*, orN] at *
| succ j =>
  simp only [take_cons_succ] at hps
  cases i with
  | zero =>
    simp only [hps, orN_cons, drop_zero] at hp
    exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
  | succ i =>
    apply Or.inr
    apply @ih ps i j hp
    simp [hps]
State after:
no goals

State before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
hps : ps = drop i (take 0 (t :: l))
⊢ t ∨ orN l
Tactic:
simp [*, orN] at *
State after:
no goals

State before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (take (j + 1) (t :: l))
⊢ t ∨ orN l
Tactic:
simp only [take_cons_succ] at hps
State after:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (t :: take j l)
⊢ t ∨ orN l

State before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (t :: take j l)
⊢ t ∨ orN l
Tactic:
cases i with
| zero =>
  simp only [hps, orN_cons, drop_zero] at hp
  exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
| succ i =>
  apply Or.inr
  apply @ih ps i j hp
  simp [hps]
State after:
no goals

State before:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j : Nat
hps : ps = drop 0 (t :: take j l)
⊢ t ∨ orN l
Tactic:
simp only [hps, orN_cons, drop_zero] at hp
State after:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp : t ∨ orN (take j l)
⊢ t ∨ orN l

State before:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp : t ∨ orN (take j l)
⊢ t ∨ orN l
Tactic:
exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
State after:
no goals

State before:
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp✝ : t ∨ orN (take j l)
hp : orN (take j l)
⊢ orN (drop 0 (take j l))
Tactic:
simp [hp]
State after:
no goals

State before:
case cons.succ.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j i : Nat
hps : ps = drop (i + 1) (t :: take j l)
⊢ t ∨ orN l
Tactic:
apply Or.inr
State after:
case cons.succ.succ.h
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j i : Nat
hps : ps = drop (i + 1) (t :: take j l)
⊢ orN l

State before:
case cons.succ.succ.h
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j i : Nat
hps : ps = drop (i + 1) (t :: take j l)
⊢ orN l
Tactic:
apply @ih ps i j hp
State after:
case cons.succ.succ.h
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j i : Nat
hps : ps = drop (i + 1) (t :: take j l)
⊢ ps = drop i (take j l)

State before:
case cons.succ.succ.h
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j i : Nat
hps : ps = drop (i + 1) (t :: take j l)
⊢ ps = drop i (take j l)
Tactic:
simp [hps]
State after:
no goals