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

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ remove a l ↔ b ∈ l ∧ b ≠ a
Tactic:
simp [List.remove, List.of_mem_filter]
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l ↔ b ∈ l ∧ ¬b = a

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l ↔ b ∈ l ∧ ¬b = a
Tactic:
constructor
State after:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a

case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l

State before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a

case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
. intro h;
  exact ⟨mem_of_mem_filter h, by simpa using of_mem_filter h⟩;
State after:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l

State before:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
. rintro ⟨h₁, h₂⟩;
  exact mem_filter_of_mem h₁ (by simpa using h₂);
State after:
no goals

State before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ filter (fun x => !decide (x = a)) l → b ∈ l ∧ ¬b = a
Tactic:
intro h
State after:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ b ∈ l ∧ ¬b = a

State before:
case mp
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ b ∈ l ∧ ¬b = a
Tactic:
exact ⟨mem_of_mem_filter h, by simpa using of_mem_filter h⟩
State after:
no goals

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h : b ∈ filter (fun x => !decide (x = a)) l
⊢ ¬b = a
Tactic:
simpa using of_mem_filter h
State after:
no goals

State before:
case mpr
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
⊢ b ∈ l ∧ ¬b = a → b ∈ filter (fun x => !decide (x = a)) l
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case mpr.intro
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ b ∈ filter (fun x => !decide (x = a)) l

State before:
case mpr.intro
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ b ∈ filter (fun x => !decide (x = a)) l
Tactic:
exact mem_filter_of_mem h₁ (by simpa using h₂)
State after:
no goals

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ (!decide (b = a)) = true
Tactic:
simpa using h₂
State after:
no goals