internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 2 * c
Tactic:
apply Exists.intro (3 * k)
Proof state after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * (3 * k)
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * (3 * k)
Tactic:
rewrite [←mul_assoc 2 3 k]
Proof state after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * 3 * k
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * 3 * k
Tactic:
show n = 2 * 3 * k from h2
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 3 ∣ n
Tactic:
define
Proof state after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 3 * c
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 3 * c
Tactic:
apply Exists.intro (2 * k)
Proof state after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * (2 * k)
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * (2 * k)
Tactic:
rewrite [←mul_assoc 3 2 k]
Proof state after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * 2 * k
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * 2 * k
Tactic:
show n = 3 * 2 * k from h2
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n
Tactic:
assume h1 : 2 ∣ n ∧ 3 ∣ n
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
⊢ 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
⊢ 6 ∣ n
Tactic:
have h2 : 2 ∣ n := h1.left
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
⊢ 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
⊢ 6 ∣ n
Tactic:
have h3 : 3 ∣ n := h1.right
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
h3 : 3 ∣ n
⊢ 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
h3 : 3 ∣ n
⊢ 6 ∣ n
Tactic:
define at h2
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : 3 ∣ n
⊢ 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : 3 ∣ n
⊢ 6 ∣ n
Tactic:
define at h3
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ 6 ∣ n
Tactic:
define
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ ∃ c, n = 6 * c
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ ∃ c, n = 6 * c
Tactic:
obtain (j : Int) (h4 : n = 2 * j) from h2
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
⊢ ∃ c, n = 6 * c
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
⊢ ∃ c, n = 6 * c
Tactic:
obtain (k : Int) (h5 : n = 3 * k) from h3
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ ∃ c, n = 6 * c
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ ∃ c, n = 6 * c
Tactic:
have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 3 * (2 * j) - 2 * (3 * k) := by ring
    _ = 3 * n - 2 * n := by rw [←h4, ←h5]
    _ = n := by ring
Proof state after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
h6 : 6 * (j - k) = n
⊢ ∃ c, n = 6 * c
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
h6 : 6 * (j - k) = n
⊢ ∃ c, n = 6 * c
Tactic:
show ∃ (c : Int), n = 6 * c from
  Exists.intro (j - k) h6.symm
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 6 * (j - k) = 3 * (2 * j) - 2 * (3 * k)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * (2 * j) - 2 * (3 * k) = 3 * n - 2 * n
Tactic:
rw [←h4, ←h5]
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * n - 2 * n = n
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_3_5_4
Proof state before:
x : ℝ
h1 : x ≤ x ^ 2
⊢ x ≤ 0 ∨ 1 ≤ x
Tactic:
or_right with h2
Proof state after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
⊢ 1 ≤ x
Theorem: HTPI.Example_3_5_4
Proof state before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
⊢ 1 ≤ x
Tactic:
have h3 : 0 < x := lt_of_not_le h2
Proof state after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ 1 ≤ x
Theorem: HTPI.Example_3_5_4
Proof state before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ 1 ≤ x
Tactic:
have h4 : 1 * x ≤ x * x :=
  calc 1 * x
    _ = x := one_mul x
    _ ≤ x ^ 2 := h1
    _ = x * x := by ring
Proof state after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
h4 : 1 * x ≤ x * x
⊢ 1 ≤ x
Theorem: HTPI.Example_3_5_4
Proof state before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
h4 : 1 * x ≤ x * x
⊢ 1 ≤ x
Tactic:
show 1 ≤ x from le_of_mul_le_mul_right h4 h3
Proof state after:
no goals
Theorem: HTPI.Example_3_5_4
Proof state before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ x ^ 2 = x * x
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_3_2_4
Proof state before:
P Q R : Prop
h : P → Q → R
⊢ ¬R → P → ¬Q
Tactic:
assume h2 : ¬R
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Theorem: HTPI.Example_3_2_4
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Tactic:
assume h3 : P
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Theorem: HTPI.Example_3_2_4
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Tactic:
have h4 : Q → R := h h3
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q → R
⊢ ¬Q
Theorem: HTPI.Example_3_2_4
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q → R
⊢ ¬Q
Tactic:
contrapos at h4
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : ¬R → ¬Q
⊢ ¬Q
Theorem: HTPI.Example_3_2_4
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : ¬R → ¬Q
⊢ ¬Q
Tactic:
show ¬Q from h4 h2
Proof state after:
no goals
Theorem: HTPI.two_imp
Proof state before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ R → ¬P
Tactic:
contrapos
Proof state after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ P → ¬R
Theorem: HTPI.two_imp
Proof state before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
⊢ P → ¬R
Tactic:
assume h3 : P
Proof state after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
⊢ ¬R
Theorem: HTPI.two_imp
Proof state before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
⊢ ¬R
Tactic:
have h4 : Q := h1 h3
Proof state after:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
h4 : Q
⊢ ¬R
Theorem: HTPI.two_imp
Proof state before:
P Q R : Prop
h1 : P → Q
h2 : Q → ¬R
h3 : P
h4 : Q
⊢ ¬R
Tactic:
show ¬R from h2 h4
Proof state after:
no goals
Theorem: HTPI.Example_3_2_5_simple
Proof state before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B \ C
⊢ a ∈ C
Tactic:
define at h2
Proof state after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple
Proof state before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C
Tactic:
demorgan at h2
Proof state after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple
Proof state before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C
Tactic:
conditional at h2
Proof state after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple
Proof state before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C
Tactic:
show a ∈ C from h2 h1
Proof state after:
no goals
Theorem: HTPI.Example_3_2_5_simple_general
Proof state before:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : a ∉ B \ C
⊢ a ∈ C
Tactic:
define at h2
Proof state after:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple_general
Proof state before:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C
Tactic:
demorgan at h2
Proof state after:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple_general
Proof state before:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C
Tactic:
conditional at h2
Proof state after:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C
Theorem: HTPI.Example_3_2_5_simple_general
Proof state before:
U : Type
B C : Set U
a : U
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C
Tactic:
show a ∈ C from h2 h1
Proof state after:
no goals
Theorem: HTPI.not_not_and_distrib
Proof state before:
p q : Prop
⊢ ¬(¬p ∧ q) ↔ p ∨ ¬q
Tactic:
rw [not_and_or, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.not_and_not_distrib
Proof state before:
p q : Prop
⊢ ¬(p ∧ ¬q) ↔ ¬p ∨ q
Tactic:
rw [not_and_or, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.not_not_or_distrib
Proof state before:
p q : Prop
⊢ ¬(¬p ∨ q) ↔ p ∧ ¬q
Tactic:
rw [not_or, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.not_or_not_distrib
Proof state before:
p q : Prop
⊢ ¬(p ∨ ¬q) ↔ ¬p ∧ q
Tactic:
rw [not_or, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.not_imp_not_iff_and
Proof state before:
p q : Prop
⊢ ¬(p → ¬q) ↔ p ∧ q
Tactic:
rw [not_imp, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.not_imp_iff_not_and
Proof state before:
p q : Prop
⊢ ¬(q → p) ↔ ¬p ∧ q
Tactic:
rw [not_imp]
Proof state after:
p q : Prop
⊢ q ∧ ¬p ↔ ¬p ∧ q
Theorem: HTPI.not_imp_iff_not_and
Proof state before:
p q : Prop
⊢ q ∧ ¬p ↔ ¬p ∧ q
Tactic:
exact And.comm
Proof state after:
no goals
Theorem: HTPI.not_not_iff
Proof state before:
p q : Prop
⊢ ¬(¬p ↔ q) ↔ (p ↔ q)
Tactic:
rw [not_iff, Classical.not_not]
Proof state after:
no goals
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ b
Tactic:
apply ExistsUnique.elim h2
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b
Tactic:
intro x h3 h4
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ b
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ b
Tactic:
apply h1 x h3
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ ∀ (y z : α), p y → p z → y = z
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ ∀ (y z : α), p y → p z → y = z
Tactic:
intro y z h5 h6
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
⊢ y = z
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
⊢ y = z
Tactic:
have h7 := h4 y h5
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
⊢ y = z
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
⊢ y = z
Tactic:
have h8 := h4 z h6
Proof state after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
h8 : z = x
⊢ y = z
Theorem: HTPI.exun_elim
Proof state before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
h8 : z = x
⊢ y = z
Tactic:
rw [h7,h8]
Proof state after:
no goals
Theorem: HTPI.induc_from
Proof state before:
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ n ≥ k, P n
Tactic:
apply @Nat.rec
Proof state after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ Nat.zero ≥ k → P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ Nat.zero ≥ k → P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h3
Proof state after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
have h4 : k = 0 := Nat.eq_zero_of_le_zero h3
Proof state after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
rewrite [h4] at h1
Proof state after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P 0
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P 0
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
exact h1
Proof state after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
fix n
Proof state after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
⊢ (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
⊢ (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h3
Proof state after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
⊢ Nat.succ n ≥ k → P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
⊢ Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h4
Proof state after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
⊢ P (Nat.succ n)
Tactic:
have h5 : k < n + 1 ∨ k = n + 1 := LE.le.lt_or_eq_dec h4
Proof state after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1 ∨ k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1 ∨ k = n + 1
⊢ P (Nat.succ n)
Tactic:
by_cases on h5
Proof state after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
have h6 : k ≤ n := Nat.le_of_lt_succ h5
Proof state after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
have h7 := h3 h6
Proof state after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
h7 : P n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
h7 : P n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
exact h2 n h6 h7
Proof state after:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
rewrite [h5] at h1
Proof state after:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h1 : P (n + 1)
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Theorem: HTPI.induc_from
Proof state before:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h1 : P (n + 1)
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
exact h1
Proof state after:
no goals
Theorem: HTPI.sum_base
Proof state before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ Sum i from k to k, f i = f k
Tactic:
define : Sum i from k to k, f i
Proof state after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq (k + 1 - k) k fun i => f i) = f k
Theorem: HTPI.sum_base
Proof state before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq (k + 1 - k) k fun i => f i) = f k
Tactic:
rewrite [Nat.add_sub_cancel_left]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq 1 k fun i => f i) = f k
Theorem: HTPI.sum_base
Proof state before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq 1 k fun i => f i) = f k
Tactic:
rewrite [sum_seq, sum_seq]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ 0 + f (k + 0) = f k
Theorem: HTPI.sum_base
Proof state before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ 0 + f (k + 0) = f k
Tactic:
rewrite [zero_add, add_zero]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ f k = f k
Theorem: HTPI.sum_base
Proof state before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ f k = f k
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ Sum i from k to n + 1, f i = (Sum i from k to n, f i) + f (n + 1)
Tactic:
define : Sum i from k to (n + 1), f i
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
obtain j h1 from Nat.le.dest h
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
have h2 : n + 1 + 1 - k = n + 1 - k + 1 := by
  rewrite [←h1, add_assoc, add_assoc, Nat.add_sub_cancel_left,
    add_assoc, Nat.add_sub_cancel_left, add_assoc]
  rfl
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
have h3 : f (n + 1) = f (k + (n + 1 - k)) := by
  rewrite [←h1, add_assoc, Nat.add_sub_cancel_left]
  rfl
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
rewrite [h2, h3]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 - k + 1) k fun i => f i) = (Sum i from k to n, f i) + f (k + (n + 1 - k))