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

State before:
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q ↔ p = q
Tactic:
constructor
State after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q

State before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
. intro h; exact mop_injective h;
State after:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q

State before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
. simp_all;
State after:
no goals

State before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q
Tactic:
intro h
State after:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
h : mop i p = mop i q
⊢ p = q

State before:
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
h : mop i p = mop i q
⊢ p = q
Tactic:
exact mop_injective h
State after:
no goals

State before:
case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q
Tactic:
simp_all
State after:
no goals