Theorem: LO.Propositional.Classical.Formula.neg_inj (Logic/Propositional/Classical/Basic/Formula.lean)

State before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q ↔ p = q
Tactic:
constructor
State after:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q → p = q

case mpr
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ p = q → ~p = ~q

State before:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q → p = q
Tactic:
intro h
State after:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
h : ~p = ~q
⊢ p = q

State before:
case mpr
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ p = q → ~p = ~q
Tactic:
exact congr_arg _
State after:
no goals