calc and exact

Stream: new members

[anan]

Why is it wrong to use 'calc' to prove the same problem?
theorem ab : x ⊔ x ⊓ y = x := by

apply le_antisymm

· apply sup_le

· exact le_refl x

· exact inf_le_left  

· exact le_sup_left

theorem absorb2 : x ⊔ x ⊓ y = x := by

apply le_antisymm

· apply sup_le

· exact le_refl x

· calc

(x ⊓ y) ≤ x := inf_le_left  

· exact le_sup_left

[Kevin Buzzard]

One-line calc blocks aren't supported right now. Calculations have to have at least two steps.

By the way, you might want to read #backticks

[anan]

thank you very much