Theorem: LO.UnaryModalOperator.multimop_injective (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ Injective (mop i)^[n]
Tactic:
apply Function.Injective.iterate (by simp)
State after:
no goals

State before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
n : ℕ
⊢ Injective (mop i)
Tactic:
simp
State after:
no goals