import tactic.mk_simp_attribute

import tactic.reserved_notation

open function

local attribute [instance, priority 10] classical.prop_decidable

section miscellany

attribute [inline] and.decidable or.decidable decidable.false xor.decidable iff.decidable

decidable.true implies.decidable not.decidable ne.decidable

bool.decidable_eq decidable.to_bool

attribute [simp] cast_eq cast_heq

variables {α : Type*} {β : Type*}

@[reducible] def hidden {α : Sort*} {a : α} := a

def empty.elim {C : Sort*} : empty → C.

instance : subsingleton empty := ⟨λa, a.elim⟩

instance subsingleton.prod {α β : Type*} [subsingleton α] [subsingleton β] : subsingleton (α × β) :=

⟨by { intros a b, cases a, cases b, congr, }⟩

instance : decidable_eq empty := λa, a.elim

instance sort.inhabited : inhabited Sort* := ⟨punit⟩

instance sort.inhabited' : inhabited default := ⟨punit.star⟩

instance psum.inhabited_left {α β} [inhabited α] : inhabited (psum α β) := ⟨psum.inl default⟩

instance psum.inhabited_right {α β} [inhabited β] : inhabited (psum α β) := ⟨psum.inr default⟩

@[priority 10] instance decidable_eq_of_subsingleton

{α} [subsingleton α] : decidable_eq α

| a b := is_true (subsingleton.elim a b)

@[simp, nontriviality] lemma eq_iff_true_of_subsingleton {α : Sort*} [subsingleton α] (x y : α) :

x = y ↔ true :=

by cc

lemma subsingleton_of_forall_eq {α : Sort*} (x : α) (h : ∀ y, y = x) : subsingleton α :=

⟨λ a b, (h a).symm ▸ (h b).symm ▸ rfl⟩

lemma subsingleton_iff_forall_eq {α : Sort*} (x : α) : subsingleton α ↔ ∀ y, y = x :=

⟨λ h y, @subsingleton.elim _ h y x, subsingleton_of_forall_eq x⟩

instance subtype.subsingleton (α : Sort*) [subsingleton α] (p : α → Prop) :

subsingleton (subtype p) :=

⟨λ ⟨x,_⟩ ⟨y,_⟩, have x = y, from subsingleton.elim _ _, by { cases this, refl }⟩

@[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]

(a : α) : (a : γ) = (a : β) := rfl

theorem coe_fn_coe_trans

{α β γ δ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ δ]

(x : α) : @coe_fn α _ _ x = @coe_fn β _ _ x := rfl

theorem coe_fn_coe_trans'

{α β γ} {δ : _} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ (λ _, δ)]

(x : α) : @coe_fn α _ _ x = @coe_fn β _ _ x := rfl

@[simp] theorem coe_fn_coe_base

{α β γ} [has_coe α β] [has_coe_to_fun β γ]

(x : α) : @coe_fn α _ _ x = @coe_fn β _ _ x := rfl

theorem coe_fn_coe_base'

{α β} {γ : _} [has_coe α β] [has_coe_to_fun β (λ _, γ)]

(x : α) : @coe_fn α _ _ x = @coe_fn β _ _ x := rfl

attribute [instance, priority 10] coe_sort_trans

theorem coe_sort_coe_trans

{α β γ δ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ δ]

(x : α) : @coe_sort α _ _ x = @coe_sort β _ _ x := rfl

library_note "function coercion"

@[simp] theorem coe_sort_coe_base

{α β γ} [has_coe α β] [has_coe_to_sort β γ]

(x : α) : @coe_sort α _ _ x = @coe_sort β _ _ x := rfl

inductive {u} pempty : Sort u

def pempty.elim {C : Sort*} : pempty → C.

instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩

@[simp] lemma not_nonempty_pempty : ¬ nonempty pempty :=

assume ⟨h⟩, h.elim

lemma congr_heq {α β γ : Sort*} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : f == g)

(h₂ : x == y) : f x = g y :=

by { cases h₂, cases h₁, refl }

lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂

| a _ rfl := heq.rfl

lemma ulift.down_injective {α : Sort*} : function.injective (@ulift.down α)

| ⟨a⟩ ⟨b⟩ rfl := rfl

@[simp] lemma ulift.down_inj {α : Sort*} {a b : ulift α} : a.down = b.down ↔ a = b :=

⟨λ h, ulift.down_injective h, λ h, by rw h⟩

lemma plift.down_injective {α : Sort*} : function.injective (@plift.down α)

| ⟨a⟩ ⟨b⟩ rfl := rfl

@[simp] lemma plift.down_inj {α : Sort*} {a b : plift α} : a.down = b.down ↔ a = b :=

⟨λ h, plift.down_injective h, λ h, by rw h⟩

attribute [symm] ne.symm

lemma ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨ne.symm, ne.symm⟩

@[simp] lemma eq_iff_eq_cancel_left {α : Sort*} {b c : α} :

(∀ {a}, a = b ↔ a = c) ↔ (b = c) :=

⟨λ h, by rw [← h], λ h a, by rw h⟩

@[simp] lemma eq_iff_eq_cancel_right {α : Sort*} {a b : α} :

(∀ {c}, a = c ↔ b = c) ↔ (a = b) :=

⟨λ h, by rw h, λ h a, by rw h⟩

class fact (p : Prop) : Prop := (out [] : p)

library_note "fact non-instances"

lemma fact.elim {p : Prop} (h : fact p) : p := h.1

lemma fact_iff {p : Prop} : fact p ↔ p := ⟨λ h, h.1, λ h, ⟨h⟩⟩

@[reducible] def function.swap₂ {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}

{φ : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → Sort*} (f : Π i₁ j₁ i₂ j₂, φ i₁ j₁ i₂ j₂) :

Π i₂ j₂ i₁ j₁, φ i₁ j₁ i₂ j₂ :=

λ i₂ j₂ i₁ j₁, f i₁ j₁ i₂ j₂

def auto_param.out {α : Sort*} {n : name} (x : auto_param α n) : α := x

def opt_param.out {α : Sort*} {d : α} (x : α := d) : α := x

end miscellany

open function

theorem false_ne_true : false ≠ true

| h := h.symm ▸ trivial

theorem eq_true_iff {a : Prop} : (a = true) = a :=

have (a ↔ true) = a, from propext (iff_true a),

eq.subst (@iff_eq_eq a true) this

section propositional

variables {a b c d e f : Prop}

instance : is_refl Prop iff := ⟨iff.refl⟩

instance : is_trans Prop iff := ⟨λ _ _ _, iff.trans⟩

theorem iff_of_eq (e : a = b) : a ↔ b := e ▸ iff.rfl

theorem iff_iff_eq : (a ↔ b) ↔ a = b := ⟨propext, iff_of_eq⟩

@[simp] lemma eq_iff_iff {p q : Prop} : (p = q) ↔ (p ↔ q) := iff_iff_eq.symm

@[simp] theorem imp_self : (a → a) ↔ true := iff_true_intro id

lemma iff.imp (h₁ : a ↔ b) (h₂ : c ↔ d) : (a → c) ↔ (b → d) := imp_congr h₁ h₂

@[simp] lemma eq_true_eq_id : eq true = id :=

by { funext, simp only [true_iff, id.def, iff_self, eq_iff_iff], }

theorem imp_intro {α β : Prop} (h : α) : β → α := λ _, h

theorem imp_false : (a → false) ↔ ¬ a := iff.rfl

theorem imp_and_distrib {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=

⟨λ h, ⟨λ ha, (h ha).left, λ ha, (h ha).right⟩,

λ h ha, ⟨h.left ha, h.right ha⟩⟩

@[simp, mfld_simps] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) :=

iff.intro (λ h ha hb, h ⟨ha, hb⟩) (λ h ⟨ha, hb⟩, h ha hb)

theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) :=

iff_iff_implies_and_implies _ _

theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) :=

iff_def.trans and.comm

theorem imp_true_iff {α : Sort*} : (α → true) ↔ true :=

iff_true_intro $ λ_, trivial

theorem imp_iff_right (ha : a) : (a → b) ↔ b :=

⟨λf, f ha, imp_intro⟩

lemma imp_iff_not (hb : ¬ b) : a → b ↔ ¬ a := imp_congr_right $ λ _, iff_false_intro hb

theorem decidable.imp_iff_right_iff [decidable a] : ((a → b) ↔ b) ↔ (a ∨ b) :=

⟨λ H, (decidable.em a).imp_right $ λ ha', H.1 $ λ ha, (ha' ha).elim,

λ H, H.elim imp_iff_right $ λ hb, ⟨λ hab, hb, λ _ _, hb⟩⟩

@[simp] theorem imp_iff_right_iff : ((a → b) ↔ b) ↔ (a ∨ b) :=

decidable.imp_iff_right_iff

lemma decidable.and_or_imp [decidable a] : (a ∧ b) ∨ (a → c) ↔ a → (b ∨ c) :=

if ha : a then by simp only [ha, true_and, true_implies_iff]

else by simp only [ha, false_or, false_and, false_implies_iff]

@[simp] theorem and_or_imp : (a ∧ b) ∨ (a → c) ↔ a → (b ∨ c) :=

decidable.and_or_imp

protected lemma function.mt : (a → b) → ¬ b → ¬ a := mt

def not.elim {α : Sort*} (H1 : ¬a) (H2 : a) : α := absurd H2 H1

@[reducible] theorem not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a := mt H1 H2

theorem not_not_of_not_imp : ¬(a → b) → ¬¬a :=

mt not.elim

theorem not_of_not_imp {a : Prop} : ¬(a → b) → ¬b :=

mt imp_intro

theorem dec_em (p : Prop) [decidable p] : p ∨ ¬p := decidable.em p

theorem dec_em' (p : Prop) [decidable p] : ¬p ∨ p := (dec_em p).swap

theorem em (p : Prop) : p ∨ ¬p := classical.em _

theorem em' (p : Prop) : ¬p ∨ p := (em p).swap

theorem or_not {p : Prop} : p ∨ ¬p := em _

section eq_or_ne

variables {α : Sort*} (x y : α)

theorem decidable.eq_or_ne [decidable (x = y)] : x = y ∨ x ≠ y := dec_em $ x = y

theorem decidable.ne_or_eq [decidable (x = y)] : x ≠ y ∨ x = y := dec_em' $ x = y

theorem eq_or_ne : x = y ∨ x ≠ y := em $ x = y

theorem ne_or_eq : x ≠ y ∨ x = y := em' $ x = y

end eq_or_ne

theorem by_contradiction {p} : (¬p → false) → p := decidable.by_contradiction

theorem by_contra {p} : (¬p → false) → p := decidable.by_contradiction

library_note "decidable namespace"

library_note "decidable arguments"

protected theorem decidable.not_not [decidable a] : ¬¬a ↔ a :=

iff.intro decidable.by_contradiction not_not_intro

@[simp] theorem not_not : ¬¬a ↔ a := decidable.not_not

theorem of_not_not : ¬¬a → a := by_contra

lemma not_ne_iff {α : Sort*} {a b : α} : ¬ a ≠ b ↔ a = b := not_not

protected theorem decidable.of_not_imp [decidable a] (h : ¬ (a → b)) : a :=

decidable.by_contradiction (not_not_of_not_imp h)

theorem of_not_imp : ¬ (a → b) → a := decidable.of_not_imp

protected theorem decidable.not_imp_symm [decidable a] (h : ¬a → b) (hb : ¬b) : a :=

decidable.by_contradiction $ hb ∘ h

theorem not.decidable_imp_symm [decidable a] : (¬a → b) → ¬b → a := decidable.not_imp_symm

theorem not.imp_symm : (¬a → b) → ¬b → a := not.decidable_imp_symm

protected theorem decidable.not_imp_comm [decidable a] [decidable b] : (¬a → b) ↔ (¬b → a) :=

⟨not.decidable_imp_symm, not.decidable_imp_symm⟩

theorem not_imp_comm : (¬a → b) ↔ (¬b → a) := decidable.not_imp_comm

@[simp] theorem imp_not_self : (a → ¬a) ↔ ¬a := ⟨λ h ha, h ha ha, λ h _, h⟩

theorem decidable.not_imp_self [decidable a] : (¬a → a) ↔ a :=

by { have := @imp_not_self (¬a), rwa decidable.not_not at this }

@[simp] theorem not_imp_self : (¬a → a) ↔ a := decidable.not_imp_self

theorem imp.swap : (a → b → c) ↔ (b → a → c) :=

⟨swap, swap⟩

theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) :=

imp.swap

lemma iff.not (h : a ↔ b) : ¬ a ↔ ¬ b := not_congr h

lemma iff.not_left (h : a ↔ ¬ b) : ¬ a ↔ b := h.not.trans not_not

lemma iff.not_right (h : ¬ a ↔ b) : a ↔ ¬ b := not_not.symm.trans h.not

protected lemma iff.ne {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c = d) → (a ≠ b ↔ c ≠ d) :=

iff.not

lemma iff.ne_left {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c ≠ d) → (a ≠ b ↔ c = d) :=

iff.not_left

lemma iff.ne_right {α β : Sort*} {a b : α} {c d : β} : (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d) :=

iff.not_right

@[simp] theorem xor_true : xor true = not := funext $ λ a, by simp [xor]

@[simp] theorem xor_false : xor false = id := funext $ λ a, by simp [xor]

theorem xor_comm (a b) : xor a b ↔ xor b a := or_comm _ _

instance : is_commutative Prop xor := ⟨λ a b, propext $ xor_comm a b⟩

@[simp] theorem xor_self (a : Prop) : xor a a = false := by simp [xor]

@[simp] theorem xor_not_left : xor (¬a) b ↔ (a ↔ b) := by by_cases a; simp *

@[simp] theorem xor_not_right : xor a (¬b) ↔ (a ↔ b) := by by_cases a; simp *

theorem xor_not_not : xor (¬a) (¬b) ↔ xor a b := by simp [xor, or_comm, and_comm]

protected theorem xor.or (h : xor a b) : a ∨ b := h.imp and.left and.left

lemma iff.and (h₁ : a ↔ b) (h₂ : c ↔ d) : a ∧ c ↔ b ∧ d := and_congr h₁ h₂

theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=

and.comm.trans $ (and_congr_right h).trans and.comm

theorem and_congr_left' (h : a ↔ b) : a ∧ c ↔ b ∧ c := h.and iff.rfl

theorem and_congr_right' (h : b ↔ c) : a ∧ b ↔ a ∧ c := iff.rfl.and h

theorem not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) :=

mt and.left

theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) :=

mt and.right

theorem and.imp_left (h : a → b) : a ∧ c → b ∧ c :=

and.imp h id

theorem and.imp_right (h : a → b) : c ∧ a → c ∧ b :=

and.imp id h

lemma and.right_comm : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=

by simp only [and.left_comm, and.comm]

lemma and_and_and_comm (a b c d : Prop) : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d :=

by rw [←and_assoc, @and.right_comm a, and_assoc]

lemma and_and_distrib_left (a b c : Prop) : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ (a ∧ c) :=

by rw [and_and_and_comm, and_self]

lemma and_and_distrib_right (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ (b ∧ c) :=

by rw [and_and_and_comm, and_self]

lemma and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a := by simp only [and.left_comm, and.comm]

lemma and.rotate : a ∧ b ∧ c → b ∧ c ∧ a := and_rotate.1

theorem and_not_self_iff (a : Prop) : a ∧ ¬ a ↔ false :=

iff.intro (assume h, (h.right) (h.left)) (assume h, h.elim)

theorem not_and_self_iff (a : Prop) : ¬ a ∧ a ↔ false :=

iff.intro (assume ⟨hna, ha⟩, hna ha) false.elim

theorem and_iff_left_of_imp {a b : Prop} (h : a → b) : (a ∧ b) ↔ a :=

iff.intro and.left (λ ha, ⟨ha, h ha⟩)

theorem and_iff_right_of_imp {a b : Prop} (h : b → a) : (a ∧ b) ↔ b :=

iff.intro and.right (λ hb, ⟨h hb, hb⟩)

lemma ne_and_eq_iff_right {α : Sort*} {a b c : α} (h : b ≠ c) : a ≠ b ∧ a = c ↔ a = c :=

and_iff_right_of_imp (λ h2, h2.symm ▸ h.symm)

@[simp] theorem and_iff_left_iff_imp {a b : Prop} : ((a ∧ b) ↔ a) ↔ (a → b) :=

⟨λ h ha, (h.2 ha).2, and_iff_left_of_imp⟩

@[simp] theorem and_iff_right_iff_imp {a b : Prop} : ((a ∧ b) ↔ b) ↔ (b → a) :=

⟨λ h ha, (h.2 ha).1, and_iff_right_of_imp⟩

@[simp] lemma iff_self_and {p q : Prop} : (p ↔ p ∧ q) ↔ (p → q) :=

by rw [@iff.comm p, and_iff_left_iff_imp]

@[simp] lemma iff_and_self {p q : Prop} : (p ↔ q ∧ p) ↔ (p → q) :=

by rw [and_comm, iff_self_and]

@[simp] lemma and.congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=

⟨λ h ha, by simp [ha] at h; exact h, and_congr_right⟩

@[simp] lemma and.congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b) :=

by simp only [and.comm, ← and.congr_right_iff]

@[simp] lemma and_self_left : a ∧ a ∧ b ↔ a ∧ b :=

⟨λ h, ⟨h.1, h.2.2⟩, λ h, ⟨h.1, h.1, h.2⟩⟩

@[simp] lemma and_self_right : (a ∧ b) ∧ b ↔ a ∧ b :=

⟨λ h, ⟨h.1.1, h.2⟩, λ h, ⟨⟨h.1, h.2⟩, h.2⟩⟩

lemma iff.or (h₁ : a ↔ b) (h₂ : c ↔ d) : a ∨ c ↔ b ∨ d := or_congr h₁ h₂

lemma or_congr_left' (h : a ↔ b) : a ∨ c ↔ b ∨ c := h.or iff.rfl

lemma or_congr_right' (h : b ↔ c) : a ∨ b ↔ a ∨ c := iff.rfl.or h

theorem or.right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, or_comm b]

lemma or_or_or_comm (a b c d : Prop) : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d :=

by rw [←or_assoc, @or.right_comm a, or_assoc]

lemma or_or_distrib_left (a b c : Prop) : a ∨ (b ∨ c) ↔ (a ∨ b) ∨ (a ∨ c) :=

by rw [or_or_or_comm, or_self]

lemma or_or_distrib_right (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ (b ∨ c) :=

by rw [or_or_or_comm, or_self]

lemma or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or.left_comm, or.comm]

lemma or.rotate : a ∨ b ∨ c → b ∨ c ∨ a := or_rotate.1

theorem or_of_or_of_imp_of_imp (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) : c ∨ d :=

or.imp h₂ h₃ h₁

theorem or_of_or_of_imp_left (h₁ : a ∨ c) (h : a → b) : b ∨ c :=

or.imp_left h h₁

theorem or_of_or_of_imp_right (h₁ : c ∨ a) (h : a → b) : c ∨ b :=

or.imp_right h h₁

theorem or.elim3 (h : a ∨ b ∨ c) (ha : a → d) (hb : b → d) (hc : c → d) : d :=

or.elim h ha (assume h₂, or.elim h₂ hb hc)

lemma or.imp3 (had : a → d) (hbe : b → e) (hcf : c → f) : a ∨ b ∨ c → d ∨ e ∨ f :=

or.imp had $ or.imp hbe hcf

theorem or_imp_distrib : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=

⟨assume h, ⟨assume ha, h (or.inl ha), assume hb, h (or.inr hb)⟩,

assume ⟨ha, hb⟩, or.rec ha hb⟩

protected theorem decidable.or_iff_not_imp_left [decidable a] : a ∨ b ↔ (¬ a → b) :=

⟨or.resolve_left, λ h, dite _ or.inl (or.inr ∘ h)⟩

theorem or_iff_not_imp_left : a ∨ b ↔ (¬ a → b) := decidable.or_iff_not_imp_left

protected theorem decidable.or_iff_not_imp_right [decidable b] : a ∨ b ↔ (¬ b → a) :=

or.comm.trans decidable.or_iff_not_imp_left

theorem or_iff_not_imp_right : a ∨ b ↔ (¬ b → a) := decidable.or_iff_not_imp_right

protected lemma decidable.not_or_of_imp [decidable a] (h : a → b) : ¬ a ∨ b :=

dite _ (or.inr ∘ h) or.inl

lemma not_or_of_imp : (a → b) → ¬ a ∨ b := decidable.not_or_of_imp

protected lemma decidable.or_not_of_imp [decidable a] (h : a → b) : b ∨ ¬ a :=

dite _ (or.inl ∘ h) or.inr

lemma or_not_of_imp : (a → b) → b ∨ ¬ a := decidable.or_not_of_imp

protected lemma decidable.imp_iff_not_or [decidable a] : a → b ↔ ¬ a ∨ b :=

⟨decidable.not_or_of_imp, or.neg_resolve_left⟩

lemma imp_iff_not_or : a → b ↔ ¬ a ∨ b := decidable.imp_iff_not_or

protected lemma decidable.imp_iff_or_not [decidable b] : b → a ↔ a ∨ ¬ b :=

decidable.imp_iff_not_or.trans or.comm

lemma imp_iff_or_not : b → a ↔ a ∨ ¬ b := decidable.imp_iff_or_not

protected theorem decidable.not_imp_not [decidable a] : (¬ a → ¬ b) ↔ (b → a) :=

⟨assume h hb, decidable.by_contradiction $ assume na, h na hb, mt⟩

theorem not_imp_not : (¬ a → ¬ b) ↔ (b → a) := decidable.not_imp_not

protected theorem function.mtr : (¬ a → ¬ b) → (b → a) := not_imp_not.mp

protected lemma decidable.or_congr_left [decidable c] (h : ¬ c → (a ↔ b)) : a ∨ c ↔ b ∨ c :=

by { rw [decidable.or_iff_not_imp_right, decidable.or_iff_not_imp_right], exact imp_congr_right h }

lemma or_congr_left (h : ¬ c → (a ↔ b)) : a ∨ c ↔ b ∨ c :=

decidable.or_congr_left h

protected lemma decidable.or_congr_right [decidable a] (h : ¬ a → (b ↔ c)) : a ∨ b ↔ a ∨ c :=

by { rw [decidable.or_iff_not_imp_left, decidable.or_iff_not_imp_left], exact imp_congr_right h }

lemma or_congr_right (h : ¬ a → (b ↔ c)) : a ∨ b ↔ a ∨ c :=

decidable.or_congr_right h

@[simp] theorem or_iff_left_iff_imp : (a ∨ b ↔ a) ↔ (b → a) :=

⟨λ h hb, h.1 (or.inr hb), or_iff_left_of_imp⟩

@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) :=

by rw [or_comm, or_iff_left_iff_imp]

lemma or_iff_left (hb : ¬ b) : a ∨ b ↔ a := ⟨λ h, h.resolve_right hb, or.inl⟩

lemma or_iff_right (ha : ¬ a) : a ∨ b ↔ b := ⟨λ h, h.resolve_left ha, or.inr⟩

theorem and_or_distrib_left : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) :=

⟨λ ⟨ha, hbc⟩, hbc.imp (and.intro ha) (and.intro ha),

or.rec (and.imp_right or.inl) (and.imp_right or.inr)⟩

theorem or_and_distrib_right : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) :=

(and.comm.trans and_or_distrib_left).trans (and.comm.or and.comm)

theorem or_and_distrib_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) :=

⟨or.rec (λha, and.intro (or.inl ha) (or.inl ha)) (and.imp or.inr or.inr),

and.rec $ or.rec (imp_intro ∘ or.inl) (or.imp_right ∘ and.intro)⟩

theorem and_or_distrib_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) :=

(or.comm.trans or_and_distrib_left).trans (or.comm.and or.comm)

@[simp] lemma or_self_left : a ∨ a ∨ b ↔ a ∨ b :=

⟨λ h, h.elim or.inl id, λ h, h.elim or.inl (or.inr ∘ or.inr)⟩

@[simp] lemma or_self_right : (a ∨ b) ∨ b ↔ a ∨ b :=

⟨λ h, h.elim id or.inr, λ h, h.elim (or.inl ∘ or.inl) or.inr⟩

lemma iff.iff (h₁ : a ↔ b) (h₂ : c ↔ d) : (a ↔ c) ↔ (b ↔ d) := iff_congr h₁ h₂

theorem iff_of_true (ha : a) (hb : b) : a ↔ b :=

⟨λ_, hb, λ _, ha⟩

theorem iff_of_false (ha : ¬a) (hb : ¬b) : a ↔ b :=

⟨ha.elim, hb.elim⟩

theorem iff_true_left (ha : a) : (a ↔ b) ↔ b :=

⟨λ h, h.1 ha, iff_of_true ha⟩

theorem iff_true_right (ha : a) : (b ↔ a) ↔ b :=

iff.comm.trans (iff_true_left ha)

theorem iff_false_left (ha : ¬a) : (a ↔ b) ↔ ¬b :=

⟨λ h, mt h.2 ha, iff_of_false ha⟩

theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b :=

iff.comm.trans (iff_false_left ha)

lemma iff_mpr_iff_true_intro {P : Prop} (h : P) : iff.mpr (iff_true_intro h) true.intro = h := rfl

protected theorem decidable.imp_or_distrib [decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=

by simp [decidable.imp_iff_not_or, or.comm, or.left_comm]

theorem imp_or_distrib : (a → b ∨ c) ↔ (a → b) ∨ (a → c) := decidable.imp_or_distrib

protected theorem decidable.imp_or_distrib' [decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=

by by_cases b; simp [h, or_iff_right_of_imp ((∘) false.elim)]

theorem imp_or_distrib' : (a → b ∨ c) ↔ (a → b) ∨ (a → c) := decidable.imp_or_distrib'

theorem not_imp_of_and_not : a ∧ ¬ b → ¬ (a → b)

| ⟨ha, hb⟩ h := hb $ h ha

protected theorem decidable.not_imp [decidable a] : ¬(a → b) ↔ a ∧ ¬b :=

⟨λ h, ⟨decidable.of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩

theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := decidable.not_imp

lemma imp_imp_imp (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) :=

assume (h₂ : a → b), h₁ ∘ h₂ ∘ h₀

protected theorem decidable.peirce (a b : Prop) [decidable a] : ((a → b) → a) → a :=

if ha : a then λ h, ha else λ h, h ha.elim

theorem peirce (a b : Prop) : ((a → b) → a) → a := decidable.peirce _ _

theorem peirce' {a : Prop} (H : ∀ b : Prop, (a → b) → a) : a := H _ id

protected theorem decidable.not_iff_not [decidable a] [decidable b] : (¬ a ↔ ¬ b) ↔ (a ↔ b) :=

by rw [@iff_def (¬ a), @iff_def' a]; exact decidable.not_imp_not.and decidable.not_imp_not

theorem not_iff_not : (¬ a ↔ ¬ b) ↔ (a ↔ b) := decidable.not_iff_not

protected theorem decidable.not_iff_comm [decidable a] [decidable b] : (¬ a ↔ b) ↔ (¬ b ↔ a) :=

by rw [@iff_def (¬ a), @iff_def (¬ b)]; exact decidable.not_imp_comm.and imp_not_comm

theorem not_iff_comm : (¬ a ↔ b) ↔ (¬ b ↔ a) := decidable.not_iff_comm

protected theorem decidable.not_iff : ∀ [decidable b], ¬ (a ↔ b) ↔ (¬ a ↔ b) :=

by intro h; cases h; simp only [h, iff_true, iff_false]

theorem not_iff : ¬ (a ↔ b) ↔ (¬ a ↔ b) := decidable.not_iff

protected theorem decidable.iff_not_comm [decidable a] [decidable b] : (a ↔ ¬ b) ↔ (b ↔ ¬ a) :=

by rw [@iff_def a, @iff_def b]; exact imp_not_comm.and decidable.not_imp_comm

theorem iff_not_comm : (a ↔ ¬ b) ↔ (b ↔ ¬ a) := decidable.iff_not_comm

protected theorem decidable.iff_iff_and_or_not_and_not [decidable b] :

(a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=

by { split; intro h,

{ rw h; by_cases b; [left,right]; split; assumption },

{ cases h with h h; cases h; split; intro; { contradiction <|> assumption } } }

theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=

decidable.iff_iff_and_or_not_and_not

lemma decidable.iff_iff_not_or_and_or_not [decidable a] [decidable b] :

(a ↔ b) ↔ ((¬a ∨ b) ∧ (a ∨ ¬b)) :=

rw [iff_iff_implies_and_implies a b],

simp only [decidable.imp_iff_not_or, or.comm]

lemma iff_iff_not_or_and_or_not : (a ↔ b) ↔ ((¬a ∨ b) ∧ (a ∨ ¬b)) :=

decidable.iff_iff_not_or_and_or_not

protected theorem decidable.not_and_not_right [decidable b] : ¬(a ∧ ¬b) ↔ (a → b) :=

⟨λ h ha, h.decidable_imp_symm $ and.intro ha, λ h ⟨ha, hb⟩, hb $ h ha⟩

theorem not_and_not_right : ¬(a ∧ ¬b) ↔ (a → b) := decidable.not_and_not_right

@[inline] def decidable_of_iff (a : Prop) (h : a ↔ b) [D : decidable a] : decidable b :=

decidable_of_decidable_of_iff D h

@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [D : decidable b] : decidable a :=

decidable_of_decidable_of_iff D h.symm

def decidable_of_bool : ∀ (b : bool) (h : b ↔ a), decidable a

| tt h := is_true (h.1 rfl)

| ff h := is_false (mt h.2 bool.ff_ne_tt)

theorem not_and_of_not_or_not (h : ¬ a ∨ ¬ b) : ¬ (a ∧ b)

| ⟨ha, hb⟩ := or.elim h (absurd ha) (absurd hb)

protected theorem decidable.not_and_distrib [decidable a] : ¬ (a ∧ b) ↔ ¬a ∨ ¬b :=

⟨λ h, if ha : a then or.inr (λ hb, h ⟨ha, hb⟩) else or.inl ha, not_and_of_not_or_not⟩

protected theorem decidable.not_and_distrib' [decidable b] : ¬ (a ∧ b) ↔ ¬a ∨ ¬b :=

⟨λ h, if hb : b then or.inl (λ ha, h ⟨ha, hb⟩) else or.inr hb, not_and_of_not_or_not⟩

theorem not_and_distrib : ¬ (a ∧ b) ↔ ¬a ∨ ¬b := decidable.not_and_distrib

@[simp] theorem not_and : ¬ (a ∧ b) ↔ (a → ¬ b) := and_imp

theorem not_and' : ¬ (a ∧ b) ↔ b → ¬a :=

not_and.trans imp_not_comm

theorem not_or_distrib : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b := or_imp_distrib

protected theorem decidable.or_iff_not_and_not [decidable a] [decidable b] : a ∨ b ↔ ¬ (¬a ∧ ¬b) :=

by rw [← not_or_distrib, decidable.not_not]

theorem or_iff_not_and_not : a ∨ b ↔ ¬ (¬a ∧ ¬b) := decidable.or_iff_not_and_not

protected theorem decidable.and_iff_not_or_not [decidable a] [decidable b] :

a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=

by rw [← decidable.not_and_distrib, decidable.not_not]

theorem and_iff_not_or_not : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) := decidable.and_iff_not_or_not

@[simp] theorem not_xor (P Q : Prop) : ¬ xor P Q ↔ (P ↔ Q) :=

by simp only [not_and, xor, not_or_distrib, not_not, ← iff_iff_implies_and_implies]

theorem xor_iff_not_iff (P Q : Prop) : xor P Q ↔ ¬ (P ↔ Q) := (not_xor P Q).not_right

theorem xor_iff_iff_not : xor a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]

theorem xor_iff_not_iff' : xor a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]

end propositional

section mem

variables {α β : Type*} [has_mem α β] {s t : β} {a b : α}

lemma ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt $ λ e, e ▸ h

lemma ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt $ λ e, e ▸ h

lemma has_mem.mem.ne_of_not_mem : a ∈ s → b ∉ s → a ≠ b := ne_of_mem_of_not_mem

lemma has_mem.mem.ne_of_not_mem' : a ∈ s → a ∉ t → s ≠ t := ne_of_mem_of_not_mem'

end mem

section equality

variables {α : Sort*} {a b : α}

@[simp, mfld_simps] theorem heq_iff_eq : a == b ↔ a = b :=

⟨eq_of_heq, heq_of_eq⟩

theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : hp == hq :=

have p = q, from propext ⟨λ _, hq, λ _, hp⟩,

by subst q; refl

lemma ball_cond_comm {α} {s : α → Prop} {p : α → α → Prop} :

(∀ a, s a → ∀ b, s b → p a b) ↔ (∀ a b, s a → s b → p a b) :=

⟨λ h a b ha hb, h a ha b hb, λ h a ha b hb, h a b ha hb⟩

lemma ball_mem_comm {α β} [has_mem α β] {s : β} {p : α → α → Prop} :

(∀ a b ∈ s, p a b) ↔ (∀ a b, a ∈ s → b ∈ s → p a b) :=

ball_cond_comm

lemma ne_of_apply_ne {α β : Sort*} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=

λ (w : x = y), h (congr_arg f w)

theorem eq_equivalence : equivalence (@eq α) :=

⟨eq.refl, @eq.symm _, @eq.trans _⟩

lemma eq_rec_constant {α : Sort*} {a a' : α} {β : Sort*} (y : β) (h : a = a') :

(@eq.rec α a (λ a, β) y a' h) = y :=

by { cases h, refl, }

lemma eq_mp_eq_cast {α β : Sort*} (h : α = β) : eq.mp h = cast h := rfl

lemma eq_mpr_eq_cast {α β : Sort*} (h : α = β) : eq.mpr h = cast h.symm := rfl

lemma cast_cast : ∀ {α β γ : Sort*} (ha : α = β) (hb : β = γ) (a : α),

cast hb (cast ha a) = cast (ha.trans hb) a

| _ _ _ rfl rfl a := rfl

@[simp] lemma congr_refl_left {α β : Sort*} (f : α → β) {a b : α} (h : a = b) :

congr (eq.refl f) h = congr_arg f h :=

rfl

@[simp] lemma congr_refl_right {α β : Sort*} {f g : α → β} (h : f = g) (a : α) :

congr h (eq.refl a) = congr_fun h a :=

rfl

@[simp] lemma congr_arg_refl {α β : Sort*} (f : α → β) (a : α) :

congr_arg f (eq.refl a) = eq.refl (f a) :=

rfl

@[simp] lemma congr_fun_rfl {α β : Sort*} (f : α → β) (a : α) :

congr_fun (eq.refl f) a = eq.refl (f a) :=

rfl

@[simp] lemma congr_fun_congr_arg {α β γ : Sort*} (f : α → β → γ) {a a' : α} (p : a = a') (b : β) :

congr_fun (congr_arg f p) b = congr_arg (λ a, f a b) p :=

rfl

lemma heq_of_cast_eq :

∀ {α β : Sort*} {a : α} {a' : β} (e : α = β) (h₂ : cast e a = a'), a == a'

| α ._ a a' rfl h := eq.rec_on h (heq.refl _)

lemma cast_eq_iff_heq {α β : Sort*} {a : α} {a' : β} {e : α = β} : cast e a = a' ↔ a == a' :=

⟨heq_of_cast_eq _, λ h, by cases h; refl⟩

lemma rec_heq_of_heq {β} {C : α → Sort*} {x : C a} {y : β} (e : a = b) (h : x == y) :

@eq.rec α a C x b e == y :=

by subst e; exact h

lemma rec_heq_iff_heq {β} {C : α → Sort*} {x : C a} {y : β} {e : a = b} :

@eq.rec α a C x b e == y ↔ x == y :=

by subst e

lemma heq_rec_iff_heq {β} {C : α → Sort*} {x : β} {y : C a} {e : a = b} :

x == @eq.rec α a C y b e ↔ x == y :=

by subst e

protected lemma eq.congr {x₁ x₂ y₁ y₂ : α} (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) :

(x₁ = x₂) ↔ (y₁ = y₂) :=

by { subst h₁, subst h₂ }

lemma eq.congr_left {x y z : α} (h : x = y) : x = z ↔ y = z := by rw [h]

lemma eq.congr_right {x y z : α} (h : x = y) : z = x ↔ z = y := by rw [h]

lemma congr_arg2 {α β γ : Sort*} (f : α → β → γ) {x x' : α} {y y' : β}

(hx : x = x') (hy : y = y') : f x y = f x' y' :=

by { subst hx, subst hy }

variables {β : α → Sort*} {γ : Π a, β a → Sort*} {δ : Π a b, γ a b → Sort*}

lemma congr_fun₂ {f g : Π a b, γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b :=

congr_fun (congr_fun h _) _

lemma congr_fun₃ {f g : Π a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :

f a b c = g a b c :=

congr_fun₂ (congr_fun h _) _ _

lemma funext₂ {f g : Π a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=

funext $ λ _, funext $ h _

lemma funext₃ {f g : Π a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=

funext $ λ _, funext₂ $ h _

end equality

section quantifiers

variables {α : Sort*}

section dependent

variables {β : α → Sort*} {γ : Π a, β a → Sort*} {δ : Π a b, γ a b → Sort*}

{ε : Π a b c, δ a b c → Sort*}

lemma pi_congr {β' : α → Sort*} (h : ∀ a, β a = β' a) : (Π a, β a) = Π a, β' a :=

(funext h : β = β') ▸ rfl

lemma forall₂_congr {p q : Π a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :

(∀ a b, p a b) ↔ ∀ a b, q a b :=

forall_congr $ λ a, forall_congr $ h a

lemma forall₃_congr {p q : Π a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :

(∀ a b c, p a b c) ↔ ∀ a b c, q a b c :=

forall_congr $ λ a, forall₂_congr $ h a

lemma forall₄_congr {p q : Π a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :

(∀ a b c d, p a b c d) ↔ ∀ a b c d, q a b c d :=

forall_congr $ λ a, forall₃_congr $ h a

lemma forall₅_congr {p q : Π a b c d, ε a b c d → Prop}

(h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :

(∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e :=

forall_congr $ λ a, forall₄_congr $ h a

lemma exists₂_congr {p q : Π a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :

(∃ a b, p a b) ↔ ∃ a b, q a b :=

exists_congr $ λ a, exists_congr $ h a

lemma exists₃_congr {p q : Π a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :

(∃ a b c, p a b c) ↔ ∃ a b c, q a b c :=

exists_congr $ λ a, exists₂_congr $ h a

lemma exists₄_congr {p q : Π a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :

(∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d :=

exists_congr $ λ a, exists₃_congr $ h a