inference_fail.lean

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (assume h : p ∧ (q ∨ r),
    have hp : p, from h.left,
    or.elim h.right
      (assume hq, or.inl ⟨hp, hq⟩)
      (assume hr, or.inr ⟨hp, hr⟩))
  (assume h : (p ∧ q) ∨ (p ∧ r),
    or.elim h
      (assume hpq,
        have hp : p, from hpq.left,
        have hq : q, from hpq.right,
        ⟨hp, or.inl hq⟩)
      (assume hpr,
        have hp : p, from hpr.left,
        have hr : r, from hpr.right,
        ⟨hp, or.inr hr⟩))
  
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (λ h : p ∧ (q ∨ r),
    (λ hp : p,
      or.elim h.right
        (λ hq, or.inl $ and.intro hp hq)
        (λ hr, or.inr $ and.intro hp hr))
    h.left)
  (λ h : (p ∧ q) ∨ (p ∧ r),
    or.elim h
      (λ hpq : p ∧ q,
        (λ hp : p,
          (λ hq: q,
            and.intro hp (or.inl hq))
          hpq.right)
        hpq.left)
      (λ hpr : p ∧ r,
        (λ hp : p,
          (λ hr : r,
            and.intro hp (or.inr hr))
          hpr.right)
        hpr.left))

/-
propositions_as_types.lean:455:4: error 
type mismatch at application
  or.elim h (λ (hpq : p ∧ q),
              (λ (hp : p),
                (λ (hq : q),
                  ⟨hp, or.inl hq⟩)
                (hpq.right))
              (hpq.left))
term
  λ (hpq : p ∧ q),
      (λ (hp : p),
        (λ (hq : q),
          ⟨hp, or.inl hq⟩)
        (hpq.right))
      (hpq.left)
has type
  ∀ (hpq : p ∧ q), p ∧ (q ∨ ?m_1[hpq, _, _])
but is expected to have type
  p ∧ q → p ∧ (q ∨ r)

propositions_as_types.lean:455:4: error 
type mismatch at application
  or.elim h ⁇ 
    (λ (hpr : p ∧ r),
      (λ (hp : p),
        (λ (hr : r), 
          ⟨hp, or.inr hr⟩)
        (hpr.right))
      (hpr.left))
term
  λ (hpr : p ∧ r), (λ (hp : p), (λ (hr : r), ⟨hp, or.inr hr⟩) (hpr.right)) (hpr.left)
has type
  ∀ (hpr : p ∧ r), p ∧ (?m_1[hpr, _, _] ∨ r)
but is expected to have type
  p ∧ r → p ∧ (q ∨ r)
-/