Need help with trivial identity

Stream: new members

[Noob]

Hi,
Can't figure out how to get p cancelled in the proof of the left side of the iff:

 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
    iff.intro
      (λ h : ¬(p ∨ q),
        λ (hp : p),
        have hpq : p ∨ q, from or.inl hp,
        show ¬p ∧ ¬ q, from false.elim (h hpq))
      (λ ⟨hnp, hnq⟩,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

Lean complains that the left side has type
¬(p ∨ q) → p → ¬p ∧ ¬q
but is expected to have type
¬(p ∨ q) → ¬p ∧ ¬q
which makes sense.
Could someone give me a hint?

[Kenny Lau]

write down a proof in maths first

[Bryan Gin-ge Chen]

Note that you can solve these by (almost mindlessly) chasing the type errors at underscores. Here are the first few steps which should get you back on the right track:

 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
    iff.intro
      (λ h : ¬(p ∨ q),
        _
      (λ ⟨hnp, hnq⟩,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
    iff.intro
      (λ h : ¬(p ∨ q),
        and.intro _ _
      (λ ⟨hnp, hnq⟩,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

 example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
    iff.intro
      (λ h : ¬(p ∨ q),
        and.intro (λ hp, _) (λ hq, _))
      (λ ⟨hnp, hnq⟩,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

etc.

[Noob]

@Bryan Gin-ge Chen, this is extremely helpful and exactly the kind of advice I was looking for. Thanks a lot!

[Kevin Buzzard]

@Noob this video might help. This is what Bryan is referring to when he talks about chasing type errors at underscores. The link points to the start of the term mode proof; the first half of the video is a tactic mode proof.

[Noob]

@Kevin Buzzard, the video is really helpful. The only feature I'm not familiar with (apart from how to use tactics) is the $ operator, but you explain it along the way. I think the term mode is not more intimidating (you need to know less to use it) if you use formatting similar to what you used in the tactics mode.

[Noob]

@Kevin Buzzard, I think having type annotations on hypotheses might make the proof easier to follow for beginners, but maybe it's just my bias as a programmer.