internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof 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
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof 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]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
n : Nat
α✝ : Type u_1
l : List α✝
h : n ≤ l.length
⊢ (take n l).length = n
Tactic:
revert n
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
Tactic:
induction l with
| nil => intro n h; simp at h; simp [h]
| cons t l ih =>
  intro n h
  cases n with
  | zero => simp
  | succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case nil
α✝ : Type u_1
⊢ ∀ {n : Nat}, n ≤ [].length → (take n []).length = n
Tactic:
intro n h
Proof state after:
case nil
α✝ : Type u_1
n : Nat
h : n ≤ [].length
⊢ (take n []).length = n
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case nil
α✝ : Type u_1
n : Nat
h : n ≤ [].length
⊢ (take n []).length = n
Tactic:
simp at h
Proof state after:
case nil
α✝ : Type u_1
n : Nat
h : n = 0
⊢ (take n []).length = n
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case nil
α✝ : Type u_1
n : Nat
h : n = 0
⊢ (take n []).length = n
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
⊢ ∀ {n : Nat}, n ≤ (t :: l).length → (take n (t :: l)).length = n
Tactic:
intro n h
Proof state after:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n ≤ (t :: l).length
⊢ (take n (t :: l)).length = n
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n ≤ (t :: l).length
⊢ (take n (t :: l)).length = n
Tactic:
cases n with
| zero => simp
| succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case cons.zero
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
h : 0 ≤ (t :: l).length
⊢ (take 0 (t :: l)).length = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n + 1 ≤ (t :: l).length
⊢ (take (n + 1) (t :: l)).length = n + 1
Tactic:
simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n + 1 ≤ (t :: l).length
⊢ ?m.37095 ≤ l.length
Tactic:
rw [length_cons, succ_le_succ_iff] at h
Proof state after:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h✝ : n + 1 ≤ (t :: l).length
h : n ≤ l.length
⊢ ?m.37095 ≤ l.length
Theorem: Smt.Reconstruct.Prop.length_take
Proof state before:
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h✝ : n + 1 ≤ (t :: l).length
h : n ≤ l.length
⊢ ?m.37095 ≤ l.length
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof state before:
i : Nat
α✝ : Type u_1
l : List α✝
h : i < l.length
⊢ (l.eraseIdx i).length = l.length - 1
Tactic:
revert i
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof state before:
case nil
α✝ : Type u_1
⊢ ∀ {i : Nat}, i < [].length → ([].eraseIdx i).length = [].length - 1
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Prop.length_eraseIdx
Proof 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)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.take_append
Proof state before:
α : Type u_1
a b : List α
⊢ take a.length (a ++ b) = a
Tactic:
have H3:= take_append_drop a.length (a ++ b)
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ take a.length (a ++ b) = a
Theorem: Smt.Reconstruct.Prop.take_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ take a.length (a ++ b) = a
Tactic:
apply (append_inj H3 _).1
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
Theorem: Smt.Reconstruct.Prop.take_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
Tactic:
rw [length_take]
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length
Theorem: Smt.Reconstruct.Prop.take_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length
Tactic:
rw [length_append]
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length
Theorem: Smt.Reconstruct.Prop.take_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length
Tactic:
apply le_add_right
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.drop_append
Proof state before:
α : Type u_1
a b : List α
⊢ drop a.length (a ++ b) = b
Tactic:
have H3:= take_append_drop a.length (a ++ b)
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ drop a.length (a ++ b) = b
Theorem: Smt.Reconstruct.Prop.drop_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ drop a.length (a ++ b) = b
Tactic:
apply (append_inj H3 _).2
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
Theorem: Smt.Reconstruct.Prop.drop_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
Tactic:
rw [length_take]
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length
Theorem: Smt.Reconstruct.Prop.drop_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length
Tactic:
rw [length_append]
Proof state after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length
Theorem: Smt.Reconstruct.Prop.drop_append
Proof state before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length
Tactic:
apply le_add_right
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_append_left
Proof state before:
ps qs : List Prop
hps : orN ps
⊢ orN (ps ++ qs)
Tactic:
apply @orN_subList ps (ps ++ qs) 0 ps.length hps
Proof state after:
ps qs : List Prop
hps : orN ps
⊢ ps = subList' (ps ++ qs) 0 ps.length
Theorem: Smt.Reconstruct.Prop.orN_append_left
Proof state before:
ps qs : List Prop
hps : orN ps
⊢ ps = subList' (ps ++ qs) 0 ps.length
Tactic:
simp [subList', take_append]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_append_right
Proof state before:
qs ps : List Prop
hqs : orN qs
⊢ orN (ps ++ qs)
Tactic:
apply @orN_subList qs (ps ++ qs) ps.length (ps.length + qs.length) hqs
Proof state after:
qs ps : List Prop
hqs : orN qs
⊢ qs = subList' (ps ++ qs) ps.length (ps.length + qs.length)
Theorem: Smt.Reconstruct.Prop.orN_append_right
Proof state before:
qs ps : List Prop
hqs : orN qs
⊢ qs = subList' (ps ++ qs) ps.length (ps.length + qs.length)
Tactic:
simp only [←length_append, subList', take_length, drop_append]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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]
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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 *
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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 *
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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 *
Proof 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)
Theorem: Smt.Reconstruct.Prop.orN_resolution
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
ps : List Prop
q : Prop
⊢ ¬andN' ps ¬q → impliesN ps q
Tactic:
induction ps with
| nil => exact notNotElim
| cons p ps ih =>
  simp only [andN', impliesN]
  intro hnpps hp
  have hnpnps := deMorganSmall₃ hnpps
  match hnpnps with
  | .inl hnp => contradiction
  | .inr hnps => exact ih hnps
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
case nil
q : Prop
⊢ ¬andN' [] ¬q → impliesN [] q
Tactic:
exact notNotElim
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬andN' (p :: ps) ¬q → impliesN (p :: ps) q
Tactic:
simp only [andN', impliesN]
Proof state after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q
Tactic:
intro hnpps hp
Proof state after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
⊢ impliesN ps q
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
⊢ impliesN ps q
Tactic:
have hnpnps := deMorganSmall₃ hnpps
Proof state after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
⊢ impliesN ps q
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
⊢ impliesN ps q
Tactic:
match hnpnps with
| .inl hnp => contradiction
| .inr hnps => exact ih hnps
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
hnp : ¬p
⊢ impliesN ps q
Tactic:
contradiction
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.implies_of_not_and
Proof state before:
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
hnps : ¬andN' ps ¬q
⊢ impliesN ps q
Tactic:
exact ih hnps
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
⊢ x * y ≤ b * x + a * y - a * b → x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
intro h
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have h₁ : (x - a) * (y - b) ≤ 0 := by linarith
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact
  match lt_trichotomy (x - a) 0, lt_trichotomy (y - b) 0 with
  | Or.inl xaNeg,           Or.inl ybNeg           => by nlinarith
  | Or.inl xaNeg,           Or.inr (Or.inl ybZero) => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaNeg' ybZero')
  | Or.inl xaNeg,           Or.inr (Or.inr ybPos)  => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inl (And.intro xaNeg' ybPos')
  | Or.inr (Or.inl xaZero), Or.inl ybNeg           => by
    have xaZero' := ge_of_eq xaZero
    simp at xaZero'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inr (And.intro xaZero' ybNeg')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inl ybZero) => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaZero' ybZero')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inr ybPos)  => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inl (And.intro xaZero' ybPos')
  | Or.inr (Or.inr xaPos),  Or.inl ybNeg           => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inr (And.intro xaPos' ybNeg')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inl ybZero) => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybZero' := le_of_eq ybZero
    simp at ybZero'
    exact Or.inr (And.intro xaPos' ybZero')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inr ybPos)  => by nlinarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ (x - a) * (y - b) ≤ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaNeg' := le_of_lt xaNeg
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaNeg'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybZero' := ge_of_eq ybZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b