import MyNat.Definition
namespace MyNat
open MyNat

Advanced proposition world.

Level 3: and_trans.

With this proof we can use the first cases tactic to extract hypotheses p : P q : Q from hpq : P ∧ Q and then we can use another cases tactic to extract hypotheses q' : Q and r : R from hpr : Q ∧ R then we can split the resulting goal ⊢ P ∧ R using constructor and easily pick off the resulting sub-goals ⊢ P and ⊢ R using our given hypotheses.

Lemma

If P, Q and R are true/false statements, then P ∧ Q and Q ∧ R together imply P ∧ R.

lemma 
and_trans: ∀ (P Q R : Prop), P ∧ Q → Q ∧ R → P ∧ R
and_trans (
P: Prop
P 
Q: Prop
Q 
R: Prop
R : 
Prop: Type
Prop) : 
P: Prop
P ∧ 
Q: Prop
Q → 
Q: Prop
Q ∧ 
R: Prop
R → 
P: Prop
P ∧ 
R: Prop
R := by
P, Q, R: Prop
P ∧ Q → Q ∧ R → P ∧ R
  intro 
hpq: P ∧ Q
hpq
P, Q, R: Prop
hpq: P ∧ Q
Q ∧ R → P ∧ R
  intro 
hqr: Q ∧ R
hqr
P, Q, R: Prop
hpq: P ∧ Q
hqr: Q ∧ R
P ∧ R
  cases 
hpq: P ∧ Q
hpq with
P, Q, R: Prop
hpq: P ∧ Q
hqr: Q ∧ R
P ∧ R
  | 
intro: ∀ {a b : Prop}, a → b → a ∧ b
intro 
p: P
p 
q: Q
q =>
P, Q, R: Prop
hqr: Q ∧ R
p: P
q: Q
intro
P ∧ R
    cases 
hqr: Q ∧ R
hqr with
P, Q, R: Prop
hqr: Q ∧ R
p: P
q: Q
intro
P ∧ R
    | 
intro: ∀ {a b : Prop}, a → b → a ∧ b
intro 
q': Q
q' 
r: R
r =>
P, Q, R: Prop
p: P
q, q': Q
r: R
intro.intro
P ∧ R
      constructor
P, Q, R: Prop
p: P
q, q': Q
r: R
intro.intro.left
P
P, Q, R: Prop
p: P
q, q': Q
r: R
intro.intro.right
R
      assumption
P, Q, R: Prop
p: P
q, q': Q
r: R
intro.intro.right
R
      assumption
Goals accomplished! 🐙

Next up Level 4