internlm/Lean-Github huggingface dataset:
Theorem: zero_plus_x_eq_eq
Proof state before:
case hs
n : ↑N0
hi : plus (z, n) = n
⊢ plus (z, S n) = S n
Tactic:
rw [splus, hi]
Proof state after:
no goals
Theorem: plus_assoc
Proof state before:
⊢ ∀ (c a b : ↑N0), plus (a, plus (b, c)) = plus (plus (a, b), c)
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (a b : ↑N0), plus (a, plus (b, z)) = plus (plus (a, b), z)

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), plus (a, plus (b, n)) = plus (plus (a, b), n)) →
      ∀ (a b : ↑N0), plus (a, plus (b, S n)) = plus (plus (a, b), S n)
Theorem: plus_assoc
Proof state before:
case hz

⊢ ∀ (a b : ↑N0), plus (a, plus (b, z)) = plus (plus (a, b), z)
Tactic:
intro a b
Proof state after:
case hz
a b : ↑N0
⊢ plus (a, plus (b, z)) = plus (plus (a, b), z)
Theorem: plus_assoc
Proof state before:
case hz
a b : ↑N0
⊢ plus (a, plus (b, z)) = plus (plus (a, b), z)
Tactic:
rw [zplus, zplus]
Proof state after:
no goals
Theorem: plus_assoc
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), plus (a, plus (b, n)) = plus (plus (a, b), n)) →
      ∀ (a b : ↑N0), plus (a, plus (b, S n)) = plus (plus (a, b), S n)
Tactic:
intro c hi a b
Proof state after:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), plus (a, plus (b, c)) = plus (plus (a, b), c)
a b : ↑N0
⊢ plus (a, plus (b, S c)) = plus (plus (a, b), S c)
Theorem: plus_assoc
Proof state before:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), plus (a, plus (b, c)) = plus (plus (a, b), c)
a b : ↑N0
⊢ plus (a, plus (b, S c)) = plus (plus (a, b), S c)
Tactic:
specialize hi a b
Proof state after:
case hs
c a b : ↑N0
hi : plus (a, plus (b, c)) = plus (plus (a, b), c)
⊢ plus (a, plus (b, S c)) = plus (plus (a, b), S c)
Theorem: plus_assoc
Proof state before:
case hs
c a b : ↑N0
hi : plus (a, plus (b, c)) = plus (plus (a, b), c)
⊢ plus (a, plus (b, S c)) = plus (plus (a, b), S c)
Tactic:
rw [splus, splus, hi, splus]
Proof state after:
no goals
Theorem: mul_distrib_add
Proof state before:
⊢ ∀ (c a b : ↑N0), mul (a, plus (b, c)) = plus (mul (a, b), mul (a, c))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (a b : ↑N0), mul (a, plus (b, z)) = plus (mul (a, b), mul (a, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (a, plus (b, n)) = plus (mul (a, b), mul (a, n))) →
      ∀ (a b : ↑N0), mul (a, plus (b, S n)) = plus (mul (a, b), mul (a, S n))
Theorem: mul_distrib_add
Proof state before:
case hz

⊢ ∀ (a b : ↑N0), mul (a, plus (b, z)) = plus (mul (a, b), mul (a, z))
Tactic:
intro a b
Proof state after:
case hz
a b : ↑N0
⊢ mul (a, plus (b, z)) = plus (mul (a, b), mul (a, z))
Theorem: mul_distrib_add
Proof state before:
case hz
a b : ↑N0
⊢ mul (a, plus (b, z)) = plus (mul (a, b), mul (a, z))
Tactic:
rw [zplus, zmul, zplus]
Proof state after:
no goals
Theorem: mul_distrib_add
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (a, plus (b, n)) = plus (mul (a, b), mul (a, n))) →
      ∀ (a b : ↑N0), mul (a, plus (b, S n)) = plus (mul (a, b), mul (a, S n))
Tactic:
intro c hi a b
Proof state after:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (a, plus (b, c)) = plus (mul (a, b), mul (a, c))
a b : ↑N0
⊢ mul (a, plus (b, S c)) = plus (mul (a, b), mul (a, S c))
Theorem: mul_distrib_add
Proof state before:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (a, plus (b, c)) = plus (mul (a, b), mul (a, c))
a b : ↑N0
⊢ mul (a, plus (b, S c)) = plus (mul (a, b), mul (a, S c))
Tactic:
specialize hi a b
Proof state after:
case hs
c a b : ↑N0
hi : mul (a, plus (b, c)) = plus (mul (a, b), mul (a, c))
⊢ mul (a, plus (b, S c)) = plus (mul (a, b), mul (a, S c))
Theorem: mul_distrib_add
Proof state before:
case hs
c a b : ↑N0
hi : mul (a, plus (b, c)) = plus (mul (a, b), mul (a, c))
⊢ mul (a, plus (b, S c)) = plus (mul (a, b), mul (a, S c))
Tactic:
rw [splus, smul, smul, hi, plus_assoc]
Proof state after:
no goals
Theorem: mul_assoc'
Proof state before:
⊢ ∀ (c a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (a b : ↑N0), mul (mul (a, b), z) = mul (a, mul (b, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (mul (a, b), n) = mul (a, mul (b, n))) →
      ∀ (a b : ↑N0), mul (mul (a, b), S n) = mul (a, mul (b, S n))
Theorem: mul_assoc'
Proof state before:
case hz

⊢ ∀ (a b : ↑N0), mul (mul (a, b), z) = mul (a, mul (b, z))
Tactic:
intro a b
Proof state after:
case hz
a b : ↑N0
⊢ mul (mul (a, b), z) = mul (a, mul (b, z))
Theorem: mul_assoc'
Proof state before:
case hz
a b : ↑N0
⊢ mul (mul (a, b), z) = mul (a, mul (b, z))
Tactic:
rw [zmul, zmul, zmul]
Proof state after:
no goals
Theorem: mul_assoc'
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (mul (a, b), n) = mul (a, mul (b, n))) →
      ∀ (a b : ↑N0), mul (mul (a, b), S n) = mul (a, mul (b, S n))
Tactic:
intro c hi a b
Proof state after:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
a b : ↑N0
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Theorem: mul_assoc'
Proof state before:
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
a b : ↑N0
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Tactic:
specialize hi a b
Proof state after:
case hs
c a b : ↑N0
hi : mul (mul (a, b), c) = mul (a, mul (b, c))
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Theorem: mul_assoc'
Proof state before:
case hs
c a b : ↑N0
hi : mul (mul (a, b), c) = mul (a, mul (b, c))
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
Tactic:
rw [smul, smul, hi, mul_distrib_add]
Proof state after:
no goals
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
⊢ ∀ (r m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (m n : ↑N0), exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (m, plus (n_1, n)) = mul (exp (m, n_1), exp (m, n))) →
      ∀ (m n_1 : ↑N0), exp (m, plus (n_1, S n)) = mul (exp (m, n_1), exp (m, S n))
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
case hz

⊢ ∀ (m n : ↑N0), exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))
Tactic:
intros m n
Proof state after:
case hz
m n : ↑N0
⊢ exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
case hz
m n : ↑N0
⊢ exp (m, plus (n, z)) = mul (exp (m, n), exp (m, z))
Tactic:
rw [zplus, zexp, smul, zmul, zero_plus_x_eq_eq]
Proof state after:
no goals
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (m, plus (n_1, n)) = mul (exp (m, n_1), exp (m, n))) →
      ∀ (m n_1 : ↑N0), exp (m, plus (n_1, S n)) = mul (exp (m, n_1), exp (m, S n))
Tactic:
intros r hi m n
Proof state after:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
m n : ↑N0
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
m n : ↑N0
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Tactic:
specialize hi m n
Proof state after:
case hs
r m n : ↑N0
hi : exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Theorem: exp_add_eq_mul_exp_exp
Proof state before:
case hs
r m n : ↑N0
hi : exp (m, plus (n, r)) = mul (exp (m, n), exp (m, r))
⊢ exp (m, plus (n, S r)) = mul (exp (m, n), exp (m, S r))
Tactic:
rw [splus, sexp, sexp, hi, mul_assoc']
Proof state after:
no goals
Theorem: exp_assoc
Proof state before:
⊢ ∀ (r m n : ↑N0), exp (exp (m, n), r) = exp (m, mul (n, r))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (m n : ↑N0), exp (exp (m, n), z) = exp (m, mul (n, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (exp (m, n_1), n) = exp (m, mul (n_1, n))) →
      ∀ (m n_1 : ↑N0), exp (exp (m, n_1), S n) = exp (m, mul (n_1, S n))
Theorem: exp_assoc
Proof state before:
case hz

⊢ ∀ (m n : ↑N0), exp (exp (m, n), z) = exp (m, mul (n, z))
Tactic:
intros m n
Proof state after:
case hz
m n : ↑N0
⊢ exp (exp (m, n), z) = exp (m, mul (n, z))
Theorem: exp_assoc
Proof state before:
case hz
m n : ↑N0
⊢ exp (exp (m, n), z) = exp (m, mul (n, z))
Tactic:
rw [zexp, zmul, zexp]
Proof state after:
no goals
Theorem: exp_assoc
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (exp (m, n_1), n) = exp (m, mul (n_1, n))) →
      ∀ (m n_1 : ↑N0), exp (exp (m, n_1), S n) = exp (m, mul (n_1, S n))
Tactic:
intros r hi m n
Proof state after:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (exp (m, n), r) = exp (m, mul (n, r))
m n : ↑N0
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))
Theorem: exp_assoc
Proof state before:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (exp (m, n), r) = exp (m, mul (n, r))
m n : ↑N0
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))
Tactic:
specialize hi m n
Proof state after:
case hs
r m n : ↑N0
hi : exp (exp (m, n), r) = exp (m, mul (n, r))
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))
Theorem: exp_assoc
Proof state before:
case hs
r m n : ↑N0
hi : exp (exp (m, n), r) = exp (m, mul (n, r))
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))
Tactic:
rw [smul, sexp, exp_add_eq_mul_exp_exp, hi]
Proof state after:
no goals
Theorem: succ_zero_mul_eq_self'
Proof state before:
⊢ ∀ (x : ↑N0), mul (S z, x) = x
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ mul (S z, z) = z

case hs

⊢ ∀ (n : ↑N0), mul (S z, n) = n → mul (S z, S n) = S n
Theorem: succ_zero_mul_eq_self'
Proof state before:
case hz

⊢ mul (S z, z) = z
Tactic:
rw [zmul]
Proof state after:
no goals
Theorem: succ_zero_mul_eq_self'
Proof state before:
case hs

⊢ ∀ (n : ↑N0), mul (S z, n) = n → mul (S z, S n) = S n
Tactic:
intros x hi
Proof state after:
case hs
x : ↑N0
hi : mul (S z, x) = x
⊢ mul (S z, S x) = S x
Theorem: succ_zero_mul_eq_self'
Proof state before:
case hs
x : ↑N0
hi : mul (S z, x) = x
⊢ mul (S z, S x) = S x
Tactic:
rw [smul, hi, splus, zplus]
Proof state after:
no goals
Theorem: zero_mul_eq_zero
Proof state before:
⊢ ∀ (x : ↑N0), mul (z, x) = z
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ mul (z, z) = z

case hs

⊢ ∀ (n : ↑N0), mul (z, n) = z → mul (z, S n) = z
Theorem: zero_mul_eq_zero
Proof state before:
case hz

⊢ mul (z, z) = z
Tactic:
rw [zmul]
Proof state after:
no goals
Theorem: zero_mul_eq_zero
Proof state before:
case hs

⊢ ∀ (n : ↑N0), mul (z, n) = z → mul (z, S n) = z
Tactic:
intro x hi
Proof state after:
case hs
x : ↑N0
hi : mul (z, x) = z
⊢ mul (z, S x) = z
Theorem: zero_mul_eq_zero
Proof state before:
case hs
x : ↑N0
hi : mul (z, x) = z
⊢ mul (z, S x) = z
Tactic:
rw [smul, hi, zero_plus_x_eq_eq]
Proof state after:
no goals
Theorem: succ_plus_eq_succ_plus
Proof state before:
⊢ ∀ (b a : ↑N0), plus (S a, b) = S (plus (a, b))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (a : ↑N0), plus (S a, z) = S (plus (a, z))

case hs

⊢ ∀ (n : ↑N0), (∀ (a : ↑N0), plus (S a, n) = S (plus (a, n))) → ∀ (a : ↑N0), plus (S a, S n) = S (plus (a, S n))
Theorem: succ_plus_eq_succ_plus
Proof state before:
case hz

⊢ ∀ (a : ↑N0), plus (S a, z) = S (plus (a, z))
Tactic:
intro a
Proof state after:
case hz
a : ↑N0
⊢ plus (S a, z) = S (plus (a, z))
Theorem: succ_plus_eq_succ_plus
Proof state before:
case hz
a : ↑N0
⊢ plus (S a, z) = S (plus (a, z))
Tactic:
rw [zplus, zplus]
Proof state after:
no goals
Theorem: succ_plus_eq_succ_plus
Proof state before:
case hs

⊢ ∀ (n : ↑N0), (∀ (a : ↑N0), plus (S a, n) = S (plus (a, n))) → ∀ (a : ↑N0), plus (S a, S n) = S (plus (a, S n))
Tactic:
intro b hi a
Proof state after:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), plus (S a, b) = S (plus (a, b))
a : ↑N0
⊢ plus (S a, S b) = S (plus (a, S b))
Theorem: succ_plus_eq_succ_plus
Proof state before:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), plus (S a, b) = S (plus (a, b))
a : ↑N0
⊢ plus (S a, S b) = S (plus (a, S b))
Tactic:
specialize hi a
Proof state after:
case hs
b a : ↑N0
hi : plus (S a, b) = S (plus (a, b))
⊢ plus (S a, S b) = S (plus (a, S b))
Theorem: succ_plus_eq_succ_plus
Proof state before:
case hs
b a : ↑N0
hi : plus (S a, b) = S (plus (a, b))
⊢ plus (S a, S b) = S (plus (a, S b))
Tactic:
rw [splus, hi, ←splus]
Proof state after:
no goals
Theorem: plus_comm
Proof state before:
⊢ ∀ (a b : ↑N0), plus (a, b) = plus (b, a)
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (b : ↑N0), plus (z, b) = plus (b, z)

case hs

⊢ ∀ (n : ↑N0), (∀ (b : ↑N0), plus (n, b) = plus (b, n)) → ∀ (b : ↑N0), plus (S n, b) = plus (b, S n)
Theorem: plus_comm
Proof state before:
case hz

⊢ ∀ (b : ↑N0), plus (z, b) = plus (b, z)
Tactic:
intro a
Proof state after:
case hz
a : ↑N0
⊢ plus (z, a) = plus (a, z)
Theorem: plus_comm
Proof state before:
case hz
a : ↑N0
⊢ plus (z, a) = plus (a, z)
Tactic:
rw [zplus, zero_plus_x_eq_eq]
Proof state after:
no goals
Theorem: plus_comm
Proof state before:
case hs

⊢ ∀ (n : ↑N0), (∀ (b : ↑N0), plus (n, b) = plus (b, n)) → ∀ (b : ↑N0), plus (S n, b) = plus (b, S n)
Tactic:
intro a hi b
Proof state after:
case hs
a : ↑N0
hi : ∀ (b : ↑N0), plus (a, b) = plus (b, a)
b : ↑N0
⊢ plus (S a, b) = plus (b, S a)
Theorem: plus_comm
Proof state before:
case hs
a : ↑N0
hi : ∀ (b : ↑N0), plus (a, b) = plus (b, a)
b : ↑N0
⊢ plus (S a, b) = plus (b, S a)
Tactic:
specialize hi b
Proof state after:
case hs
a b : ↑N0
hi : plus (a, b) = plus (b, a)
⊢ plus (S a, b) = plus (b, S a)
Theorem: plus_comm
Proof state before:
case hs
a b : ↑N0
hi : plus (a, b) = plus (b, a)
⊢ plus (S a, b) = plus (b, S a)
Tactic:
rw [splus, succ_plus_eq_succ_plus, hi]
Proof state after:
no goals
Theorem: muls
Proof state before:
⊢ ∀ (b a : ↑N0), mul (S a, b) = plus (mul (a, b), b)
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (a : ↑N0), mul (S a, z) = plus (mul (a, z), z)

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a : ↑N0), mul (S a, n) = plus (mul (a, n), n)) → ∀ (a : ↑N0), mul (S a, S n) = plus (mul (a, S n), S n)
Theorem: muls
Proof state before:
case hz

⊢ ∀ (a : ↑N0), mul (S a, z) = plus (mul (a, z), z)
Tactic:
intro a
Proof state after:
case hz
a : ↑N0
⊢ mul (S a, z) = plus (mul (a, z), z)
Theorem: muls
Proof state before:
case hz
a : ↑N0
⊢ mul (S a, z) = plus (mul (a, z), z)
Tactic:
rw [zmul, zmul, zplus]
Proof state after:
no goals
Theorem: muls
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a : ↑N0), mul (S a, n) = plus (mul (a, n), n)) → ∀ (a : ↑N0), mul (S a, S n) = plus (mul (a, S n), S n)
Tactic:
intro b hi a
Proof state after:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), mul (S a, b) = plus (mul (a, b), b)
a : ↑N0
⊢ mul (S a, S b) = plus (mul (a, S b), S b)
Theorem: muls
Proof state before:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), mul (S a, b) = plus (mul (a, b), b)
a : ↑N0
⊢ mul (S a, S b) = plus (mul (a, S b), S b)
Tactic:
specialize hi a
Proof state after:
case hs
b a : ↑N0
hi : mul (S a, b) = plus (mul (a, b), b)
⊢ mul (S a, S b) = plus (mul (a, S b), S b)
Theorem: muls
Proof state before:
case hs
b a : ↑N0
hi : mul (S a, b) = plus (mul (a, b), b)
⊢ mul (S a, S b) = plus (mul (a, S b), S b)
Tactic:
rw [smul, smul, hi, splus, splus, ←plus_assoc, plus_comm b, plus_assoc]
Proof state after:
no goals
Theorem: mul_comm'
Proof state before:
⊢ ∀ (a b : ↑N0), mul (a, b) = mul (b, a)
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (b : ↑N0), mul (z, b) = mul (b, z)

case hs

⊢ ∀ (n : ↑N0), (∀ (b : ↑N0), mul (n, b) = mul (b, n)) → ∀ (b : ↑N0), mul (S n, b) = mul (b, S n)
Theorem: mul_comm'
Proof state before:
case hz

⊢ ∀ (b : ↑N0), mul (z, b) = mul (b, z)
Tactic:
intro a
Proof state after:
case hz
a : ↑N0
⊢ mul (z, a) = mul (a, z)
Theorem: mul_comm'
Proof state before:
case hz
a : ↑N0
⊢ mul (z, a) = mul (a, z)
Tactic:
rw [zmul, zero_mul_eq_zero]
Proof state after:
no goals
Theorem: mul_comm'
Proof state before:
case hs

⊢ ∀ (n : ↑N0), (∀ (b : ↑N0), mul (n, b) = mul (b, n)) → ∀ (b : ↑N0), mul (S n, b) = mul (b, S n)
Tactic:
intro a hi b
Proof state after:
case hs
a : ↑N0
hi : ∀ (b : ↑N0), mul (a, b) = mul (b, a)
b : ↑N0
⊢ mul (S a, b) = mul (b, S a)
Theorem: mul_comm'
Proof state before:
case hs
a : ↑N0
hi : ∀ (b : ↑N0), mul (a, b) = mul (b, a)
b : ↑N0
⊢ mul (S a, b) = mul (b, S a)
Tactic:
specialize hi b
Proof state after:
case hs
a b : ↑N0
hi : mul (a, b) = mul (b, a)
⊢ mul (S a, b) = mul (b, S a)
Theorem: mul_comm'
Proof state before:
case hs
a b : ↑N0
hi : mul (a, b) = mul (b, a)
⊢ mul (S a, b) = mul (b, S a)
Tactic:
rw [smul, muls, hi]
Proof state after:
no goals
Theorem: exp_distrib_mul
Proof state before:
⊢ ∀ (r m n : ↑N0), exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ ∀ (m n : ↑N0), exp (mul (m, n), z) = mul (exp (m, z), exp (n, z))

case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (mul (m, n_1), n) = mul (exp (m, n), exp (n_1, n))) →
      ∀ (m n_1 : ↑N0), exp (mul (m, n_1), S n) = mul (exp (m, S n), exp (n_1, S n))
Theorem: exp_distrib_mul
Proof state before:
case hz

⊢ ∀ (m n : ↑N0), exp (mul (m, n), z) = mul (exp (m, z), exp (n, z))
Tactic:
intro m n
Proof state after:
case hz
m n : ↑N0
⊢ exp (mul (m, n), z) = mul (exp (m, z), exp (n, z))
Theorem: exp_distrib_mul
Proof state before:
case hz
m n : ↑N0
⊢ exp (mul (m, n), z) = mul (exp (m, z), exp (n, z))
Tactic:
rw [zexp, zexp, zexp, succ_zero_mul_eq_self']
Proof state after:
no goals
Theorem: exp_distrib_mul
Proof state before:
case hs

⊢ ∀ (n : ↑N0),
    (∀ (m n_1 : ↑N0), exp (mul (m, n_1), n) = mul (exp (m, n), exp (n_1, n))) →
      ∀ (m n_1 : ↑N0), exp (mul (m, n_1), S n) = mul (exp (m, S n), exp (n_1, S n))
Tactic:
intro r hi m n
Proof state after:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
m n : ↑N0
⊢ exp (mul (m, n), S r) = mul (exp (m, S r), exp (n, S r))
Theorem: exp_distrib_mul
Proof state before:
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
m n : ↑N0
⊢ exp (mul (m, n), S r) = mul (exp (m, S r), exp (n, S r))
Tactic:
specialize hi m n
Proof state after:
case hs
r m n : ↑N0
hi : exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
⊢ exp (mul (m, n), S r) = mul (exp (m, S r), exp (n, S r))
Theorem: exp_distrib_mul
Proof state before:
case hs
r m n : ↑N0
hi : exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
⊢ exp (mul (m, n), S r) = mul (exp (m, S r), exp (n, S r))
Tactic:
rw [sexp, sexp, sexp, hi, ←mul_assoc', mul_assoc' m, mul_comm' _ m, ←mul_assoc', ←mul_assoc']
Proof state after:
no goals
Theorem: false_proof
Proof state before:
⊢ False
Tactic:
let baldie : Person := ⟨[]⟩
Proof state after:
baldie : Person := { hair := [] }
⊢ False
Theorem: false_proof
Proof state before:
baldie : Person := { hair := [] }
⊢ False
Tactic:
have bald : Bald baldie := rfl
Proof state after:
baldie : Person := { hair := [] }
bald : Bald baldie
⊢ False
Theorem: false_proof
Proof state before:
baldie : Person := { hair := [] }
bald : Bald baldie
⊢ False
Tactic:
have still_bald := add_one_hair_still_bald bald
Proof state after:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False
Theorem: false_proof
Proof state before:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False
Tactic:
rw [Bald, add_one_hair] at still_bald
Proof state after:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : { hair := Strand.strand :: baldie.hair }.hair = ∅
⊢ False
Theorem: false_proof
Proof state before:
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : { hair := Strand.strand :: baldie.hair }.hair = ∅
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: all_people_bald
Proof state before:
⊢ ∀ (person : Person), Bald person
Tactic:
intro person
Proof state after:
person : Person
⊢ Bald person
Theorem: all_people_bald
Proof state before:
person : Person
⊢ Bald person
Tactic:
rw [Bald]
Proof state after:
person : Person
⊢ person.hair = ∅
Theorem: all_people_bald
Proof state before:
person : Person
⊢ person.hair = ∅
Tactic:
induction' person.hair with _ h ih
Proof state after:
case nil
person : Person
⊢ [] = ∅

case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
⊢ head✝ :: h = ∅
Theorem: all_people_bald
Proof state before:
case nil
person : Person
⊢ [] = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: all_people_bald
Proof state before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
⊢ head✝ :: h = ∅
Tactic:
have baldie := add_one_hair_still_bald ih
Proof state after:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : Bald (add_one_hair { hair := h })
⊢ head✝ :: h = ∅
Theorem: all_people_bald
Proof state before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : Bald (add_one_hair { hair := h })
⊢ head✝ :: h = ∅
Tactic:
rw [add_one_hair, Bald] at baldie
Proof state after:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : { hair := Strand.strand :: { hair := h }.hair }.hair = ∅
⊢ head✝ :: h = ∅
Theorem: all_people_bald
Proof state before:
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : { hair := Strand.strand :: { hair := h }.hair }.hair = ∅
⊢ head✝ :: h = ∅
Tactic:
exact baldie
Proof state after:
no goals
Theorem: ℕplus.mul_def
Proof state before:
a b : ℕplus
⊢ ↑a * ↑b ≠ 0
Tactic:
simp only [ne_eq, mul_eq_zero, not_or]
Proof state after:
a b : ℕplus
⊢ ¬↑a = 0 ∧ ¬↑b = 0
Theorem: ℕplus.mul_def
Proof state before:
a b : ℕplus
⊢ ¬↑a = 0 ∧ ¬↑b = 0
Tactic:
exact ⟨a.property, b.property⟩
Proof state after:
no goals
Theorem: dvd_iff_nat_dvd
Proof state before:
a b : ℕplus
⊢ R3 a b ↔ ↑a ∣ ↑b
Tactic:
constructor
Proof state after:
case mp
a b : ℕplus
⊢ R3 a b → ↑a ∣ ↑b

case mpr
a b : ℕplus
⊢ ↑a ∣ ↑b → R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mp
a b : ℕplus
⊢ R3 a b → ↑a ∣ ↑b
Tactic:
intro hdvd
Proof state after:
case mp
a b : ℕplus
hdvd : R3 a b
⊢ ↑a ∣ ↑b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mp
a b : ℕplus
hdvd : R3 a b
⊢ ↑a ∣ ↑b
Tactic:
rcases hdvd with ⟨c, hc⟩
Proof state after:
case mp.intro
a b c : ℕplus
hc : b = a * c
⊢ ↑a ∣ ↑b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mp.intro
a b c : ℕplus
hc : b = a * c
⊢ ↑a ∣ ↑b
Tactic:
use c.val
Proof state after:
case h
a b c : ℕplus
hc : b = a * c
⊢ ↑b = ↑a * ↑c
Theorem: dvd_iff_nat_dvd
Proof state before:
case h
a b c : ℕplus
hc : b = a * c
⊢ ↑b = ↑a * ↑c
Tactic:
rw [ℕplus.mul_def] at hc
Proof state after:
case h
a b c : ℕplus
hc : b = { val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Theorem: dvd_iff_nat_dvd
Proof state before:
case h
a b c : ℕplus
hc : b = { val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Tactic:
apply_fun Subtype.val at hc
Proof state after:
case h
a b c : ℕplus
hc : ↑b = ↑{ val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Theorem: dvd_iff_nat_dvd
Proof state before:
case h
a b c : ℕplus
hc : ↑b = ↑{ val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Tactic:
exact hc
Proof state after:
no goals
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr
a b : ℕplus
⊢ ↑a ∣ ↑b → R3 a b
Tactic:
intro hdvd
Proof state after:
case mpr
a b : ℕplus
hdvd : ↑a ∣ ↑b
⊢ R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr
a b : ℕplus
hdvd : ↑a ∣ ↑b
⊢ R3 a b
Tactic:
rcases hdvd with ⟨c, hc⟩
Proof state after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
⊢ R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
⊢ R3 a b
Tactic:
have hb := b.property
Proof state after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑b ≠ 0
⊢ R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑b ≠ 0
⊢ R3 a b
Tactic:
rw [hc, mul_ne_zero_iff] at hb
Proof state after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
⊢ R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
⊢ R3 a b
Tactic:
let lc : ℕplus := ⟨c, hb.2⟩
Proof state after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ R3 a b
Theorem: dvd_iff_nat_dvd
Proof state before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ R3 a b
Tactic:
use lc
Proof state after:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ b = a * lc