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

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ remove a l₁ ⊆ remove a l₂
Tactic:
simp[subset_def, mem_remove_iff]
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ ∀ {a_1 : α}, a_1 ∈ l₁ → ¬a_1 = a → a_1 ∈ l₂ ∧ ¬a_1 = a

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ ∀ {a_1 : α}, a_1 ∈ l₁ → ¬a_1 = a → a_1 ∈ l₂ ∧ ¬a_1 = a
Tactic:
intros
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂ ∧ ¬a✝² = a

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂ ∧ ¬a✝² = a
Tactic:
simp[*]
State after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂
Tactic:
exact h (by assumption)
State after:
no goals

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₁
Tactic:
assumption
State after:
no goals