α : 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
α : 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)
rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
α : 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
α : 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
apply le_inf inf_le_left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.26537 ⊔ 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
⊢ α
α : 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
apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
no goals
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.26537 ⊔ 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
⊢ α
rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]