Ill-made Question 13, Exam Review 2

[hanzhi713]

Question 13 says

Use example to prove that for all proposition, P, Q, and R, if P → Q → R then P → R.

This is not correct. I can prove it's false. See my piazza post

theorem exist_not_not_forall : 
    ∀ (α : Type) (P : α → Prop), (∃ x, ¬ P x) → ¬ (∀ x, P x) :=
    begin
        assume α P,
        assume h,
        assume f,
        apply exists.elim h,
            assume a npa,
            have : P a, from f a,
            show false, from npa this
    end

example : ¬(∀ {P Q R : Prop}, (P → Q → R) → (P → R)) :=
begin
    apply exist_not_not_forall,
        apply exists.intro true,
            apply exist_not_not_forall,
                apply exists.intro false,
                    apply exist_not_not_forall,
                        apply exists.intro false,
                            assume h,
                            have : true → false → false,
                                assume t f, assumption,
                            have : true → false, from h this,
                            show false, from this true.intro
end