OR elimination type mismatch

Stream: new members

[Kunwar Shaanjeet Singh Grover]

Hi! I was trying to prove this example using this proof (You can look at the goal information below for ease of reading):

variables A B C : Prop
variables p q r : Prop

section
  example : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
  λ h : A ∧ (B ∨ C),
  have a : A,
    from h.left,
  have boc : (B ∨ C),
    from h.right,
  have br : B → (A ∧ B) ∨ (A ∧ C), from (
    λ b : B,
    have anb : A ∧ B,
      from and.intro a b,
    show (A ∧ B) ∨ (A ∧ C),
    from or.inl anb),
  have cr : C → (A ∧ B) ∨ (A ∧ C), from (
    λ c : C,
    have anc : A ∧ C,
      from and.intro a c,
    show (A ∧ B) ∨ (A ∧ C),
    from or.inr anc),
  have bocr : (B ∨ C) → (A ∧ B) ∨ (A ∧ C),
    from or.elim boc br cr,
  show (A ∧ B) ∨ (A ∧ C),
    from bocr boc
end

This proof gives me an error on the proof of (B ∨ C) → (A ∧ B) ∨ (A ∧ C) using or.elim with the error:

type mismatch at application
  boc.elim br
term
  br
has type
  B → A ∧ B ∨ A ∧ C
but is expected to have type
  B → B ∨ C → A ∧ B ∨ A ∧ C

The goal:

1 goal
A B C : Prop,
h : A ∧ (B ∨ C),
a : A,
boc : B ∨ C,
br : B → A ∧ B ∨ A ∧ C,
cr : C → A ∧ B ∨ A ∧ C
⊢ B ∨ C → A ∧ B ∨ A ∧ C

This doesn't make sense to me since or.elim's type says that I need three things to prove A or B -> C :

A or B
A -> C
B -> C

which I have provided. So I'm a bit confused about where this is coming from.

NOTE: The proof is a homework question. I only want to understand why there is a type error, not the answer.

[Stuart Presnell]

Check again what the output type of or.elim boc br cr is. Does it match the type you’ve given for bocr?

[Kunwar Shaanjeet Singh Grover]

Ah, that was a stupid mistake. Sorry!

[Kunwar Shaanjeet Singh Grover]

And thanks for helping out!

[Stuart Presnell]

No problem :)