logic.lemmas

# More basic logic properties #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A few more logic lemmas. These are in their own file, rather than logic.basic, because it is convenient to be able to use the split_ifs tactic.

## Implementation notes #

We spell those lemmas out with dite and ite rather than the if then else notation because this would result in less delta-reduced statements.

@[protected]
theorem heq.eq {α : Sort u_1} {a b : α} :
a == b a = b

Alias of the forward direction of heq_iff_eq.

@[protected]
theorem eq.heq {α : Sort u_1} {a b : α} :
a = b a == b

Alias of the reverse direction of heq_iff_eq.

theorem eq.trans_ne {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b c) :
a c

Alias of ne_of_eq_of_ne.

theorem ne.trans_eq {α : Sort u} {a b c : α} (h₁ : a b) (h₂ : b = c) :
a c

Alias of ne_of_ne_of_eq.

theorem dite_dite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p α} {b : ¬p q α} {c : ¬p ¬q α} :
dite p a (λ (hp : ¬p), dite q (b hp) (c hp)) = dite q (λ (hq : q), dite p a (λ (hp : ¬p), b hp hq)) (λ (hq : ¬q), dite p a (λ (hp : ¬p), c hp hq))
theorem dite_dite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p q α} {b : p ¬q α} {c : ¬p α} :
dite p (λ (hp : p), dite q (a hp) (b hp)) c = dite q (λ (hq : q), dite p (λ (hp : p), a hp hq) c) (λ (hq : ¬q), dite p (λ (hp : p), b hp hq) c)
theorem ite_dite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : α} {b : q α} {c : ¬q α} :
ite p a (dite q b c) = dite q (λ (hq : q), ite p a (b hq)) (λ (hq : ¬q), ite p a (c hq))
theorem ite_dite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : q α} {b : ¬q α} {c : α} :
ite p (dite q a b) c = dite q (λ (hq : q), ite p (a hq) c) (λ (hq : ¬q), ite p (b hq) c)
theorem dite_ite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p α} {b c : ¬p α} :
dite p a (λ (hp : ¬p), ite q (b hp) (c hp)) = ite q (dite p a b) (dite p a c)
theorem dite_ite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b : p α} {c : ¬p α} :
dite p (λ (hp : p), ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c)
theorem ite_ite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b c : α} :
ite p a (ite q b c) = ite q (ite p a b) (ite p a c)
theorem ite_ite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b c : α} :
ite p (ite q a b) c = ite q (ite p a c) (ite p b c)
theorem Prop.forall {f : Prop Prop} :
( (p : Prop), f p) f true
theorem Prop.exists {f : Prop Prop} :
( (p : Prop), f p) f true