proof style readability improvement

Stream: new members

[Nicolas Rolland]

The second proof below seems more readable to me than the first, but I am sure there are improvements.
If you have any I am interested

import Mathlib.Tactic

variable {α : Type _} [Lattice α]
variable (a b c : α)

#check sup_assoc      -- (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)
#check inf_sup_self   -- a ⊓ (a ⊔ b) = a
#check  sup_inf_self  -- a ⊔ (a ⊓ b) = a
#check  inf_comm      -- a ⊓ b = b ⊓ a

-- It is also a good exercise to show that in any lattice,
-- either distributivity law implies the other:

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) := calc
  a ⊔ (b ⊓ c) = (a ⊔ (a ⊓ c)) ⊔ (b ⊓ c)  := by rw [(sup_inf_self : a ⊔ (a ⊓ c) = a)]
            _ = a  ⊔  ((a ⊓ c) ⊔ (b ⊓ c))  := by rw [sup_assoc]
            _ = a  ⊔  ((c ⊓ a) ⊔ (b ⊓ c))  := by rw [inf_comm]
            _ = a  ⊔  ((c ⊓ a) ⊔ (c ⊓ b))  := by rw [@inf_comm _ _ b]
            _ = a  ⊔  (c ⊓ (a ⊔ b))   := by rw [h ]
            _ = a  ⊔  ((a ⊔ b) ⊓ c)  := by rw [inf_comm]
            _ = (a ⊓ (a ⊔ b)) ⊔  ((a ⊔ b) ⊓ c)  := by rw [inf_sup_self]
            _ = ((a ⊔ b) ⊓ a) ⊔  ((a ⊔ b) ⊓ c)  := by  rw [inf_comm ]
            _ = (a ⊔ b) ⊓ (a ⊔ c)  := by rw [h]


example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) := calc
  a ⊔ (b ⊓ c) = (a ⊔ (a ⊓ c)) ⊔ (b ⊓ c)         := by rw [sup_inf_self]
            _ = a  ⊔ ((c ⊓ a) ⊔ (c ⊓ b))        := by simp only [sup_assoc, inf_comm]
            _ = a  ⊔ (c ⊓ (a ⊔ b))              := by rw [h]
            _ = ((a ⊔ b) ⊓ a) ⊔  ((a ⊔ b) ⊓ c)  := by simp only [inf_comm , inf_sup_self]
            _ = (a ⊔ b) ⊓ (a ⊔ c)               := by rw [h]

[Nicolas Rolland]

The "solution" folder in Mathematics in lean rewrites this as

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
  rw [h, @inf_comm _ _ (a ⊔ b), absorb1, @inf_comm _ _ (a ⊔ b), h, ← sup_assoc, @inf_comm _ _ c a,
    absorb2, inf_comm]

more compact for sure, but not more readable

[Martin Dvořák]

I like your solution:

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) :
  a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) :=
calc
  a ⊔ (b ⊓ c) = (a ⊔ (a ⊓ c)) ⊔ (b ⊓ c)        := by rw [sup_inf_self]
            _ = a ⊔ ((c ⊓ a) ⊔ (c ⊓ b))        := by simp only [sup_assoc, inf_comm]
            _ = a ⊔ (c ⊓ (a ⊔ b))              := by rw [h]
            _ = ((a ⊔ b) ⊓ a) ⊔ ((a ⊔ b) ⊓ c)  := by simp only [inf_comm , inf_sup_self]
            _ = (a ⊔ b) ⊓ (a ⊔ c)              := by rw [h]