Theorem: List.remove_cons_subset_cons_remove (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
⊢ remove b (a :: l) ⊆ a :: remove b l
Tactic:
intro x
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x ∈ remove b (a :: l) → x ∈ a :: remove b l

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x ∈ remove b (a :: l) → x ∈ a :: remove b l
Tactic:
simp[List.mem_remove_iff]
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x = a ∨ x ∈ l → ¬x = b → x = a ∨ x ∈ l ∧ ¬x = b

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x = a ∨ x ∈ l → ¬x = b → x = a ∨ x ∈ l ∧ ¬x = b
Tactic:
rintro (rfl | hx) nex <;> simp[*]
State after:
no goals