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

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ remove a l
⊢ b ∈ l
Tactic:
rw [mem_remove_iff] at h
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l ∧ b ≠ a
⊢ b ∈ l

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.180995 → Type ?u.180997
α : Type u_1
β : Type ?u.181003
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l ∧ b ≠ a
⊢ b ∈ l
Tactic:
exact h.1
State after:
no goals