Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
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 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: 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
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: 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
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: 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
t: α
t
e: α
e
=
t: α
t
:= match 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