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

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
⊢ l.toFinset ⊆ l'.toFinset
Tactic:
intro a
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l.toFinset → a ∈ l'.toFinset

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l.toFinset → a ∈ l'.toFinset
Tactic:
simp
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l → a ∈ l'

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l → a ∈ l'
Tactic:
intro ha
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
ha : a ∈ l
⊢ a ∈ l'

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
ha : a ∈ l
⊢ a ∈ l'
Tactic:
exact h ha
State after:
no goals