X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hm : IsMaximal x (x ⊔ y)
⊢ Iso (x, x ⊔ y) (x ⊓ y, y)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y a b : X
hm : IsMaximal x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ Iso (x, a) (b, y)
substs a b
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hm : IsMaximal x (x ⊔ y)
⊢ Iso (x, x ⊔ y) (x ⊓ y, y)
exact second_iso hm