prop

Stream: new members

[BANGJI HU]

import Mathlib.Tactic

variable (P Q R: Prop)

theorem q1 : ((P↔Q)↔R) ↔ (P↔(Q↔R)) := by
  constructor
  intro h
  constructor
  intro p
  constructor
  intro q

[BANGJI HU]

Can you give me some hints?

[Yoh Tanimoto]

I think, when you introduce two goals for ↔, it's better to indent like this

import Mathlib.Tactic

variable (P Q R: Prop)

theorem q1 : ((P↔Q)↔R) ↔ (P↔(Q↔R)) := by
  constructor
  · intro h
    constructor
    · intro p
      constructor
      · intro q

Note that if h: A↔B, then h.mp : A → B and h.mpr : B → A

[BANGJI HU]

(deleted)