Hello

Inspecting Lean

#eval"4.32.2" Lean.versionString: String
Lean.versionString

#eval"4.32.2" Lean.versionStringCore: String
Lean.versionStringCore

#eval"leanprover/lean4:4.32.2" Lean.toolchain: String
Lean.toolchain

#eval"leanprover/lean4" Lean.origin: String
Lean.origin

#eval"f3b06c705e6c85f5314019d5d3baab0fec5b580c" Lean.githash: String
Lean.githash

Proofs

theorem test: ∀ (p q : Prop), p → q → (p ∧ q ↔ q ∧ p)
test (p: Prop
p q: Prop
q : Prop: Type
Prop) (hp: p
hp : p: Prop
p) (hq: q
hq : q: Prop
q): p: Prop
p ∧ q: Prop
q ↔ q: Prop
q ∧ p: Prop
p := byGoals accomplished! 🐙
  apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introp, q: Prop
hp: p
hq: q
mpp ∧ q → q ∧ p
p, q: Prop
hp: p
hq: q
mprq ∧ p → p ∧ q
  .p, q: Prop
hp: p
hq: q
mpp ∧ q → q ∧ p intro h: p ∧ q
hp, q: Prop
hp: p
hq: q
h: p ∧ q
mpq ∧ p
    apply And.intro: ∀ {a b : Prop}, a → b → a ∧ b
And.introp, q: Prop
hp: p
hq: q
h: p ∧ q
mp.leftq
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.rightp
    .p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.leftq exact hq: q
hqGoals accomplished! 🐙
    .p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.rightp exact hp: p
hpGoals accomplished! 🐙
  .p, q: Prop
hp: p
hq: q
mprq ∧ p → p ∧ q intro h: q ∧ p
hp, q: Prop
hp: p
hq: q
h: q ∧ p
mprp ∧ q
    apply And.intro: ∀ {a b : Prop}, a → b → a ∧ b
And.introp, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.leftp
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.rightq
    .p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.leftp exact hp: p
hpGoals accomplished! 🐙
    .p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.rightq exact hq: q
hqGoals accomplished! 🐙