[GOAL]
P : Type u_1
inst✝ : LE P
I J s✝ t✝ : Ideal P
x y : P
s t : Ideal P
x✝ : s.toLowerSet = t.toLowerSet
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
P : Type u_1
inst✝ : LE P
I J s t✝ : Ideal P
x y : P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
P : Type u_1
inst✝ : LE P
I J s t : Ideal P
x y : P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : Set.Nonempty toLowerSet✝¹.carrier
directed'✝¹ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }
[PROOFSTEP]
congr
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
⊢ False
[PROOFSTEP]
have := mem_univ p
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ univ
⊢ False
[PROOFSTEP]
rw [← hp] at this
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False
[PROOFSTEP]
exact nmem this
[GOAL]
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨a, ha⟩ := I.nonempty
[GOAL]
case intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨b, hb⟩ := J.nonempty
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨c, hac, hbc⟩ := exists_le_le a b
[GOAL]
case intro.intro.intro.intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
exact ⟨c, I.lower hac ha, J.lower hbc hb⟩
[GOAL]
P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirected P fun x x_1 => x ≤ x_1
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
src✝ : IsProper I := IsCoatom.isProper hI
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ
[PROOFSTEP]
simp [hI.2 _ hJ]
[GOAL]
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
⊢ I = ⊤
[PROOFSTEP]
ext
[GOAL]
case a.h
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
x✝ : P
⊢ x✝ ∈ ↑I ↔ x✝ ∈ ↑⊤
[PROOFSTEP]
exact iff_of_true (I.lower le_top h) trivial
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
inst✝ : OrderBot P
⊢ ∀ (a : Ideal P), ⊥ ≤ a
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x✝ : P
I✝ J✝ K s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I✝ J✝ K s t I J : Ideal P
⊢ Set.Nonempty
    { carrier := {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j},
        lower' :=
          (_ :
            ∀ (x y : P),
              y ≤ x →
                x ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j} → y ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j}) }.carrier
[PROOFSTEP]
cases' inter_nonempty I J with w h
[GOAL]
case intro
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I✝ J✝ K s t I J : Ideal P
w : P
h : w ∈ ↑I ∩ ↑J
⊢ Set.Nonempty
    { carrier := {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j},
        lower' :=
          (_ :
            ∀ (x y : P),
              y ≤ x →
                x ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j} → y ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j}) }.carrier
[PROOFSTEP]
exact ⟨w, w, h.1, w, h.2, le_sup_left⟩
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I J K s t : Ideal P
hx : ¬x ∈ I
h : I = I ⊔ principal x
⊢ x ∈ I
[PROOFSTEP]
simpa only [left_eq_sup, principal_le_iff] using h
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ ⊥ ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
[PROOFSTEP]
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ ∀ (i : Ideal P), i ∈ S → ⊥ ∈ ↑i.toLowerSet
[PROOFSTEP]
exact fun s _ ↦ s.bot_mem
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
a : P
ha : a ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
b : P
hb : b ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
⊢ a ⊔ b ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
[PROOFSTEP]
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂] at ha hb ⊢
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
a : P
ha : ∀ (i : Ideal P), i ∈ S → a ∈ ↑i.toLowerSet
b : P
hb : ∀ (i : Ideal P), i ∈ S → b ∈ ↑i.toLowerSet
⊢ ∀ (i : Ideal P), i ∈ S → a ⊔ b ∈ ↑i.toLowerSet
[PROOFSTEP]
exact fun s hs ↦ sup_mem (ha _ hs) (hb _ hs)
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ (s : Ideal P), s ∈ S → x ∈ s
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
⊢ IsGLB S (sInf S)
[PROOFSTEP]
refine' ⟨fun s hs ↦ _, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ s ≤ sInf S
[PROOFSTEP]
rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ sInf S ≤ s
[PROOFSTEP]
rw [← coe_subset_coe, coe_sInf]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ ⋂ (s : Ideal P) (_ : s ∈ S), ↑s ⊆ ↑s
[PROOFSTEP]
exact biInter_subset_of_mem hs
[GOAL]
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i', i' ∈ I ∧ ∃ j', j' ∈ J ∧ x = i' ⊔ j'
[PROOFSTEP]
refine' ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, _⟩
[GOAL]
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j
[PROOFSTEP]
calc
  x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
  _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
⊢ ¬x ∈ I
[PROOFSTEP]
intro hx
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
[PROOFSTEP]
apply hI.top_not_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I
[PROOFSTEP]
have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I
[PROOFSTEP]
rwa [sup_compl_eq_top] at ht
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
[PROOFSTEP]
have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
h : xᶜ ∈ I → ¬x ∈ I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
[PROOFSTEP]
tauto
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)
[PROOFSTEP]
apply monotone_nat_of_le_succ
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
[PROOFSTEP]
intro n
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
[PROOFSTEP]
dsimp only [sequenceOfCofinals, Nat.add]
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
cases (Encodable.decode n : Option ι)
[GOAL]
case hf.none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
rfl
[GOAL]
case hf.some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
apply Cofinal.le_above
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
[PROOFSTEP]
dsimp only [sequenceOfCofinals, Nat.add]
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
[PROOFSTEP]
rw [Encodable.encodek]
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
[PROOFSTEP]
apply Cofinal.above_mem


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt a
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
x✝ : α × β
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
x✝ : α × β
a : α
b c : β
h : b < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt a
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b c : β
h : c < b
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, a < b
[PROOFSTEP]
classical
obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
exact ⟨_, lt_update_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : a (Classical.arbitrary ι) < b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨_, lt_update_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a
[PROOFSTEP]
classical
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
exact ⟨_, update_lt_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨_, update_lt_self_iff.2 hb⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a
[PROOFSTEP]
simpa [not_le] using exists_not_ge a
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoTopOrder α
a : α
⊢ ∃ b, a < b
[PROOFSTEP]
simpa [not_le] using exists_not_le a
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬IsMin a ↔ ∃ b, b < a
[PROOFSTEP]
simp [lt_iff_le_not_le, IsMin, not_forall, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬IsMax a ↔ ∃ b, a < b
[PROOFSTEP]
simp [lt_iff_le_not_le, IsMax, not_forall, exists_prop]


[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
[PROOFSTEP]
rw [inf_comm, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a
[PROOFSTEP]
exact fun ha hb => covby_sup_of_inf_covby_of_inf_covby_left hb ha
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
[PROOFSTEP]
rw [sup_comm, inf_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b
[PROOFSTEP]
exact fun ha hb => inf_covby_of_covby_sup_of_covby_sup_left hb ha
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b
[PROOFSTEP]
rw [sup_comm, inf_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ b → a ⋖ b ⊔ a
[PROOFSTEP]
exact covby_sup_of_inf_covby_left
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ a ⊔ b → a ⊓ b ⋖ a
[PROOFSTEP]
rw [inf_comm, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ b ⊔ a → b ⊓ a ⋖ a
[PROOFSTEP]
exact inf_covby_of_covby_sup_left
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
h : z ≤ x
⊢ x ⊓ y ⊔ z = x ⊓ (y ⊔ z)
[PROOFSTEP]
rw [inf_comm, sup_comm, ← sup_inf_assoc_of_le y h, inf_comm, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z = x✝ ⊔ y ⊓ z
[PROOFSTEP]
rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ z ⊓ y ⊔ x✝ = z ⊓ (y ⊔ x✝)
[PROOFSTEP]
exact @sup_inf_assoc_of_le α _ _ _ y _ xz
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
h : y ≤ x ⊔ z
⊢ z ⊓ y ≤ z ⊓ x
[PROOFSTEP]
rw [inf_comm, @inf_comm _ _ z]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
h : y ≤ x ⊔ z
⊢ y ⊓ z ≤ x ⊓ z
[PROOFSTEP]
exact hinf
[GOAL]
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (f₂ A, g₂ A) (f₂ B, g₂ B)
[PROOFSTEP]
simp only [Prod.lex_def, lt_iff_le_not_le, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg, le_antisymm_iff]
[GOAL]
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K ≤ B ⊓ K ∧ ¬B ⊓ K ≤ A ⊓ K ∨ (A ⊓ K ≤ B ⊓ K ∧ B ⊓ K ≤ A ⊓ K) ∧ A ⊔ K ≤ B ⊔ K ∧ ¬B ⊔ K ≤ A ⊔ K
[PROOFSTEP]
simp only [gci.l_le_l_iff, gi.u_le_u_iff, ← lt_iff_le_not_le, ← le_antisymm_iff]
[GOAL]
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
[PROOFSTEP]
cases' lt_or_eq_of_le (inf_le_inf_right K (le_of_lt hAB)) with h h
[GOAL]
case inl
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K < B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
[PROOFSTEP]
exact Or.inl h
[GOAL]
case inr
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K = B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
[PROOFSTEP]
exact Or.inr ⟨h, sup_lt_sup_of_lt_of_inf_le_inf hAB (le_of_eq h.symm)⟩
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ ↑((fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) })
        ((fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) }) x)) =
    ↑x
[PROOFSTEP]
change a ⊓ (↑x ⊔ b) = ↑x
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ a ⊓ (↑x ⊔ b) = ↑x
[PROOFSTEP]
rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ ↑((fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) })
        ((fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) }) x)) =
    ↑x
[PROOFSTEP]
change a ⊓ ↑x ⊔ b = ↑x
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ a ⊓ ↑x ⊔ b = ↑x
[PROOFSTEP]
rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
⊢ ↑{ toFun := fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) },
            invFun := fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Icc (a ⊓ b) a)),
                  (fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) })
                      ((fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) }) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Icc b (a ⊔ b))),
                  (fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) })
                      ((fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) }) x) =
                    x) }
        x ≤
      ↑{ toFun := fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) },
            invFun := fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Icc (a ⊓ b) a)),
                  (fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) })
                      ((fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) }) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Icc b (a ⊔ b))),
                  (fun x => { val := ↑x ⊔ b, property := (_ : b ≤ ↑x ⊔ b ∧ ↑x ⊔ b ≤ a ⊔ b) })
                      ((fun x => { val := a ⊓ ↑x, property := (_ : a ⊓ b ≤ a ⊓ ↑x ∧ a ⊓ ↑x ≤ a) }) x) =
                    x) }
        y ↔
    x ≤ y
[PROOFSTEP]
simp only [Subtype.mk_le_mk, Equiv.coe_fn_mk, and_true_iff, le_sup_right]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
⊢ ↑x ⊔ b ≤ ↑y ⊔ b ↔ x ≤ y
[PROOFSTEP]
rw [← Subtype.coe_le_coe]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
⊢ ↑x ⊔ b ≤ ↑y ⊔ b ↔ ↑x ≤ ↑y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => sup_le_sup_right h _⟩
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ ↑x ≤ ↑y
[PROOFSTEP]
rw [← sup_eq_right.2 x.prop.1, inf_sup_assoc_of_le _ x.prop.2, sup_comm, ← sup_eq_right.2 y.prop.1,
  inf_sup_assoc_of_le _ y.prop.2, @sup_comm _ _ b]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (↑x ⊔ b) ≤ a ⊓ (↑y ⊔ b)
[PROOFSTEP]
exact inf_le_inf_left _ h
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ ↑((fun c => { val := a ⊓ ↑c, property := (_ : a ⊓ b < a ⊓ ↑c ∧ a ⊓ ↑c < a) })
        ((fun c => { val := ↑c ⊔ b, property := (_ : b < ↑c ⊔ b ∧ ↑c ⊔ b < a ⊔ b) }) c)) =
    ↑c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ a ⊓ (↑c ⊔ b) = ↑c
[PROOFSTEP]
rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo b (a ⊔ b))
⊢ ↑((fun c => { val := ↑c ⊔ b, property := (_ : b < ↑c ⊔ b ∧ ↑c ⊔ b < a ⊔ b) })
        ((fun c => { val := a ⊓ ↑c, property := (_ : a ⊓ b < a ⊓ ↑c ∧ a ⊓ ↑c < a) }) c)) =
    ↑c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo b (a ⊔ b))
⊢ a ⊓ ↑c ⊔ b = ↑c
[PROOFSTEP]
rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⋖ a ⊔ b → a ⊓ b ⋖ b
[PROOFSTEP]
simp_rw [covby_iff_Ioo_eq, @sup_comm _ _ a, @inf_comm _ _ a, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
  (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b) → ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b)
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b
[PROOFSTEP]
simp_rw [covby_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
  (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]
[GOAL]
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b)) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z
[PROOFSTEP]
rw [← inf_eq_left.2 xz, h]
[GOAL]
α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z
[PROOFSTEP]
rw [inf_sup_right, inf_eq_left.2 xz]
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)
[PROOFSTEP]
rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b
[PROOFSTEP]
apply le_inf inf_le_left
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b
[PROOFSTEP]
apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.28074 ⊔ a) ⊓ (c ⊔ b) ≤ b
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ α
[PROOFSTEP]
rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c
[PROOFSTEP]
rw [disjoint_comm, sup_comm]
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)
[PROOFSTEP]
apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
[GOAL]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
[PROOFSTEP]
rwa [sup_comm, disjoint_comm] at hsup
[GOAL]
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ IsCompl { val := x, property := hx } { val := y ⊓ a, property := (_ : y ⊓ a ∈ Iic a) }
[PROOFSTEP]
constructor
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ Disjoint { val := x, property := hx } { val := y ⊓ a, property := (_ : y ⊓ a ∈ Iic a) }
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ { val := x, property := hx } ⊓ { val := y ⊓ a, property := (_ : y ⊓ a ∈ Iic a) } ≤ ⊥
[PROOFSTEP]
change
  x ⊓ (y ⊓ a) ≤
    ⊥
      -- improve lattice subtype API
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ x ⊓ (y ⊓ a) ≤ ⊥
[PROOFSTEP]
rw [← inf_assoc]
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ x ⊓ y ⊓ a ≤ ⊥
[PROOFSTEP]
exact le_trans inf_le_left hy.1.le_bot
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ Codisjoint { val := x, property := hx } { val := y ⊓ a, property := (_ : y ⊓ a ∈ Iic a) }
[PROOFSTEP]
rw [codisjoint_iff_le_sup]
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ ⊤ ≤ { val := x, property := hx } ⊔ { val := y ⊓ a, property := (_ : y ⊓ a ∈ Iic a) }
[PROOFSTEP]
change a ≤ x ⊔ y ⊓ a
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
y : α
hy : IsCompl x y
⊢ a ≤ x ⊔ y ⊓ a
[PROOFSTEP]
rw [← sup_inf_assoc_of_le _ (Set.mem_Iic.1 hx), hy.2.eq_top, top_inf_eq]
[GOAL]
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ IsCompl { val := x, property := hx } { val := y ⊔ a, property := (_ : y ⊔ a ∈ Ici a) }
[PROOFSTEP]
constructor
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ Disjoint { val := x, property := hx } { val := y ⊔ a, property := (_ : y ⊔ a ∈ Ici a) }
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ { val := x, property := hx } ⊓ { val := y ⊔ a, property := (_ : y ⊔ a ∈ Ici a) } ≤ ⊥
[PROOFSTEP]
change x ⊓ (y ⊔ a) ≤ a
[GOAL]
case disjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ x ⊓ (y ⊔ a) ≤ a
[PROOFSTEP]
rw [← inf_sup_assoc_of_le _ (Set.mem_Ici.1 hx), hy.1.eq_bot, bot_sup_eq]
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ Codisjoint { val := x, property := hx } { val := y ⊔ a, property := (_ : y ⊔ a ∈ Ici a) }
[PROOFSTEP]
rw [codisjoint_iff_le_sup]
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ ⊤ ≤ { val := x, property := hx } ⊔ { val := y ⊔ a, property := (_ : y ⊔ a ∈ Ici a) }
[PROOFSTEP]
change
  ⊤ ≤
    x ⊔
      (y ⊔ a)
        -- improve lattice subtype API
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ ⊤ ≤ x ⊔ (y ⊔ a)
[PROOFSTEP]
rw [← sup_assoc]
[GOAL]
case codisjoint
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
y : α
hy : IsCompl x y
⊢ ⊤ ≤ x ⊔ y ⊔ a
[PROOFSTEP]
exact le_trans hy.2.top_le le_sup_left


[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (id '' s) (id x)
[PROOFSTEP]
simpa only [image_id] using h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
hf : LeftOrdContinuous f
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₂ ∈ upperBounds {a₁, a₂}
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
hg : LeftOrdContinuous g
hf : LeftOrdContinuous f
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (g ∘ f '' s) ((g ∘ f) x)
[PROOFSTEP]
simpa only [image_image] using hg (hf h)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
⊢ LeftOrdContinuous f^[n]
[PROOFSTEP]
induction n with
| zero => exact LeftOrdContinuous.id α
| succ n ihn => exact ihn.comp hf
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
⊢ LeftOrdContinuous f^[n]
[PROOFSTEP]
induction n with
| zero => exact LeftOrdContinuous.id α
| succ n ihn => exact ihn.comp hf
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
⊢ LeftOrdContinuous f^[Nat.zero]
[PROOFSTEP]

| zero => exact LeftOrdContinuous.id α
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
⊢ LeftOrdContinuous f^[Nat.zero]
[PROOFSTEP]
exact LeftOrdContinuous.id α
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
ihn : LeftOrdContinuous f^[n]
⊢ LeftOrdContinuous f^[Nat.succ n]
[PROOFSTEP]

| succ n ihn => exact ihn.comp hf
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
ihn : LeftOrdContinuous f^[n]
⊢ LeftOrdContinuous f^[Nat.succ n]
[PROOFSTEP]
exact ihn.comp hf
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
x y : α
⊢ IsLUB (f '' {x, y}) (f x ⊔ f y)
[PROOFSTEP]
simp only [image_pair, isLUB_pair]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x ≤ f y ↔ x ≤ y
[PROOFSTEP]
simp only [← sup_eq_right, ← hf.map_sup, h.eq_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x < f y ↔ x < y
[PROOFSTEP]
simp only [lt_iff_le_not_le, hf.le_iff h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
⊢ f (sSup s) = ⨆ (x : α) (_ : x ∈ s), f x
[PROOFSTEP]
rw [hf.map_sSup', sSup_image]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
[PROOFSTEP]
simp only [iSup, hf.map_sSup', ← range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
[PROOFSTEP]
simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
s : Set α
x : α
h : IsGLB s x
⊢ IsGLB (id '' s) (id x)
[PROOFSTEP]
simpa only [image_id] using h