variable (P Q R : Prop)

/-- multiline `sorry` -/
example : (P → Q) → (Q → R) → (P → R) := by
  sorry

/-- various size of indent -/
example : (P → Q) → (Q → R) → (P → R) := by
  try
    sorry

/-- focusing dot -/
example : (P → Q) → (P → R) → (P → Q ∧ R) := by
  intro pq pr p
  constructor
  · sorry
  · sorry

/-- inline `sorry` -/
example : 1 + n = n + 1 := by
  calc
    1 + n = n + 1 := by sorry
    _ = n + 1 := by sorry
    _ = sorry := by sorry

/-- ignore pattern for a line -/
example : 1 + n = n + 1 := by
  calc
    1 + n = 1 + n := by rfl
    _ = n + 1 := by sorry

/-- ignore pattern for a block -/
example : 1 + n = n + 1 := by
  calc
    1 + n = 1 + n := by rfl
    _ = n + 1 := by ac_rfl
