Theorem: List.erase_diff_len_lt_diff_len (FOL/Parsing/DFT.lean)

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.erase x).diff l2).length < (l1.diff l2).length
Tactic:
simp only [← List.diff_erase]
State after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
have s1 : x ∈ l1.diff l2 := List.mem_diff_of_mem h1 h2
State after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
have s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred := List.length_erase_of_mem s1
State after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
simp only [s2]
State after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ (l1.diff l2).length.pred < (l1.diff l2).length

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Tactic:
have s3 : 0 < (l1.diff l2).length := List.length_pos_of_mem s1
State after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
s3 : 0 < (l1.diff l2).length
⊢ (l1.diff l2).length.pred < (l1.diff l2).length

State before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
s3 : 0 < (l1.diff l2).length
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Tactic:
exact Nat.pred_lt' s3
State after:
no goals