Theorem: inj_not (Instructor/Lectures/grad/sets_relations.lean)

State before:
⊢ Injective Bool.not
Tactic:
unfold Injective
State after:
⊢ ∀ ⦃a₁ a₂ : Bool⦄, Bool.not a₁ = Bool.not a₂ → a₁ = a₂

State before:
⊢ ∀ ⦃a₁ a₂ : Bool⦄, Bool.not a₁ = Bool.not a₂ → a₁ = a₂
Tactic:
intros a1 a2 h
State after:
a1 a2 : Bool
h : Bool.not a1 = Bool.not a2
⊢ a1 = a2

State before:
a1 a2 : Bool
h : Bool.not a1 = Bool.not a2
⊢ a1 = a2
Tactic:
cases a1 with
  | true =>
      cases a2 with
      | true => rfl
      | false => nomatch h
  | false =>
        cases a2 with
        | true => nomatch h
        | false => rfl
State after:
no goals

State before:
case true
a2 : Bool
h : Bool.not true = Bool.not a2
⊢ true = a2
Tactic:
cases a2 with
| true => rfl
| false => nomatch h
State after:
no goals

State before:
case true.true
h : Bool.not true = Bool.not true
⊢ true = true
Tactic:
rfl
State after:
no goals

State before:
case true.false
h : Bool.not true = Bool.not false
⊢ true = false
Tactic:
nomatch h
State after:
no goals

State before:
case false
a2 : Bool
h : Bool.not false = Bool.not a2
⊢ false = a2
Tactic:
cases a2 with
| true => nomatch h
| false => rfl
State after:
no goals

State before:
case false.true
h : Bool.not false = Bool.not true
⊢ false = true
Tactic:
nomatch h
State after:
no goals

State before:
case false.false
h : Bool.not false = Bool.not false
⊢ false = false
Tactic:
rfl
State after:
no goals