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

State before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ remove (f a) (map f l) ⊆ map f (remove a l)
Tactic:
simp[List.subset_def, List.mem_remove_iff]
State after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ ∀ a_1 ∈ l, ¬f a_1 = f a → ∃ a_4, (a_4 ∈ l ∧ ¬a_4 = a) ∧ f a_4 = f a_1

State before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ ∀ a_1 ∈ l, ¬f a_1 = f a → ∃ a_4, (a_4 ∈ l ∧ ¬a_4 = a) ∧ f a_4 = f a_1
Tactic:
intro b hb neb
State after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ∃ a_1, (a_1 ∈ l ∧ ¬a_1 = a) ∧ f a_1 = f b

State before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ∃ a_1, (a_1 ∈ l ∧ ¬a_1 = a) ∧ f a_1 = f b
Tactic:
exact ⟨b, ⟨hb, by rintro rfl; exact neb rfl⟩, rfl⟩
State after:
no goals

State before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ¬b = a
Tactic:
rintro rfl
State after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
b : α
hb : b ∈ l
neb : ¬f b = f b
⊢ False

State before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
b : α
hb : b ∈ l
neb : ¬f b = f b
⊢ False
Tactic:
exact neb rfl
State after:
no goals