Theorem: List.multimop_cons (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
hl : p ∉ l
⊢ List.multimop i n (p :: l) ~ (mop i)^[n] p :: List.multimop i n l
Tactic:
simp [List.multimop]
State after:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
hl : p ∉ l
⊢ (insert ((mop i)^[n] p) (Finset.image (mop i)^[n] l.toFinset)).toList ~
    (mop i)^[n] p :: (Finset.multimop i n l.toFinset).toList

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
hl : p ∉ l
⊢ (insert ((mop i)^[n] p) (Finset.image (mop i)^[n] l.toFinset)).toList ~
    (mop i)^[n] p :: (Finset.multimop i n l.toFinset).toList
Tactic:
apply Finset.toList_insert
State after:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
hl : p ∉ l
⊢ (mop i)^[n] p ∉ Finset.image (mop i)^[n] l.toFinset

State before:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
hl : p ∉ l
⊢ (mop i)^[n] p ∉ Finset.image (mop i)^[n] l.toFinset
Tactic:
simp_all
State after:
no goals