[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
