import Mathlib.Tactic

variable (p q r s : Prop)

-- Proof 1
-- =======

example:
  (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
by
  intro ⟨hpq, hrs⟩ ⟨hp, hr⟩
  -- hpq : p → q
  -- hrs : r → s
  -- hp : p
  -- hr : r
  constructor
  . -- q
    exact hpq hp
  . -- s
    exact hrs hr

-- Proof 2
-- =======

example:
  (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
by
  intro ⟨hpq, hrs⟩ ⟨hp, hr⟩
  -- hpq : p → q
  -- hrs : r → s
  -- hp : p
  -- hr : r
  exact ⟨hpq hp, hrs hr⟩

-- Proof 3
-- =======

example:
  (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
fun ⟨hpq, hrs⟩ ⟨hp, hr⟩ ↦ ⟨hpq hp, hrs hr⟩

-- Proof 4
-- =======

example:
  (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
fun ⟨hpq, hrs⟩ hpr ↦ And.imp hpq hrs hpr

-- Proof 5
-- =======

example:
  (p → q) ∧ (r → s) → ((p ∧ r) → (q ∧ s)) :=
by aesop

theory Praeclarum_theorema
imports Main
begin

(* Proof 1 *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof (rule impI)
  assume "(p ⟶ q) ∧ (r ⟶ s)"
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof (rule impI)
    assume "p ∧ r"
    show "q ∧ s"
    proof (rule conjI)
      have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct1)
      moreover have "p" using ‹p ∧ r› by (rule conjunct1)
      ultimately show "q" by (rule mp)
    next
      have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct2)
      moreover have "r" using ‹p ∧ r› by (rule conjunct2)
      ultimately show "s" by (rule mp)
    qed
  qed
qed

(* Proof 2 *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
proof
  assume "(p ⟶ q) ∧ (r ⟶ s)"
  show "(p ∧ r) ⟶ (q ∧ s)"
  proof
    assume "p ∧ r"
    show "q ∧ s"
    proof
      have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..
      moreover have "p" using ‹p ∧ r› ..
      ultimately show "q" ..
    next
      have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..
      moreover have "r" using ‹p ∧ r› ..
      ultimately show "s" ..
    qed
  qed
qed

(* Proof 3 *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  apply (rule impI)
  apply (rule impI)
  apply (erule conjE)+
  apply (rule conjI)
   apply (erule mp)
   apply assumption
  apply (erule mp)
  apply assumption
  done

(* Proof 4 *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  by simp

end