I had a question about theorem proving in lean book

Stream: new members

[Shubham Kumar]

In the book Theorem Proving in Lean

The exercises for associativity

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

I am not able to add braces when I prove the above theorems
My solution :

  theorem and_assoc : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
    Iff.intro
      (λ h₁ : (p ∧ q) ∧ r =>
        And.intro
          (And.left (And.left h₁))
          ((And.intro
            (And.right (And.left h₁))
            (And.right h₁))))
      (λ h₂ : p ∧ (q ∧ r) =>
        And.intro
          ((And.intro
            (And.left h₂)
            (And.left (And.right h₂))))
          (And.right (And.right h₂)))

when I check it

  #check and_assoc p q r

I get the following message

and_assoc p q r : (p ∧ q) ∧ r ↔ p ∧ q ∧ r

but it should be ideally

and_assoc p q r : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r)

[Alex J. Best]

You can add set_option pp.parens true on a new line before the check to ask lean to insert the parentheses in places like this where it chooses not to by default (because and is left associative for lean so the statement isn't ambiguous for lean without)

[Shubham Kumar]

so when I add set_option pp.parens true on a newline before the check I am getting the following message

unknown option 'pp.parens'

[Alex J. Best]

Which version of lean are you running?

[Shubham Kumar]

Lean 4

[Alex J. Best]

Ah I see, then maybe that option doesn't exist in Lean 4 unfortunately. You can use the info-view to click on the expression in vscode to see how the brackets are implicitly placed if that helps