Theorem: not_MultisetRedLt_0 (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ ¬MultisetRedLt M 0
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
h : MultisetRedLt M 0
⊢ False

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
h : MultisetRedLt M 0
⊢ False
Tactic:
cases h with
| RedLt X Y a M nonsense _ =>
  have contra : a ∈ (0 : Multiset α):= by
    rw [nonsense]
    simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
  contradiction
State after:
no goals

State before:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ False
Tactic:
have contra : a ∈ (0 : Multiset α):= by
  rw [nonsense]
  simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
State after:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
contra : a ∈ 0
⊢ False

State before:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
contra : a ∈ 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ 0
Tactic:
rw [nonsense]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ X + {a}

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ X + {a}
Tactic:
simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
State after:
no goals