/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/

import Std.Logic
import Mathlib.Init.Logic

/-! Lemmas use by the congruence closure module -/

theorem 
iff_eq_of_eq_true_left: ∀ {a b : Prop}, a = True → (a ↔ b) = b
iff_eq_of_eq_true_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = True
h : 
a: Prop
a = 
True: Prop
True) : (
a: Prop
a ↔ 
b: Prop
b) = 
b: Prop
b :=
  
h: a = True
h.
symm: ∀ {α : Sort ?u.16} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
true_iff_iff: ∀ {a : Prop}, (True ↔ a) ↔ a
true_iff_iff

theorem 
iff_eq_of_eq_true_right: ∀ {a b : Prop}, b = True → (a ↔ b) = a
iff_eq_of_eq_true_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = True
h : 
b: Prop
b = 
True: Prop
True) : (
a: Prop
a ↔ 
b: Prop
b) = 
a: Prop
a :=
  
h: b = True
h.
symm: ∀ {α : Sort ?u.58} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
iff_true_iff: ∀ {a : Prop}, (a ↔ True) ↔ a
iff_true_iff

theorem 
iff_eq_true_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b) = True
iff_eq_true_of_eq {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = b
h : 
a: Prop
a = 
b: Prop
b) : (
a: Prop
a ↔ 
b: Prop
b) = 
True: Prop
True :=
  
h: a = b
h ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
iff_self_iff: ∀ (a : Prop), (a ↔ a) ↔ True
iff_self_iff 
_: Prop
_)

theorem 
and_eq_of_eq_true_left: ∀ {a b : Prop}, a = True → (a ∧ b) = b
and_eq_of_eq_true_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = True
h : 
a: Prop
a = 
True: Prop
True) : (
a: Prop
a ∧ 
b: Prop
b) = 
b: Prop
b :=
  
h: a = True
h.
symm: ∀ {α : Sort ?u.134} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
true_and_iff: ∀ (p : Prop), True ∧ p ↔ p
true_and_iff 
_: Prop
_)

theorem 
and_eq_of_eq_true_right: ∀ {a b : Prop}, b = True → (a ∧ b) = a
and_eq_of_eq_true_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = True
h : 
b: Prop
b = 
True: Prop
True) : (
a: Prop
a ∧ 
b: Prop
b) = 
a: Prop
a :=
  
h: b = True
h.
symm: ∀ {α : Sort ?u.178} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
and_true_iff: ∀ (p : Prop), p ∧ True ↔ p
and_true_iff 
_: Prop
_)

theorem 
and_eq_of_eq_false_left: ∀ {a b : Prop}, a = False → (a ∧ b) = False
and_eq_of_eq_false_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = False
h : 
a: Prop
a = 
False: Prop
False) : (
a: Prop
a ∧ 
b: Prop
b) = 
False: Prop
False :=
  
h: a = False
h.
symm: ∀ {α : Sort ?u.222} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
false_and_iff: ∀ (p : Prop), False ∧ p ↔ False
false_and_iff 
_: Prop
_)

theorem 
and_eq_of_eq_false_right: ∀ {a b : Prop}, b = False → (a ∧ b) = False
and_eq_of_eq_false_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = False
h : 
b: Prop
b = 
False: Prop
False) : (
a: Prop
a ∧ 
b: Prop
b) = 
False: Prop
False :=
  
h: b = False
h.
symm: ∀ {α : Sort ?u.266} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
and_false_iff: ∀ (p : Prop), p ∧ False ↔ False
and_false_iff 
_: Prop
_)

theorem 
and_eq_of_eq: ∀ {a b : Prop}, a = b → (a ∧ b) = a
and_eq_of_eq {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = b
h : 
a: Prop
a = 
b: Prop
b) : (
a: Prop
a ∧ 
b: Prop
b) = 
a: Prop
a :=
  
h: a = b
h ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
and_self_iff: ∀ (p : Prop), p ∧ p ↔ p
and_self_iff 
_: Prop
_)

theorem 
or_eq_of_eq_true_left: ∀ {a b : Prop}, a = True → (a ∨ b) = True
or_eq_of_eq_true_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = True
h : 
a: Prop
a = 
True: Prop
True) : (
a: Prop
a ∨ 
b: Prop
b) = 
True: Prop
True :=
  
h: a = True
h.
symm: ∀ {α : Sort ?u.346} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
true_or_iff: ∀ (p : Prop), True ∨ p ↔ True
true_or_iff 
_: Prop
_)

theorem 
or_eq_of_eq_true_right: ∀ {a b : Prop}, b = True → (a ∨ b) = True
or_eq_of_eq_true_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = True
h : 
b: Prop
b = 
True: Prop
True) : (
a: Prop
a ∨ 
b: Prop
b) = 
True: Prop
True :=
  
h: b = True
h.
symm: ∀ {α : Sort ?u.390} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
or_true_iff: ∀ (p : Prop), p ∨ True ↔ True
or_true_iff 
_: Prop
_)

theorem 
or_eq_of_eq_false_left: ∀ {a b : Prop}, a = False → (a ∨ b) = b
or_eq_of_eq_false_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = False
h : 
a: Prop
a = 
False: Prop
False) : (
a: Prop
a ∨ 
b: Prop
b) = 
b: Prop
b :=
  
h: a = False
h.
symm: ∀ {α : Sort ?u.434} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
false_or_iff: ∀ (p : Prop), False ∨ p ↔ p
false_or_iff 
_: Prop
_)

theorem 
or_eq_of_eq_false_right: ∀ {a b : Prop}, b = False → (a ∨ b) = a
or_eq_of_eq_false_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = False
h : 
b: Prop
b = 
False: Prop
False) : (
a: Prop
a ∨ 
b: Prop
b) = 
a: Prop
a :=
  
h: b = False
h.
symm: ∀ {α : Sort ?u.478} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
or_false_iff: ∀ (p : Prop), p ∨ False ↔ p
or_false_iff 
_: Prop
_)

theorem 
or_eq_of_eq: ∀ {a b : Prop}, a = b → (a ∨ b) = a
or_eq_of_eq {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = b
h : 
a: Prop
a = 
b: Prop
b) : (
a: Prop
a ∨ 
b: Prop
b) = 
a: Prop
a :=
  
h: a = b
h ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
or_self_iff: ∀ (p : Prop), p ∨ p ↔ p
or_self_iff 
_: Prop
_)

theorem 
imp_eq_of_eq_true_left: ∀ {a b : Prop}, a = True → (a → b) = b
imp_eq_of_eq_true_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = True
h : 
a: Prop
a = 
True: Prop
True) : (
a: Prop
a → 
b: Prop
b) = 
b: Prop
b :=
  
h: a = True
h.
symm: ∀ {α : Sort ?u.561} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨fun 
h: ?m.584
h ↦ 
h: ?m.584
h 
trivial: True
trivial, fun 
h₁: ?m.589
h₁ 
_: ?m.592
_ ↦ 
h₁: ?m.589
h₁⟩

theorem 
imp_eq_of_eq_true_right: ∀ {a b : Prop}, b = True → (a → b) = True
imp_eq_of_eq_true_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = True
h : 
b: Prop
b = 
True: Prop
True) : (
a: Prop
a → 
b: Prop
b) = 
True: Prop
True :=
  
h: b = True
h.
symm: ∀ {α : Sort ?u.633} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨fun 
_: ?m.656
_ ↦ 
trivial: True
trivial, fun 
h₁: ?m.661
h₁ 
_: ?m.664
_ ↦ 
h₁: ?m.661
h₁⟩

theorem 
imp_eq_of_eq_false_left: ∀ {a b : Prop}, a = False → (a → b) = True
imp_eq_of_eq_false_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = False
h : 
a: Prop
a = 
False: Prop
False) : (
a: Prop
a → 
b: Prop
b) = 
True: Prop
True :=
  
h: a = False
h.
symm: ∀ {α : Sort ?u.705} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨fun 
_: ?m.728
_ ↦ 
trivial: True
trivial, fun 
_: ?m.733
_ 
h₂: ?m.736
h₂ ↦ 
False.elim: ∀ {C : Sort ?u.738}, False → C
False.elim 
h₂: ?m.736
h₂⟩

theorem 
imp_eq_of_eq_false_right: ∀ {a b : Prop}, b = False → (a → b) = ¬a
imp_eq_of_eq_false_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = False
h : 
b: Prop
b = 
False: Prop
False) : (
a: Prop
a → 
b: Prop
b) = 
Not: Prop → Prop
Not 
a: Prop
a :=
  
h: b = False
h.
symm: ∀ {α : Sort ?u.779} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨fun 
h: ?m.802
h ↦ 
h: ?m.802
h, fun 
hna: ?m.808
hna 
ha: ?m.811
ha ↦ 
hna: ?m.808
hna 
ha: ?m.811
ha⟩

/- Remark: the congruence closure module will only use the following lemma is
   cc_config.em is tt. -/
theorem 
not_imp_eq_of_eq_false_right: ∀ {a b : Prop}, b = False → (¬a → b) = a
not_imp_eq_of_eq_false_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: b = False
h : 
b: Prop
b = 
False: Prop
False) : (
Not: Prop → Prop
Not 
a: Prop
a → 
b: Prop
b) = 
a: Prop
a :=
  
h: b = False
h.
symm: ∀ {α : Sort ?u.852} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.intro (
    fun 
h': ?m.871
h' ↦ 
Classical.byContradiction: ∀ {p : Prop}, (¬p → False) → p
Classical.byContradiction fun 
hna: ?m.875
hna ↦ 
h': ?m.871
h' 
hna: ?m.875
hna) fun 
ha: ?m.884
ha 
hna: ?m.887
hna ↦ 
hna: ?m.887
hna 
ha: ?m.884
ha)

theorem 
imp_eq_true_of_eq: ∀ {a b : Prop}, a = b → (a → b) = True
imp_eq_true_of_eq {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: a = b
h : 
a: Prop
a = 
b: Prop
b) : (
a: Prop
a → 
b: Prop
b) = 
True: Prop
True :=
  
h: a = b
h ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext ⟨fun 
_: ?m.944
_ ↦ 
trivial: True
trivial, fun 
_: ?m.949
_ 
ha: ?m.952
ha ↦ 
ha: ?m.952
ha⟩

theorem 
not_eq_of_eq_true: ∀ {a : Prop}, a = True → (¬a) = False
not_eq_of_eq_true {
a: Prop
a : 
Prop: Type
Prop} (
h: a = True
h : 
a: Prop
a = 
True: Prop
True) : 
Not: Prop → Prop
Not 
a: Prop
a = 
False: Prop
False :=
  
h: a = True
h.
symm: ∀ {α : Sort ?u.987} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_true: ¬True ↔ False
not_true

theorem 
not_eq_of_eq_false: ∀ {a : Prop}, a = False → (¬a) = True
not_eq_of_eq_false {
a: Prop
a : 
Prop: Type
Prop} (
h: a = False
h : 
a: Prop
a = 
False: Prop
False) : 
Not: Prop → Prop
Not 
a: Prop
a = 
True: Prop
True :=
  
h: a = False
h.
symm: ∀ {α : Sort ?u.1024} {a b : α}, a = b → b = a
symm ▸ 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_false_iff: ¬False ↔ True
not_false_iff

theorem 
false_of_a_eq_not_a: ∀ {a : Prop}, a = ¬a → False
false_of_a_eq_not_a {
a: Prop
a : 
Prop: Type
Prop} (
h: a = ¬a
h : 
a: Prop
a = 
Not: Prop → Prop
Not 
a: Prop
a) : 
False: Prop
False :=
  have : 
Not: Prop → Prop
Not 
a: Prop
a := fun 
ha: ?m.1061
ha ↦ 
absurd: ∀ {a : Prop} {b : Sort ?u.1063}, a → ¬a → b
absurd 
ha: ?m.1061
ha (
Eq.mp: ∀ {α β : Sort ?u.1066}, α = β → α → β
Eq.mp 
h: a = ¬a
h 
ha: ?m.1061
ha)
  
absurd: ∀ {a : Prop} {b : Sort ?u.1076}, a → ¬a → b
absurd (
Eq.mpr: ∀ {α β : Sort ?u.1079}, α = β → β → α
Eq.mpr 
h: a = ¬a
h 
this: ¬a
this) 
this: ¬a
this

universe u

theorem 
if_eq_of_eq_true: ∀ {c : Prop} [d : Decidable c] {α : Sort u} (t e : α), c = True → (if c then t else e) = t
if_eq_of_eq_true {
c: Prop
c : 
Prop: Type
Prop} [
d: Decidable c
d : 
Decidable: Prop → Type
Decidable 
c: Prop
c] {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} (
t: α
t 
e: α
e : 
α: Sort u
α) (
h: c = True
h : 
c: Prop
c = 
True: Prop
True) :
  @
ite: {α : Sort ?u.1105} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
α: Sort u
α 
c: Prop
c 
d: Decidable c
d 
t: α
t 
e: α
e = 
t: α
t :=
  
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1114} {t e : α}, (if c then t else e) = t
if_pos (
of_eq_true: ∀ {p : Prop}, p = True → p
of_eq_true 
h: c = True
h)

theorem 
if_eq_of_eq_false: ∀ {c : Prop} [d : Decidable c] {α : Sort u} (t e : α), c = False → (if c then t else e) = e
if_eq_of_eq_false {
c: Prop
c : 
Prop: Type
Prop} [
d: Decidable c
d : 
Decidable: Prop → Type
Decidable 
c: Prop
c] {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} (
t: α
t 
e: α
e : 
α: Sort u
α) (
h: c = False
h : 
c: Prop
c = 
False: Prop
False) :
  @
ite: {α : Sort ?u.1155} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
α: Sort u
α 
c: Prop
c 
d: Decidable c
d 
t: α
t 
e: α
e = 
e: α
e :=
  
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1164} {t e : α}, (if c then t else e) = e
if_neg (
not_of_eq_false: ∀ {p : Prop}, p = False → ¬p
not_of_eq_false 
h: c = False
h)

theorem 
if_eq_of_eq: ∀ (c : Prop) [d : Decidable c] {α : Sort u} {t e : α}, t = e → (if c then t else e) = t
if_eq_of_eq (
c: Prop
c : 
Prop: Type
Prop) [
d: Decidable c
d : 
Decidable: Prop → Type
Decidable 
c: Prop
c] {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
t: α
t 
e: α
e : 
α: Sort u
α} (
h: t = e
h : 
t: α
t = 
e: α
e) :
  @
ite: {α : Sort ?u.1208} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
α: Sort u
α 
c: Prop
c 
d: Decidable c
d 
t: α
t 
e: α
e = 
t: α
t :=
  match 
d: Decidable c
d with
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue _ => 
rfl: ∀ {α : Sort ?u.1231} {a : α}, a = a
rfl
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse _ => 
Eq.symm: ∀ {α : Sort ?u.1249} {a b : α}, a = b → b = a
Eq.symm 
h: t = e
h

theorem 
eq_true_of_and_eq_true_left: ∀ {a b : Prop}, (a ∧ b) = True → a = True
eq_true_of_and_eq_true_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: (a ∧ b) = True
h : (
a: Prop
a ∧ 
b: Prop
b) = 
True: Prop
True) : 
a: Prop
a = 
True: Prop
True :=
  
eq_true: ∀ {p : Prop}, p → p = True
eq_true (
And.left: ∀ {a b : Prop}, a ∧ b → a
And.left (
of_eq_true: ∀ {p : Prop}, p = True → p
of_eq_true 
h: (a ∧ b) = True
h))

theorem 
eq_true_of_and_eq_true_right: ∀ {a b : Prop}, (a ∧ b) = True → b = True
eq_true_of_and_eq_true_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: (a ∧ b) = True
h : (
a: Prop
a ∧ 
b: Prop
b) = 
True: Prop
True) : 
b: Prop
b = 
True: Prop
True :=
  
eq_true: ∀ {p : Prop}, p → p = True
eq_true (
And.right: ∀ {a b : Prop}, a ∧ b → b
And.right (
of_eq_true: ∀ {p : Prop}, p = True → p
of_eq_true 
h: (a ∧ b) = True
h))

theorem 
eq_false_of_or_eq_false_left: ∀ {a b : Prop}, (a ∨ b) = False → a = False
eq_false_of_or_eq_false_left {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: (a ∨ b) = False
h : (
a: Prop
a ∨ 
b: Prop
b) = 
False: Prop
False) : 
a: Prop
a = 
False: Prop
False :=
  
eq_false: ∀ {p : Prop}, ¬p → p = False
eq_false fun 
ha: ?m.1399
ha ↦ 
False.elim: ∀ {C : Sort ?u.1401}, False → C
False.elim (
Eq.mp: ∀ {α β : Sort ?u.1403}, α = β → α → β
Eq.mp 
h: (a ∨ b) = False
h (
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl 
ha: ?m.1399
ha))

theorem 
eq_false_of_or_eq_false_right: ∀ {a b : Prop}, (a ∨ b) = False → b = False
eq_false_of_or_eq_false_right {
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop} (
h: (a ∨ b) = False
h : (
a: Prop
a ∨ 
b: Prop
b) = 
False: Prop
False) : 
b: Prop
b = 
False: Prop
False :=
  
eq_false: ∀ {p : Prop}, ¬p → p = False
eq_false fun 
hb: ?m.1435
hb ↦ 
False.elim: ∀ {C : Sort ?u.1437}, False → C
False.elim (
Eq.mp: ∀ {α β : Sort ?u.1439}, α = β → α → β
Eq.mp 
h: (a ∨ b) = False
h (
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr 
hb: ?m.1435
hb))

theorem 
eq_false_of_not_eq_true: ∀ {a : Prop}, (¬a) = True → a = False
eq_false_of_not_eq_true {
a: Prop
a : 
Prop: Type
Prop} (
h: (¬a) = True
h : 
Not: Prop → Prop
Not 
a: Prop
a = 
True: Prop
True) : 
a: Prop
a = 
False: Prop
False :=
  
eq_false: ∀ {p : Prop}, ¬p → p = False
eq_false fun 
ha: ?m.1468
ha ↦ 
absurd: ∀ {a : Prop} {b : Sort ?u.1470}, a → ¬a → b
absurd 
ha: ?m.1468
ha (
Eq.mpr: ∀ {α β : Sort ?u.1473}, α = β → β → α
Eq.mpr 
h: (¬a) = True
h 
trivial: True
trivial)

/- Remark: the congruence closure module will only use the following lemma is
   cc_config.em is tt. -/
theorem 
eq_true_of_not_eq_false: ∀ {a : Prop}, (¬a) = False → a = True
eq_true_of_not_eq_false {
a: Prop
a : 
Prop: Type
Prop} (
h: (¬a) = False
h : 
Not: Prop → Prop
Not 
a: Prop
a = 
False: Prop
False) : 
a: Prop
a = 
True: Prop
True :=
  
eq_true: ∀ {p : Prop}, p → p = True
eq_true (
Classical.byContradiction: ∀ {p : Prop}, (¬p → False) → p
Classical.byContradiction fun 
hna: ?m.1500
hna ↦ 
Eq.mp: ∀ {α β : Sort ?u.1502}, α = β → α → β
Eq.mp 
h: (¬a) = False
h 
hna: ?m.1500
hna)

theorem 
ne_of_eq_of_ne: ∀ {α : Sort u} {a b c : α}, a = b → b ≠ c → a ≠ c
ne_of_eq_of_ne {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
a: α
a 
b: α
b 
c: α
c : 
α: Sort u
α} (
h₁: a = b
h₁ : 
a: α
a = 
b: α
b) (
h₂: b ≠ c
h₂ : 
b: α
b ≠ 
c: α
c) : 
a: α
a ≠ 
c: α
c :=
  
h₁: a = b
h₁.
symm: ∀ {α : Sort ?u.1544} {a b : α}, a = b → b = a
symm ▸ 
h₂: b ≠ c
h₂

alias 
ne_of_eq_of_ne: ∀ {α : Sort u} {a b c : α}, a = b → b ≠ c → a ≠ c
ne_of_eq_of_ne ← 
Eq.trans_ne: ∀ {α : Sort u} {a b c : α}, a = b → b ≠ c → a ≠ c
Eq.trans_ne
#align eq.trans_ne 
Eq.trans_ne: ∀ {α : Sort u} {a b c : α}, a = b → b ≠ c → a ≠ c
Eq.trans_ne

theorem 
ne_of_ne_of_eq: ∀ {α : Sort u} {a b c : α}, a ≠ b → b = c → a ≠ c
ne_of_ne_of_eq {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
a: α
a 
b: α
b 
c: α
c : 
α: Sort u
α} (
h₁: a ≠ b
h₁ : 
a: α
a ≠ 
b: α
b) (
h₂: b = c
h₂ : 
b: α
b = 
c: α
c) : 
a: α
a ≠ 
c: α
c :=
  
h₂: b = c
h₂ ▸ 
h₁: a ≠ b
h₁

alias 
ne_of_ne_of_eq: ∀ {α : Sort u} {a b c : α}, a ≠ b → b = c → a ≠ c
ne_of_ne_of_eq ← 
Ne.trans_eq: ∀ {α : Sort u} {a b c : α}, a ≠ b → b = c → a ≠ c
Ne.trans_eq
#align ne.trans_eq 
Ne.trans_eq: ∀ {α : Sort u} {a b c : α}, a ≠ b → b = c → a ≠ c
Ne.trans_eq