Theorem: Finset.premultimop_multimop_eq_of_subset_multimop (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
have := Set.eq_premultimop_multimop_of_subset_premultimop hs
State after:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : Set.multimop i n (Set.premultimop i n ↑s) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s

State before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : Set.multimop i n (Set.premultimop i n ↑s) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
rw [←premultimop_coe, ←multimop_coe] at this
State after:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : ↑(Finset.multimop i n (Finset.premultimop i n s)) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s

State before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : ↑(Finset.multimop i n (Finset.premultimop i n s)) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
exact Finset.coe_inj.mp this
State after:
no goals