Hello

Inspecting Lean

#eval"4.13.0-rc3"
 Lean.versionString: String
Lean.versionString

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

#eval"leanprover/lean4:4.13.0-rc3"
 Lean.toolchain: String
Lean.toolchain

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

#eval"01d414ac36dc28f3e424dabd36d818873fea655c"
 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 introp, q: Prop
hp: p
hq: q
mpp ∧ q → q ∧ p h: p ∧ q
hWarning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p, 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 introp, q: Prop
hp: p
hq: q
mprq ∧ p → p ∧ q h: q ∧ p
hWarning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p, 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! 🐙