internlm/Lean-Github huggingface dataset:
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (z, S n) = S n
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : plus (z, n) = n
⊢ plus (z, S n) = S n
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : plus (z, n) = n
⊢ plus (z, S n) = S n
Tactic:
rw [splus, hel]
Proof state after:
no goals
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
let A := {y : N0 | plus ((S x), y) = S (plus (x, y))}
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  simp [zplus]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [splus, hel, ←splus]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x_1 : α),
    (∃ (x_2 : x_1 ∈ N0),
        plus (S x, { val := x_1, property := (_ : x_1 ∈ N0) }) =
          S (plus (x, { val := x_1, property := (_ : x_1 ∈ N0) }))) ↔
      x_1 ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x_1 : α),
    (∃ (x_2 : x_1 ∈ N0),
        plus (S x, { val := x_1, property := (_ : x_1 ∈ N0) }) =
          S (plus (x, { val := x_1, property := (_ : x_1 ∈ N0) }))) ↔
      x_1 ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
specialize heq y
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑y ∈ N0),
      plus (S x, { val := ↑y, property := (_ : ↑y ∈ N0) }) = S (plus (x, { val := ↑y, property := (_ : ↑y ∈ N0) }))) ↔
    ↑y ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑y ∈ N0),
      plus (S x, { val := ↑y, property := (_ : ↑y ∈ N0) }) = S (plus (x, { val := ↑y, property := (_ : ↑y ∈ N0) }))) ↔
    ↑y ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S x, y) = S (plus (x, y))
⊢ plus (S x, y) = S (plus (x, y))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S x, y) = S (plus (x, y))
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
exact heq
Proof state after:
no goals
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, z) = S (plus (x, z))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, z) = S (plus (x, z))
Tactic:
simp [zplus]
Proof state after:
no goals
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S x, S n) = S (plus (x, S n))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S x, S n) = S (plus (x, S n))
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S x, n) = S (plus (x, n))
⊢ plus (S x, S n) = S (plus (x, S n))
Theorem: succ_plus_eq_succ_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S x, n) = S (plus (x, n))
⊢ plus (S x, S n) = S (plus (x, S n))
Tactic:
rw [splus, hel, ←splus]
Proof state after:
no goals
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
let A := {x : N0 | plus ((S y), x) = S (plus (x, y))}
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  rw [zplus, zero_plus_x_eq_eq]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [splus, hel, succ_plus_eq_succ_plus]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        plus (S y, { val := x, property := (_ : x ∈ N0) }) = S (plus ({ val := x, property := (_ : x ∈ N0) }, y))) ↔
      x ∈ N0
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        plus (S y, { val := x, property := (_ : x ∈ N0) }) = S (plus ({ val := x, property := (_ : x ∈ N0) }, y))) ↔
      x ∈ N0
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
specialize heq x
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0),
      plus (S y, { val := ↑x, property := (_ : ↑x ∈ N0) }) = S (plus ({ val := ↑x, property := (_ : ↑x ∈ N0) }, y))) ↔
    ↑x ∈ N0
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0),
      plus (S y, { val := ↑x, property := (_ : ↑x ∈ N0) }) = S (plus ({ val := ↑x, property := (_ : ↑x ∈ N0) }, y))) ↔
    ↑x ∈ N0
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S y, x) = S (plus (x, y))
⊢ plus (S y, x) = S (plus (x, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S y, x) = S (plus (x, y))
⊢ plus (S y, x) = S (plus (x, y))
Tactic:
exact heq
Proof state after:
no goals
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ plus (S y, z) = S (plus (z, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ plus (S y, z) = S (plus (z, y))
Tactic:
rw [zplus, zero_plus_x_eq_eq]
Proof state after:
no goals
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S y, S n) = S (plus (S n, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S y, S n) = S (plus (S n, y))
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S y, n) = S (plus (n, y))
⊢ plus (S y, S n) = S (plus (S n, y))
Theorem: succ_plus_n_eq_succ_n_plus
Proof state before:
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S y, n) = S (plus (n, y))
⊢ plus (S y, S n) = S (plus (S n, y))
Tactic:
rw [splus, hel, succ_plus_eq_succ_plus]
Proof state after:
no goals
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
⊢ mul (z, x) = z
Tactic:
let A := {x : N0 | mul (z, x) = z}
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ mul (z, x) = z
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  rw [zmul]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
⊢ mul (z, x) = z
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [smul, hel, zero_plus_x_eq_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ mul (z, x) = z
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ mul (z, x) = z
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ∀ (x : α), (∃ (x_1 : x ∈ N0), mul (z, { val := x, property := (_ : x ∈ N0) }) = z) ↔ x ∈ N0
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ∀ (x : α), (∃ (x_1 : x ∈ N0), mul (z, { val := x, property := (_ : x ∈ N0) }) = z) ↔ x ∈ N0
⊢ mul (z, x) = z
Tactic:
specialize heq x
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : (∃ (x_1 : ↑x ∈ N0), mul (z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = z) ↔ ↑x ∈ N0
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : (∃ (x_1 : ↑x ∈ N0), mul (z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = z) ↔ ↑x ∈ N0
⊢ mul (z, x) = z
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : mul (z, x) = z
⊢ mul (z, x) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : mul (z, x) = z
⊢ mul (z, x) = z
Tactic:
exact heq
Proof state after:
no goals
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ mul (z, z) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ mul (z, z) = z
Tactic:
rw [zmul]
Proof state after:
no goals
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ mul (z, S n) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ mul (z, S n) = z
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : mul (z, n) = z
⊢ mul (z, S n) = z
Theorem: zero_mul_eq_zero
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
n : ↑N0
hel : mul (z, n) = z
⊢ mul (z, S n) = z
Tactic:
rw [smul, hel, zero_plus_x_eq_eq]
Proof state after:
no goals
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
⊢ mul (S z, x) = x
Tactic:
let A := {x : N0 | mul (S z, x) = x}
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
⊢ mul (S z, x) = x
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  rw [zmul]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
⊢ mul (S z, x) = x
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [smul, hel, splus, zplus]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ mul (S z, x) = x
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ mul (S z, x) = x
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0), mul (S z, { val := x, property := (_ : x ∈ N0) }) = { val := x, property := (_ : x ∈ N0) }) ↔
      x ∈ N0
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0), mul (S z, { val := x, property := (_ : x ∈ N0) }) = { val := x, property := (_ : x ∈ N0) }) ↔
      x ∈ N0
⊢ mul (S z, x) = x
Tactic:
specialize heq x
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0), mul (S z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔
    ↑x ∈ N0
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0), mul (S z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔
    ↑x ∈ N0
⊢ mul (S z, x) = x
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : mul (S z, x) = x
⊢ mul (S z, x) = x
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : mul (S z, x) = x
⊢ mul (S z, x) = x
Tactic:
exact heq
Proof state after:
no goals
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
⊢ mul (S z, z) = z
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
⊢ mul (S z, z) = z
Tactic:
rw [zmul]
Proof state after:
no goals
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ mul (S z, S n) = S n
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ mul (S z, S n) = S n
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : mul (S z, n) = n
⊢ mul (S z, S n) = S n
Theorem: succ_zero_mul_eq_self
Proof state before:
x : ↑N0
A : Set ↑N0 := {x | mul (S z, x) = x}
hzmem : z ∈ A
n : ↑N0
hel : mul (S z, n) = n
⊢ mul (S z, S n) = S n
Tactic:
rw [smul, hel, splus, zplus]
Proof state after:
no goals
Theorem: succ_plus_n_eq_succ_n_plus'
Proof state before:
⊢ ∀ (x y : ↑N0), plus (S y, x) = S (plus (x, y))
Tactic:
apply generic_recursor
Proof state after:
case hz

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

case hs

⊢ ∀ (n : ↑N0), (∀ (y : ↑N0), plus (S y, n) = S (plus (n, y))) → ∀ (y : ↑N0), plus (S y, S n) = S (plus (S n, y))
Theorem: succ_plus_n_eq_succ_n_plus'
Proof state before:
case hz

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

⊢ ∀ (n : ↑N0), (∀ (y : ↑N0), plus (S y, n) = S (plus (n, y))) → ∀ (y : ↑N0), plus (S y, S n) = S (plus (S n, y))
Tactic:
intros n hi y
Proof state after:
case hs
n : ↑N0
hi : ∀ (y : ↑N0), plus (S y, n) = S (plus (n, y))
y : ↑N0
⊢ plus (S y, S n) = S (plus (S n, y))
Theorem: succ_plus_n_eq_succ_n_plus'
Proof state before:
case hs
n : ↑N0
hi : ∀ (y : ↑N0), plus (S y, n) = S (plus (n, y))
y : ↑N0
⊢ plus (S y, S n) = S (plus (S n, y))
Tactic:
rw [splus, hi, succ_plus_eq_succ_plus]
Proof state after:
no goals
Theorem: sum_squared_eq_sum_cubes
Proof state before:
n : ℕ
⊢ (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3

case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3
Tactic:
ring_nf
Proof state after:
case zero

⊢ (∑ x in Finset.range (1 + Nat.zero), x) ^ 2 = ∑ x in Finset.range (1 + Nat.zero), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case zero

⊢ (∑ x in Finset.range (1 + Nat.zero), x) ^ 2 = ∑ x in Finset.range (1 + Nat.zero), x ^ 3
Tactic:
simp only [Nat.zero_eq, add_zero, Finset.range_one, Finset.sum_singleton, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow']
Proof state after:
no goals
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ n + 1), x ^ 3
Tactic:
rw [Finset.range_succ,
    Finset.sum_insert Finset.not_mem_range_self,
    Finset.sum_insert Finset.not_mem_range_self]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Theorem: sum_squared_eq_sum_cubes
Proof state before:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
Tactic:
rw [add_sq]
Proof state after:
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3