Natural Numbers
❱
Addition World
❱
Multiplication World
❱
Power World
❱
Function World
❱
Proposition World
❱
Advanced Proposition World
❱
Advanced Addition World
❱
Advanced Multiplication World
❱
Inequality World
❱
Tactics
❱

The Lean Natural Numbers

import MyNat.Definition
namespace MyNat
open MyNat

Advanced proposition world.

Level 4: `iff_trans`.

The mathematical statement P ↔ Q is equivalent to (P ⟹ Q) ∧ (Q ⟹ P). The cases and split tactics work on hypotheses and goals (respectively) of the form P ↔ Q.

If you need to write an ↔ arrow in Visual Studio Code you can do so by typing \iff. See the "Lean 4: Show All Abbreviations" command.

After an initial intro h you can type cases h with hpq hqp to break h : P ↔ Q into its constituent parts.

Lemma

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

lemma iff_trans: ∀ (P Q R : Prop), (P ↔ Q) → (Q ↔ R) → (P ↔ R)
iff_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) := byP, Q, R: Prop
(P ↔ Q) → (Q ↔ R) → (P ↔ R)
  intro hpq: P ↔ Q
hpqP, Q, R: Prop
hpq: P ↔ Q
(Q ↔ R) → (P ↔ R)
  intro hqr: Q ↔ R
hqrP, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
P ↔ R
  constructorP, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpP → R
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mprR → P
  cases hpq: P ↔ Q
hpq withP, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpP → R
  | intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
intro pq: P → Q
pq qp: Q → P
qp =>P, Q, R: Prop
hqr: Q ↔ R
pq: P → Q
qp: Q → P
mp.introP → R
    cases hqr: Q ↔ R
hqr withP, Q, R: Prop
hqr: Q ↔ R
pq: P → Q
qp: Q → P
mp.introP → R
    | intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
intro qr: Q → R
qr rq: R → Q
rq =>P, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
mp.intro.introP → R
      intro p: P
pP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
p: P
mp.intro.introR
      apply qr: Q → R
qrP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
p: P
mp.intro.introQ
      apply pq: P → Q
pqP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
p: P
mp.intro.introP
      exact p: P
pGoals accomplished! 🐙
  cases hpq: P ↔ Q
hpq withP, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mprR → P
  | intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
intro pq: P → Q
pq qp: Q → P
qp =>P, Q, R: Prop
hqr: Q ↔ R
pq: P → Q
qp: Q → P
mpr.introR → P
    cases hqr: Q ↔ R
hqr withP, Q, R: Prop
hqr: Q ↔ R
pq: P → Q
qp: Q → P
mpr.introR → P
    | intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
intro qr: Q → R
qr rq: R → Q
rq =>P, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
mpr.intro.introR → P
      intro r: R
rP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
r: R
mpr.intro.introP
      apply qp: Q → P
qpP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
r: R
mpr.intro.introQ
      apply rq: R → Q
rqP, Q, R: Prop
pq: P → Q
qp: Q → P
qr: Q → R
rq: R → Q
r: R
mpr.intro.introR
      exact r: R
rGoals accomplished! 🐙

Next up Level 5