@[reducible]

noncomputable def Nonempty.inhabited {α : Type u_4} (h : Nonempty α) : Inhabited α

Equations

• h.inhabited = Classical.inhabited_of_nonempty h

noncomputable def choose? {α : Type u_4} (p : α → Prop) : Option α

Equations

• choose? p = if h : ∃ (x : α), p x then some h.choose else none

noncomputable def idNC {α : Type u_1} (x : α) : α

Equations

• idNC x = Classical.epsilon fun (y : α) => x = y

noncomputable def ite' {α : Type u_1} (p : Prop) (x y : α) : α

Equations

• ite' p x y = if p then x else y

noncomputable def dite' {α : Type u_1} (p : Prop) (f : p → α) (g : ¬p → α) : α

Equations

• dite' p f g = if h : p then f h else g h

class ExiVarC {α : Type u_1} (p : outParam Prop) (q : α → Prop) : Prop

• exi_iff : (∃ (x : α), q x) ↔ p

class AllVarC {α : Type u_1} (p : outParam Prop) (q : α → Prop) : Prop

• all_iff : (∀ (x : α), q x) ↔ p

theorem τ_spec {α : Type u_1} {p : α → Prop} (h : ∃ (y : α), p y) : p (Classical.epsilon p)

theorem hv {α : Type u_4} (x : α) : ∃ (y : α), y = x

theorem ne_of_congr {α : Type u_4} {β : Type u_5} {x y : α} (f : α → β) (h : f x ≠ f y) : x ≠ y

theorem prop_ind (R : Prop → Prop) (h₁ : R True) (h₂ : R False) (P : Prop) : R P

@[simp]

theorem ite_eq {a b : ℕ} : (if a = b then a else b) = b

@[simp]

theorem forall_unit_iff {p : Unit → Prop} : (∀ (u : Unit), p u) ↔ p ()

@[simp]

theorem exi_unit_iff {p : Unit → Prop} : (∃ (u : Unit), p u) ↔ p ()

@[simp]

theorem exi_prop_pos_and {p : Prop → Prop} : (∃ (P : Prop), P ∧ p P) ↔ p True

theorem forall_spec {α : Type u_4} {β : Type u_5} {p : α → Prop} (f : β → α) (h : ∀ (x : α), p x) (y : β) : p (f y)

theorem forall_spec₂ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {p : α → Prop} (f : β → γ → α) (h : ∀ (x : α), p x) (y : β) (z : γ) : p (f y z)

theorem prop_bcs (P : Prop) {R : Prop} (h₁ : P → R) (h₂ : (P → R) → ¬P → R) : R

theorem eq_true_of {P : Prop} (h : P) : P = True

theorem skolemize {α : Type u_4} {β : Type u_5} [hb : Nonempty β] {p : α → Prop} {q : α → β → Prop} : (∀ (x : α), p x → ∃ (y : β), q x y) ↔ ∃ (f : α → β), ∀ (x : α), p x → q x (f x)

theorem skolemize' {α : Type u_4} {β : Type u_5} [hb : Nonempty β] {p : α → β → Prop} : (∀ (x : α), ∃ (y : β), p x y) ↔ ∃ (f : α → β), ∀ (x : α), p x (f x)

theorem and_intro (P : Prop) {Q : Prop} : P ∧ Q → Q

theorem iff_of_and {P Q : Prop} (hp : P) (hq : Q) : P ↔ Q

theorem iff_of_not_and {P Q : Prop} (hp : ¬P) (hq : ¬Q) : P ↔ Q

theorem and_of {P Q : Prop} (h₁ : P) (h₂ : P → Q) : P ∧ Q

theorem iff_of {P Q : Prop} (h₁ : P → Q) (h₂ : (P → Q) → Q → P) : P ↔ Q

theorem not_iff' {P Q : Prop} : ¬(P ↔ Q) ↔ (P ↔ ¬Q)

theorem not_iff_comm' {P Q : Prop} : (¬P ↔ Q) ↔ (P ↔ ¬Q)

theorem imp_cpos {P Q : Prop} : P → Q ↔ ¬Q → ¬P

theorem choose_eq_τ {α : Type u_4} [Nonempty α] {P : α → Prop} (h : ∃ (x : α), P x) : h.choose = Classical.epsilon fun (x : α) => P x

theorem forall_prop_iff {R : Prop → Prop} : (∀ (P : Prop), R P) ↔ R True ∧ R False

theorem exi_prop_iff {R : Prop → Prop} : (∃ (P : Prop), R P) ↔ R True ∨ R False

@[instance_reducible]

def instDecidableForallOfTrueOfFalse_projects {R : Prop → Prop} [ht : Decidable (R True)] [hf : Decidable (R False)] : Decidable (∀ (P : Prop), R P)

Equations

• instDecidableForallOfTrueOfFalse_projects = match h₁ : decide (R True ∧ R False) with | true => isTrue ⋯ | false => isFalse ⋯

@[instance_reducible]

def instDecidableExistsOfTrueOfFalse_projects {R : Prop → Prop} [ht : Decidable (R True)] [hf : Decidable (R False)] : Decidable (∃ (P : Prop), R P)

Equations

• instDecidableExistsOfTrueOfFalse_projects = match h₁ : decide (R True ∨ R False) with | true => isTrue ⋯ | false => isFalse ⋯

theorem not_forall_congr_iff : ¬∀ (α : Type u_4) (P Q : α → Prop), ((∀ (x : α), P x) ↔ ∀ (x : α), Q x) ↔ ∀ (x : α), P x ↔ Q x

theorem not_exi_congr_iff : ¬∀ (α : Type u_4) (P Q : α → Prop), ((∃ (x : α), P x) ↔ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ↔ Q x

theorem heq_fn {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β} {p : γ → Prop} {x : α} {y z : γ} (h : p y ↔ p z) : (fun (x_1 : p y) => f x) ≍ fun (x_1 : p z) => f x

theorem inst_decidable_eq {P : Prop} {H₁ H₂ : Decidable P} : H₁ = H₂

theorem inst_decidablePred_eq {α : Type u_4} {p : α → Prop} {H₁ H₂ : DecidablePred p} : H₁ = H₂

theorem inst_decidableRel_eq {α : Type u_4} {β : Type u_5} {r : α → β → Prop} {H₁ H₂ : DecidableRel r} : H₁ = H₂

theorem inst_decidableEq_eq {α : Type u_4} {H₁ H₂ : DecidableEq α} : H₁ = H₂

theorem forall_iff_of {α : Sort u_4} {p q : α → Prop} (h : ∀ (x : α), p x ↔ q x) : (∀ (x : α), p x) ↔ ∀ (x : α), q x

theorem exists_iff_of {α : Sort u_4} {p q : α → Prop} (h : ∀ (x : α), p x ↔ q x) : (∃ (x : α), p x) ↔ ∃ (x : α), q x

theorem iff_of_isEquiv {α : Type u_4} {r : α → α → Prop} [hr : IsEquiv α r] {a b c d : α} (h₁ : r a c) (h₂ : r b d) : r a b ↔ r c d

theorem not_and_iff_or {P Q : Prop} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

theorem ne_symm' {α : Type u_4} {a b : α} (h : ¬a = b) : ¬b = a

theorem ne_comm' {α : Type u_4} {a b : α} : ¬a = b ↔ ¬b = a

theorem dite_eq_dite_of_pos {α : Type u_4} {P Q : Prop} [hp : Decidable P] [hq : Decidable Q] {f : P → α} {g : Q → α} {x y : α} (h₁ : P) (h₂ : Q) (h₃ : f h₁ = g h₂) : (if h : P then f h else x) = if h : Q then g h else y

theorem choose?_eq_dite {α : Type u_4} {p : α → Prop} : choose? p = if h : ∃ (x : α), p x then some (Classical.epsilon fun (x : α) => p x) else none

theorem choose?_eq_ite {α : Type u_4} {p : α → Prop} [ha : Nonempty α] : choose? p = if ∃ (x : α), p x then some (Classical.epsilon fun (x : α) => p x) else none

theorem choose?_eq_of_exi {α : Type u_4} {p : α → Prop} (h : ∃ (x : α), p x) : choose? p = some (Classical.epsilon fun (x : α) => p x)

theorem choose?_eq_of_pos {α : Type u_4} {p : α → Prop} (h : ∃ (x : α), p x) : choose? p = some (Classical.epsilon fun (x : α) => p x)

@[simp]

theorem choose?_eq_none_iff {α : Type u_4} {p : α → Prop} : choose? p = none ↔ ∀ (x : α), ¬p x

theorem choose?_eq_of_neg {α : Type u_4} {p : α → Prop} (h : ∀ (x : α), ¬p x) : choose? p = none

theorem forall_eq_left_iff_eq_iff {α : Type u_4} {x y : α} : (∀ (z : α), z = x ↔ z = y) ↔ x = y

theorem forall_eq_right_iff_eq_iff {α : Type u_4} {x y : α} : (∀ (z : α), x = z ↔ y = z) ↔ x = y

theorem and_iff_and_of {P Q R S : Prop} (h₁ : P ↔ R) (h₂ : Q ↔ S) : P ∧ Q ↔ R ∧ S

@[simp]

theorem match_decide_eq_dite {α : Type u_4} {P : Prop} [H : Decidable P] {f : decide P = true → α} {g : decide P = false → α} : (match h₁ : decide P with | true => f h₁ | false => g h₁) = if h : P then f ⋯ else g ⋯

@[simp]

theorem match_decide_eq_ite {α : Type u_4} {P : Prop} [H : Decidable P] {x y : α} : (match decide P with | true => x | false => y) = if P then x else y

@[simp]

theorem choose?_eq_some_iff {α : Type u_4} {p : α → Prop} {x : α} : choose? p = some x ↔ p x ∧ (Classical.epsilon fun (x : α) => p x) = x

theorem τ_eq_of_exiu {α : Type u_4} [ha : Nonempty α] {p : α → Prop} {x : α} (h₁ : p x) (h₂ : ∃! x : α, p x) : (Classical.epsilon fun (x : α) => p x) = x

theorem τ_eq_of {α : Type u_4} [ha : Nonempty α] {p : α → Prop} {x : α} (h₁ : p x) (h₂ : ∀ (y : α), p y → y = x) : (Classical.epsilon fun (x : α) => p x) = x

theorem Bool.dite_eq_false_iff {α : Type u_4} {b : Bool} {f : b = false → α} {g : ¬b = false → α} : (if h : b = false then f h else g h) = if h : b = true then g ⋯ else f ⋯

@[simp]

theorem Bool.ite_eq_false_iff {α : Type u_4} {b : Bool} {x y : α} : (if b = false then x else y) = if b = true then y else x

@[simp]

theorem and_not_iff_right_iff {P Q : Prop} : (P ∧ ¬Q ↔ Q) ↔ ¬P ∧ ¬Q

@[simp]

theorem forall_ne_iff_not {α : Type u_4} {p : α → Prop} {x : α} : (∀ (y : α), p y → y ≠ x) ↔ ¬p x

@[simp]

theorem forall_ne_iff_not' {α : Type u_4} {p : α → Prop} {x : α} : (∀ (y : α), p y → x ≠ y) ↔ ¬p x

@[simp]

instance fact_true : Fact True

@[simp]

theorem not_fact_false : ¬Fact False

theorem iff_iff_not' {P Q : Prop} : (P ↔ Q) ↔ (¬P ↔ ¬Q)

theorem imp_iff_not' {P Q : Prop} : P → Q ↔ ¬Q → ¬P

@[instance_reducible]

instance instDecidableOfFact_projects {P : Prop} [H : Fact P] : Decidable P

Equations

• instDecidableOfFact_projects = isTrue ⋯

instance instFact_projects {P : Prop} [H : Fact P] : Fact (Fact P)

theorem eq_iff_and_apply {α : Type u_4} {β : Type u_5} {x y : α} (f : α → β) : x = y ↔ x = y ∧ f x = f y

@[simp]

theorem epsilon_eq_left {α : Type u_4} {x : α} [ha : Nonempty α] : (Classical.epsilon fun (y : α) => y = x) = x

@[simp]

theorem epsilon_eq_right {α : Type u_4} {x : α} [ha : Nonempty α] : (Classical.epsilon fun (y : α) => x = y) = x

@[simp]

theorem iff_not_left_imp_iff {P Q : Prop} : (P ↔ ¬P → Q) ↔ Q → P

@[simp]

theorem not_left_iff_imp_iff {P Q : Prop} : (¬P ↔ P → Q) ↔ Q → ¬P

theorem ne_def {α : Type u_4} {x y : α} : x ≠ y ↔ ¬x = y

theorem setoid_apply_of_eq {α : Type u_1} {s : Setoid α} {x y : α} (h : x = y) : s x y

theorem Equivalence.comm {α : Type u_1} {r : α → α → Prop} {a b : α} (h : Equivalence r) : r a b ↔ r b a

theorem Equivalence.iff_of_left {α : Type u_1} {r : α → α → Prop} {a b c : α} (h₁ : Equivalence r) (h₂ : r a b) : r a c ↔ r b c

theorem Equivalence.iff_of_right {α : Type u_1} {r : α → α → Prop} {a b c : α} (h₁ : Equivalence r) (h₂ : r a b) : r c a ↔ r c b

@[simp]

theorem bif_eq_if {α : Type u_1} {b : Bool} {x y : α} : (bif b then x else y) = if b = true then x else y

@[instance_reducible]

instance instDecidableEqId_projects {α : Type u_1} [ha : DecidableEq α] : DecidableEq (Id α)

Equations

• instDecidableEqId_projects = ha

theorem idNC_def {α : Type u_1} : idNC = fun (x : α) => x

@[instance_reducible, instance 100]

noncomputable instance instInhabitedOfNonempty_projects {α : Type u_4} [ha : Nonempty α] : Inhabited α

Equations

• instInhabitedOfNonempty_projects = Classical.inhabited_of_nonempty ha

theorem ite_eq_ite' {α : Type u_1} {p : Prop} {x y : α} [Decidable p] : (if p then x else y) = ite' p x y

theorem ite'_eq_ite {α : Type u_1} {p : Prop} {x y : α} [Decidable p] : ite' p x y = if p then x else y

@[simp]

theorem ite'_true {α : Type u_1} {x y : α} : ite' True x y = x

@[simp]

theorem ite'_false {α : Type u_1} {x y : α} : ite' False x y = y

@[simp]

theorem ite'_same {α : Type u_1} {p : Prop} {x : α} : ite' p x x = x

theorem dite_eq_dite' {α : Type u_1} {p : Prop} {f : p → α} {g : ¬p → α} [Decidable p] : (if h : p then f h else g h) = dite' p f g

theorem dite'_eq_dite {α : Type u_1} {p : Prop} {f : p → α} {g : ¬p → α} [Decidable p] : dite' p f g = if h : p then f h else g h

@[simp]

theorem dite'_true {α : Type u_1} {f : True → α} {g : ¬True → α} : dite' True f g = f trivial

@[simp]

theorem dite'_false {α : Type u_1} {f : False → α} {g : ¬False → α} : dite' False f g = g not_false

@[simp]

theorem decide_eq_not_decide {p q : Prop} [hp : Decidable p] [hq : Decidable q] : decide p = !decide q ↔ (p ↔ ¬q)

@[simp]

theorem not_decide_eq_decide {p q : Prop} [hp : Decidable p] [hq : Decidable q] : (!decide p) = decide q ↔ (p ↔ ¬q)

theorem choose?_of_pos {α : Type u_1} {P : Option α → Prop} {p : α → Prop} (h₁ : ∃ (x : α), p x) (h₂ : ∀ (x : α), (Classical.epsilon fun (x : α) => p x) = x → p x → P (some x)) : P (choose? p)

theorem choose?_of_neg {α : Type u_1} {P : Option α → Prop} {p : α → Prop} (h₁ : ∀ (x : α), ¬p x) (h₂ : P none) : P (choose? p)

theorem exiu_iff {α : Type u_1} {p : α → Prop} : (∃! x : α, p x) ↔ ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x

theorem not_exiu_iff {α : Type u_1} {p : α → Prop} : (¬∃! x : α, p x) ↔ ∀ (x : α), p x → ∃ (y : α), p y ∧ y ≠ x

theorem not_exiu_iff_or {α : Type u_1} {p : α → Prop} : (¬∃! x : α, p x) ↔ (∀ (x : α), ¬p x) ∨ ∃ (x : α) (y : α), p x ∧ p y ∧ x ≠ y

@[simp]

theorem eq_symm_iff_simp {α : Type u_4} {x y : α} : (x = y ↔ y = x) ↔ True

theorem comm_of_symm {α : Type u_4} {r : α → α → Prop} {x y : α} (h : ∀ {x y : α}, r x y → r y x) : r x y ↔ r y x

theorem dite_true_eq! {α : Type u_1} : @dite α True = fun (x : Decidable True) (f : True → α) (x_1 : ¬True → α) => f trivial

theorem dite_false_eq! {α : Type u_1} : @dite α False = fun (x : Decidable False) (x_1 : False → α) (g : ¬False → α) => g not_false

theorem min_comm! {α : Type u_1} [ha : SemilatticeInf α] : min = fun (x y : α) => y ⊓ x

theorem max_comm! {α : Type u_1} [ha : SemilatticeSup α] : max = fun (x y : α) => y ⊔ x

@[simp]

theorem fmap_Id {α β : Type} {f : α → β} {x : α} : f <$> x = f x

theorem τ_eq_of_ofPred {α : Type u_1} [ha : Nonempty α] {p : α → Prop} {x : α} (h : Set.ofPred p = {x}) : (Classical.epsilon fun (x : α) => p x) = x

@[simp]

theorem or_iff_or_left {p q r : Prop} : (p ∨ q ↔ p ∨ r) ↔ ¬p → (q ↔ r)

@[simp]

theorem or_iff_or_right {p q r : Prop} : (p ∨ q ↔ r ∨ q) ↔ ¬q → (p ↔ r)

@[simp]

theorem imp_not_imp_iff {p q : Prop} : p → ¬p → q ↔ True

@[simp]

theorem not_imp_imp_iff {p q : Prop} : ¬p → p → q ↔ True

theorem ExiVarC.iff {α : Type u_1} {p : Prop} {q : α → Prop} : ExiVarC p q ↔ ((∃ (x : α), q x) ↔ p)

instance instExiVarCAndNonempty {α : Type u_1} {p : Prop} : ExiVarC (p ∧ Nonempty α) fun (x : α) => p

instance instExiVarCTrueEq {α : Type u_1} {y : α} : ExiVarC True fun (x : α) => x = y

instance instExiVarCTrueEq_1 {α : Type u_1} {y : α} : ExiVarC True fun (x : α) => y = x

instance instExiVarCAndEq {α : Type u_1} {p : Prop} {y : α} : ExiVarC p fun (x : α) => p ∧ x = y

instance instExiVarCAndEq_1 {α : Type u_1} {p : Prop} {y : α} : ExiVarC p fun (x : α) => x = y ∧ p

instance instExiVarCOrAndEq {α : Type u_1} {p p' : Prop} {q : α → Prop} {y : α} [h : ExiVarC p q] : ExiVarC (p' ∨ p) fun (x : α) => p' ∧ x = y ∨ q x

instance instExiVarCOrAndEq_1 {α : Type u_1} {p p' : Prop} {q : α → Prop} {y : α} [h : ExiVarC p q] : ExiVarC (p' ∨ p) fun (x : α) => x = y ∧ p' ∨ q x

theorem AllVarC.iff {α : Type u_1} {p : Prop} {q : α → Prop} : AllVarC p q ↔ ((∀ (x : α), q x) ↔ p)

instance instAllVarCOrIsEmpty {α : Type u_1} {p : Prop} : AllVarC (p ∨ IsEmpty α) fun (x : α) => p

instance instAllVarCForallEq {α : Type u_1} {p : Prop} {y : α} : AllVarC p fun (x : α) => x = y → p

instance instAllVarCForallEq_1 {α : Type u_1} {p : Prop} {y : α} : AllVarC p fun (x : α) => y = x → p

instance instAllVarCAndForallEq {α : Type u_1} {p p' : Prop} {q : α → Prop} {y : α} [h : AllVarC p q] : AllVarC (p' ∧ p) fun (x : α) => (x = y → p') ∧ q x

instance instAllVarCAndForallEq_1 {α : Type u_1} {p p' : Prop} {q : α → Prop} {y : α} [h : AllVarC p q] : AllVarC (p' ∧ p) fun (x : α) => (y = x → p') ∧ q x

@[simp]

theorem pairs_eq_simp {α : Type u_1} {β : Type u_2} {x : α} {y : β} {p q : α → β → Prop} : (∀ (x' : α) (y' : β), x' = x ∧ y' = y ∨ p x' y' → q x' y') ↔ q x y ∧ ∀ (x' : α) (y' : β), p x' y' → q x' y'

@[simp]

theorem imp_and_eq_left_simp {α : Type u_1} {y : α} {p q : α → Prop} : (∀ (x : α), (x = y → p x) ∧ q x) ↔ p y ∧ ∀ (x : α), q x

@[simp]

theorem imp_and_eq_right_simp {α : Type u_1} {y : α} {p q : α → Prop} : (∀ (x : α), (y = x → p x) ∧ q x) ↔ p y ∧ ∀ (x : α), q x

theorem Acc.of_isEmpty {α : Type u_1} [ha : IsEmpty α] {r : α → α → Prop} {x : α} : Acc r x

theorem WellFounded.of_isEmpty {α : Type u_1} [ha : IsEmpty α] {r : α → α → Prop} : WellFounded r

theorem Relation.TransGen.lt_of_le_of_lt {α : Type u_1} {r : α → α → Prop} {a c : α} (b : α) (h₁ : a = b ∨ TransGen r a b) (h₂ : TransGen r b c) : TransGen r a c

theorem Relation.TransGen.lt_of_lt_of_le {α : Type u_1} {r : α → α → Prop} {a c : α} (b : α) (h₁ : TransGen r a b) (h₂ : b = c ∨ TransGen r b c) : TransGen r a c

theorem imp_comm_left {a b c : Prop} : a → b → c ↔ b → a → c

theorem imp_and_of {p q r : Prop} (h₁ : p) (h₂ : p → q) (h₃ : p → q → r) : (p → q) ∧ r

theorem imp_fn_and_of {α : Type u_1} {β : Type u_2} {x : Option (α → β)} {y z : α → β} {r : α → Prop} (h₁ : x = some y) (h₂ : ∀ (w : α), z w = y w) (h₃ : x = some z → ∀ (w : α), r w) (w : α) : (x = some y → z w = y w) ∧ r w

theorem forall_and_true {α : Type u_1} {p : α → Prop} (h : ∀ (x : α), p x ∧ True) (x : α) : p x

@[simp]

theorem decide_decidable_of_bool_eq_true_eq {p : Prop} {b : Bool} {h : b = true ↔ p} : (decide p = true) = (b = true)

@[simp]

theorem decide_decidable_of_bool_eq_false_eq {p : Prop} {b : Bool} {h : b = true ↔ p} : (decide p = false) = ((!b) = true)

@[simp]

theorem ite_eq_ite_iff {α : Type u_1} {p : Prop} [hp₁ : Decidable p] [hp₂ : Decidable p] {a b c d : α} : ((if p then a else b) = if p then c else d) ↔ if p then a = c else b = d

theorem forall_imp_of_forall {α : Type u_1} {p : α → Prop} (q : α → Prop) (h : ∀ (x : α), p x) (x : α) : q x → p x