[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
⊢ disjointed ≤ id
[PROOFSTEP]
rintro f n
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n ≤ id f n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero ≤ id f Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) ≤ id f (Nat.succ n✝)
[PROOFSTEP]
exact sdiff_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ Pairwise (Disjoint on disjointed f)
[PROOFSTEP]
refine' (Symmetric.pairwise_on Disjoint.symm _).2 fun m n h => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m n : ℕ
h : m < n
⊢ Disjoint (disjointed f m) (disjointed f n)
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m : ℕ
h : m < Nat.zero
⊢ Disjoint (disjointed f m) (disjointed f Nat.zero)
[PROOFSTEP]
exact (Nat.not_lt_zero _ h).elim
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m n✝ : ℕ
h : m < Nat.succ n✝
⊢ Disjoint (disjointed f m) (disjointed f (Nat.succ n✝))
[PROOFSTEP]
exact disjoint_sdiff_self_right.mono_left ((disjointed_le f m).trans (le_partialSups_of_le f (Nat.lt_add_one_iff.1 h)))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (disjointed f (n + 1))
[PROOFSTEP]
suffices H : ∀ k, p (f (n + 1) \ partialSups f k)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
H : (k : ℕ) → p (f (n + 1) \ ↑(partialSups f) k)
⊢ p (disjointed f (n + 1))
[PROOFSTEP]
exact H n
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ (k : ℕ) → p (f (n + 1) \ ↑(partialSups f) k)
[PROOFSTEP]
rintro k
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
⊢ p (f (n + 1) \ ↑(partialSups f) k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case H.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (f (n + 1) \ ↑(partialSups f) Nat.zero)
[PROOFSTEP]
exact hdiff h
[GOAL]
case H.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
ih : p (f (n + 1) \ ↑(partialSups f) k)
⊢ p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
[PROOFSTEP]
rw [partialSups_succ, ← sdiff_sdiff_left]
[GOAL]
case H.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
ih : p (f (n + 1) \ ↑(partialSups f) k)
⊢ p ((f (n + 1) \ ↑(partialSups f) k) \ f (k + 1))
[PROOFSTEP]
exact hdiff ih
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
hf : Monotone f
n : ℕ
⊢ disjointed f (n + 1) = f (n + 1) \ f n
[PROOFSTEP]
rw [disjointed_succ, hf.partialSups_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ partialSups (disjointed f) = partialSups f
[PROOFSTEP]
ext n
[GOAL]
case h.h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups (disjointed f)) n = ↑(partialSups f) n
[PROOFSTEP]
induction' n with k ih
[GOAL]
case h.h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ ↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
[PROOFSTEP]
rw [partialSups_zero, partialSups_zero, disjointed_zero]
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
k : ℕ
ih : ↑(partialSups (disjointed f)) k = ↑(partialSups f) k
⊢ ↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
[PROOFSTEP]
rw [partialSups_succ, partialSups_succ, disjointed_succ, ih, sup_sdiff_self_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d = disjointed f
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d n = disjointed f n
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d Nat.zero = disjointed f Nat.zero
[PROOFSTEP]
rw [← partialSups_zero d, hsups, partialSups_zero, disjointed_zero]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
[PROOFSTEP]
suffices h : d n.succ = partialSups d n.succ \ partialSups d n
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
[PROOFSTEP]
rw [h, hsups, partialSups_succ, disjointed_succ, sup_sdiff, sdiff_self, bot_sup_eq]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
[PROOFSTEP]
rw [partialSups_succ, sup_sdiff, sdiff_self, bot_sup_eq, eq_comm, sdiff_eq_self_iff_disjoint]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
[PROOFSTEP]
suffices h : ∀ m ≤ n, Disjoint (partialSups d m) (d n.succ)
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
[PROOFSTEP]
exact h n le_rfl
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
[PROOFSTEP]
rintro m hm
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm : m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
[PROOFSTEP]
induction' m with m ih
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm✝ : m ≤ n
hm : Nat.zero ≤ n
⊢ Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
[PROOFSTEP]
exact hdisj (Nat.succ_ne_zero _).symm
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
[PROOFSTEP]
rw [partialSups_succ, disjoint_iff, inf_sup_right, sup_eq_bot_iff, ← disjoint_iff, ← disjoint_iff]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
[PROOFSTEP]
exact ⟨ih (Nat.le_of_succ_le hm), hdisj (Nat.lt_succ_of_le hm).ne⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n = f n ⊓ ⨅ (i : ℕ) (_ : i < n), (f i)ᶜ
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero = f Nat.zero ⊓ ⨅ (i : ℕ) (_ : i < Nat.zero), (f i)ᶜ
[PROOFSTEP]
rw [disjointed_zero, eq_comm, inf_eq_left]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ f Nat.zero ≤ ⨅ (i : ℕ) (_ : i < Nat.zero), (f i)ᶜ
[PROOFSTEP]
simp_rw [le_iInf_iff]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ ∀ (i : ℕ), i < Nat.zero → f Nat.zero ≤ (f i)ᶜ
[PROOFSTEP]
exact fun i hi => (i.not_lt_zero hi).elim
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
simp_rw [disjointed_succ, partialSups_eq_biSup, sdiff_eq, compl_iSup]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ f (n✝ + 1) ⊓ ⨅ (i : ℕ) (_ : i ≤ n✝), (f i)ᶜ = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
congr
[GOAL]
case succ.e_a.e_s
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (fun i => ⨅ (_ : i ≤ n✝), (f i)ᶜ) = fun i => ⨅ (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
ext i
[GOAL]
case succ.e_a.e_s.h
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ i : ℕ
⊢ ⨅ (_ : i ≤ n✝), (f i)ᶜ = ⨅ (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
rw [Nat.lt_succ_iff]
[GOAL]
α : Type u_1
β : Type u_2
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
⊢ (fun x => Nat.find (_ : ∃ n, x ∈ s n)) ⁻¹' {n} = disjointed s n
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ x ∈ (fun x => Nat.find (_ : ∃ n, x ∈ s n)) ⁻¹' {n} ↔ x ∈ disjointed s n
[PROOFSTEP]
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]


[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b c d : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a
[PROOFSTEP]
rwa [← h] at hab
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c d : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
[PROOFSTEP]
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, inf_assoc]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c d : α
⊢ Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
[PROOFSTEP]
simp_rw [disjoint_iff_inf_le, inf_left_comm]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c d : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
[PROOFSTEP]
simp_rw [disjoint_iff_inf_le, inf_right_comm]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
[PROOFSTEP]
simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
[PROOFSTEP]
simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ b ⊔ c
[PROOFSTEP]
rwa [sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a b c d : α
ha : a ≠ ⊤
hab : Codisjoint a b
h : a = b
⊢ Codisjoint a a
[PROOFSTEP]
rwa [← h] at hab
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c
[PROOFSTEP]
simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c
[PROOFSTEP]
simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c
[PROOFSTEP]
rwa [inf_comm]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c
[PROOFSTEP]
rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)
[PROOFSTEP]
exact inf_le_inf_right _ le_sup_left
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x
[PROOFSTEP]
rw [h.symm.inf_eq_bot, sup_bot_eq]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
[PROOFSTEP]
rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z
[PROOFSTEP]
rw [disjoint_iff]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
[PROOFSTEP]
exact h.inf_left_eq_bot_iff
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
[PROOFSTEP]
rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm, h'.inf_eq_bot, inf_bot_eq]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
[PROOFSTEP]
rw [sup_inf_left, @sup_comm _ _ x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq, sup_assoc, sup_left_comm,
  h'.sup_eq_top, sup_top_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
[PROOFSTEP]
refine' ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, _⟩ ⟨hy, _⟩).1, fun b hx hy ↦ (@h (⊥, b) ⟨_, hx⟩ ⟨_, hy⟩).2⟩
[GOAL]
case mp.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd
case mp.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd
case mp.refine'_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst
case mp.refine'_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst
[PROOFSTEP]
all_goals exact bot_le
[GOAL]
case mp.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd
[PROOFSTEP]
exact bot_le
[GOAL]
case mp.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd
[PROOFSTEP]
exact bot_le
[GOAL]
case mp.refine'_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst
[PROOFSTEP]
exact bot_le
[GOAL]
case mp.refine'_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst
[PROOFSTEP]
exact bot_le
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y
[PROOFSTEP]
rintro ⟨ha, hb⟩ z hza hzb
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥
[PROOFSTEP]
refine' ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
[PROOFSTEP]
simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ≤ ↑b ↔ a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint ↑a ↑b ↔ Disjoint a b
[PROOFSTEP]
rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Codisjoint ↑a ↑b ↔ Codisjoint a b
[PROOFSTEP]
rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b
[PROOFSTEP]
simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]


[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
⊢ Function.Injective fun c => ↑c.toOrderHom
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝¹ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝¹ x
idempotent'✝¹ : ∀ (x : α), OrderHom.toFun toOrderHom✝¹ (OrderHom.toFun toOrderHom✝¹ x) = OrderHom.toFun toOrderHom✝¹ x
toOrderHom✝ : α →o α
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝ x
idempotent'✝ : ∀ (x : α), OrderHom.toFun toOrderHom✝ (OrderHom.toFun toOrderHom✝ x) = OrderHom.toFun toOrderHom✝ x
h :
  (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
⊢ { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toOrderHom
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝¹ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝¹ x
idempotent'✝¹ : ∀ (x : α), OrderHom.toFun toOrderHom✝¹ (OrderHom.toFun toOrderHom✝¹ x) = OrderHom.toFun toOrderHom✝¹ x
toOrderHom✝ : α →o α
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝ x
idempotent'✝ : ∀ (x : α), OrderHom.toFun toOrderHom✝ (OrderHom.toFun toOrderHom✝ x) = OrderHom.toFun toOrderHom✝ x
h :
  (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
⊢ toOrderHom✝¹ = toOrderHom✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
c₁ : α → α
monotone'✝¹ : Monotone c₁
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x
idempotent'✝¹ :
  ∀ (x : α),
    OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ }
        (OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x) =
      OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x
c₂ : α → α
monotone'✝ : Monotone c₂
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x
idempotent'✝ :
  ∀ (x : α),
    OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ }
        (OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x) =
      OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x
h :
  ↑{ toOrderHom := { toFun := c₁, monotone' := monotone'✝¹ }, le_closure' := le_closure'✝¹,
        idempotent' := idempotent'✝¹ } =
    ↑{ toOrderHom := { toFun := c₂, monotone' := monotone'✝ }, le_closure' := le_closure'✝,
        idempotent' := idempotent'✝ }
⊢ { toOrderHom := { toFun := c₁, monotone' := monotone'✝¹ }, le_closure' := le_closure'✝¹,
      idempotent' := idempotent'✝¹ } =
    { toOrderHom := { toFun := c₂, monotone' := monotone'✝ }, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ Set.range ↑c → x ∈ closed c
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ ↑c y ∈ closed c
[PROOFSTEP]
apply c.idempotent
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x y : α
hy : closed c y
⊢ ↑c x ≤ y ↔ x ≤ y
[PROOFSTEP]
rw [← c.closure_eq_self_of_mem_closed hy, ← le_closure_iff]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c✝ c : ClosureOperator α
⊢ c =
    mk₃ (↑c) (closed c) (_ : ∀ (x : α), x ≤ ↑c x) (_ : ∀ (x : α), ↑c x ∈ closed c)
      (_ : ∀ (x y : α), x ≤ y → closed c y → ↑c x ≤ y)
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c✝ c : ClosureOperator α
x✝ : α
⊢ ↑c x✝ =
    ↑(mk₃ (↑c) (closed c) (_ : ∀ (x : α), x ≤ ↑c x) (_ : ∀ (x : α), ↑c x ∈ closed c)
          (_ : ∀ (x y : α), x ≤ y → closed c y → ↑c x ≤ y))
      x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ ↑c (x ⊔ ↑c y) = ↑c (x ⊔ y)
[PROOFSTEP]
rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ ↑c (↑c x ⊔ ↑c y) = ↑c (x ⊔ y)
[PROOFSTEP]
rw [closure_sup_closure_left, closure_sup_closure_right]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
u : β → α
l : LowerAdjoint u
l₁ : α → β
gc'✝¹ : GaloisConnection l₁ u
l₂ : α → β
gc'✝ : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc'✝¹ }.toFun = { toFun := l₂, gc' := gc'✝ }.toFun
⊢ { toFun := l₁, gc' := gc'✝¹ } = { toFun := l₂, gc' := gc'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ x ∈ toFun l s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ toFun l {x} ≤ toFun l s ↔ ∀ (S : α), toFun l s ≤ S → toFun l {x} ≤ S
[PROOFSTEP]
exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
x y : α
⊢ toFun l (↑(toFun l ↑x) ∪ ↑(toFun l ↑y)) = toFun l (↑x ∪ ↑y)
[PROOFSTEP]
rw [closure_union_closure_right, closure_union_closure_left]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val) = c
[PROOFSTEP]
ext x
[GOAL]
case a.h
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ↑(GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val)) x = ↑c x
[PROOFSTEP]
rfl


[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
by_cases H : ∀ a : α, ∃ b, ¬b ≤ a
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
exact PSum.inr ⟨H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ¬∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
push_neg at H
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
letI : Top α := ⟨Classical.choose H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
this : Top α := { top := Classical.choose H }
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
exact PSum.inl ⟨Classical.choose_spec H⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ f a
[PROOFSTEP]
rw [h_top]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case refl
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
[PROOFSTEP]
apply top_unique
[GOAL]
case refl.h
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤
[PROOFSTEP]
exact @le_top _ _ A _
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : OrderTop α
⊢ A = B
[PROOFSTEP]
rcases A with ⟨ha⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : OrderTop α
toTop✝ : Top α
ha : ∀ (a : α), a ≤ ⊤
⊢ mk ha = B
[PROOFSTEP]
rcases B with ⟨hb⟩
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ mk ha = mk hb
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toTop
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ toTop✝¹ = toTop✝
[PROOFSTEP]
ext
[GOAL]
case mk.mk.e_toTop.top
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ ⊤ = ⊤
[PROOFSTEP]
exact le_antisymm (hb _) (ha _)
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
by_cases H : ∀ a : α, ∃ b, ¬a ≤ b
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
exact PSum.inr ⟨H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ¬∀ (a : α), ∃ b, ¬a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
push_neg at H
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
letI : Bot α := ⟨Classical.choose H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), a ≤ b
this : Bot α := { bot := Classical.choose H }
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
exact PSum.inl ⟨Classical.choose_spec H⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p
[PROOFSTEP]
rw [h_bot]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p
[PROOFSTEP]
exact bot_le
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A : OrderBot α
hB : PartialOrder α
B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case refl
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
[PROOFSTEP]
apply bot_unique
[GOAL]
case refl.h
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥
[PROOFSTEP]
exact @bot_le _ _ A _
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : OrderBot α
⊢ A = B
[PROOFSTEP]
rcases A with ⟨ha⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : OrderBot α
toBot✝ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = B
[PROOFSTEP]
rcases B with ⟨hb⟩
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = mk hb
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toBot
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ toBot✝¹ = toBot✝
[PROOFSTEP]
ext
[GOAL]
case mk.mk.e_toBot.bot
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ ⊥ = ⊥
[PROOFSTEP]
exact le_antisymm (ha _) (hb _)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
[PROOFSTEP]
rw [eq_bot_iff, sup_le_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
⊢ A = B
[PROOFSTEP]
have ht : @BoundedOrder.toOrderTop α _ A = @BoundedOrder.toOrderTop α _ B := OrderTop.ext
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
⊢ A = B
[PROOFSTEP]
have hb : @BoundedOrder.toOrderBot α _ A = @BoundedOrder.toOrderBot α _ B := OrderBot.ext
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : BoundedOrder α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = mk
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤
[PROOFSTEP]
rw [map_top]
  -- Porting note: lean3 didn't need the type annotation
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤
[PROOFSTEP]
exact @le_top β _ _ _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Bot α
inst✝¹ : LE β
inst✝ : OrderBot β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_bot : f ⊥ = ⊥
a : α
⊢ f ⊥ ≤ f a
[PROOFSTEP]
rw [map_bot]
  -- Porting note: lean3 didn't need the type annotation
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Bot α
inst✝¹ : LE β
inst✝ : OrderBot β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_bot : f ⊥ = ⊥
a : α
⊢ ⊥ ≤ f a
[PROOFSTEP]
exact @bot_le β _ _ _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥
[PROOFSTEP]
rw [← coe_bot hbot, ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : OrderTop (Subtype p)
htop : p ⊤
x : { x // p x }
⊢ ↑x = ⊤ ↔ x = ⊤
[PROOFSTEP]
rw [← coe_top htop, ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
[PROOFSTEP]
simp only [← inf_eq_min, ← le_bot_iff, inf_le_iff]