Theorem: Section6Sheet3solutions.foo (FormalisingMathematics2024/Solutions/Section06orderingsAndLattices/Sheet3.lean)

State before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
Tactic:
letI : DistribLattice L := { (show Lattice L by infer_instance) with le_sup_inf := fun x y z => by rw [← h] }
State after:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
this : DistribLattice L :=
  let src :=
    let_fun this := inferInstance;
    this;
  DistribLattice.mk (_ : ∀ (x y z : L), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

State before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
this : DistribLattice L :=
  let src :=
    let_fun this := inferInstance;
    this;
  DistribLattice.mk (_ : ∀ (x y z : L), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
Tactic:
exact fun a b c => inf_sup_left
State after:
no goals

State before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
⊢ Lattice L
Tactic:
infer_instance
State after:
no goals

State before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
src✝ : Lattice L :=
  let_fun this := inferInstance;
  this
x y z : L
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
Tactic:
rw [← h]
State after:
no goals