internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
⊢ q' ≠ 0
Tactic:
contradict qne0 with h11
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
h11 : q' = 0
⊢ q = 0
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
h11 : q' = 0
⊢ q = 0
Tactic:
rewrite [q'halfq, h11]
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
h11 : q' = 0
⊢ 2 * 0 = 0
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
h11 : q' = 0
⊢ 2 * 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.rep_image_base
Proof state before:
A : Type
f : A → A
B : Set A
⊢ rep_image f 0 B = B
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.rep_image_step
Proof state before:
A : Type
f : A → A
n : ℕ
B : Set A
⊢ rep_image f (n + 1) B = image f (rep_image f n B)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.rep_image_sub_closed
Proof state before:
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D
Tactic:
by_induc
Proof state after:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ rep_image f 0 B ⊆ D

case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ rep_image f 0 B ⊆ D
Tactic:
rewrite [rep_image_base]
Proof state after:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ B ⊆ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ B ⊆ D
Tactic:
show B ⊆ D from h1
Proof state after:
no goals
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
⊢ rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
⊢ rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Tactic:
assume ih : rep_image f n B ⊆ D
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
⊢ rep_image f (n + 1) B ⊆ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
⊢ rep_image f (n + 1) B ⊆ D
Tactic:
fix x : A
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
⊢ x ∈ rep_image f (n + 1) B → x ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
⊢ x ∈ rep_image f (n + 1) B → x ∈ D
Tactic:
assume h3 : x ∈ rep_image f (n + 1) B
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ rep_image f (n + 1) B
⊢ x ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ rep_image f (n + 1) B
⊢ x ∈ D
Tactic:
rewrite [rep_image_step] at h3
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ image f (rep_image f n B)
⊢ x ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ image f (rep_image f n B)
⊢ x ∈ D
Tactic:
define at h3
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
⊢ x ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
⊢ x ∈ D
Tactic:
obtain (b : A) (h4 : b ∈ rep_image f n B ∧ f b = x) from h3
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ x ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ x ∈ D
Tactic:
rewrite [←h4.right]
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ f b ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ f b ∈ D
Tactic:
have h5 : b ∈ D := ih h4.left
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Tactic:
define at h2
Proof state after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : ∀ x ∈ D, f x ∈ D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Theorem: HTPI.rep_image_sub_closed
Proof state before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : ∀ x ∈ D, f x ∈ D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Tactic:
show f b ∈ D from h2 b h5
Proof state after:
no goals
Theorem: HTPI.Theorem_6_5_1
Proof state before:
A : Type
f : A → A
B : Set A
⊢ closure f B (cumul_image f B)
Tactic:
define
Proof state after:
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D} ∧ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Theorem: HTPI.Theorem_6_5_1
Proof state before:
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D} ∧ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Tactic:
apply And.intro
Proof state after:
case left
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D}

case right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D}
Tactic:
define
Proof state after:
case left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B ∧ closed f (cumul_image f B)
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B ∧ closed f (cumul_image f B)
Tactic:
apply And.intro
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B

case left.right
A : Type
f : A → A
B : Set A
⊢ closed f (cumul_image f B)
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B
Tactic:
fix x : A
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ B → x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ B → x ∈ cumul_image f B
Tactic:
assume h1 : x ∈ B
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ cumul_image f B
Tactic:
define
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ ∃ n, x ∈ rep_image f n B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ ∃ n, x ∈ rep_image f n B
Tactic:
apply Exists.intro 0
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ rep_image f 0 B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ rep_image f 0 B
Tactic:
rewrite [rep_image_base]
Proof state after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ B
Tactic:
show x ∈ B from h1
Proof state after:
no goals
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
⊢ closed f (cumul_image f B)
Tactic:
define
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ cumul_image f B, f x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ cumul_image f B, f x ∈ cumul_image f B
Tactic:
fix x : A
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ cumul_image f B → f x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ cumul_image f B → f x ∈ cumul_image f B
Tactic:
assume h1 : x ∈ cumul_image f B
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ cumul_image f B
⊢ f x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ cumul_image f B
⊢ f x ∈ cumul_image f B
Tactic:
define at h1
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
⊢ f x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
⊢ f x ∈ cumul_image f B
Tactic:
obtain (m : Nat) (h2 : x ∈ rep_image f m B) from h1
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ cumul_image f B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ cumul_image f B
Tactic:
define
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ n, f x ∈ rep_image f n B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ n, f x ∈ rep_image f n B
Tactic:
apply Exists.intro (m + 1)
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ rep_image f (m + 1) B
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ rep_image f (m + 1) B
Tactic:
rewrite [rep_image_step]
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ image f (rep_image f m B)
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ image f (rep_image f m B)
Tactic:
define
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ x_1 ∈ rep_image f m B, f x_1 = f x
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ x_1 ∈ rep_image f m B, f x_1 = f x
Tactic:
apply Exists.intro x
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ x ∈ rep_image f m B ∧ f x = f x
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ x ∈ rep_image f m B ∧ f x = f x
Tactic:
apply And.intro h2
Proof state after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x = f x
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Tactic:
fix D : Set A
Proof state after:
case right
A : Type
f : A → A
B D : Set A
⊢ D ∈ {D | B ⊆ D ∧ closed f D} → sub A (cumul_image f B) D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
⊢ D ∈ {D | B ⊆ D ∧ closed f D} → sub A (cumul_image f B) D
Tactic:
assume h1 : D ∈ {D : Set A | B ⊆ D ∧ closed f D}
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : D ∈ {D | B ⊆ D ∧ closed f D}
⊢ sub A (cumul_image f B) D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : D ∈ {D | B ⊆ D ∧ closed f D}
⊢ sub A (cumul_image f B) D
Tactic:
define at h1
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ sub A (cumul_image f B) D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ sub A (cumul_image f B) D
Tactic:
define
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D
Tactic:
fix x : A
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
⊢ x ∈ cumul_image f B → x ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
⊢ x ∈ cumul_image f B → x ∈ D
Tactic:
assume h2 : x ∈ cumul_image f B
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : x ∈ cumul_image f B
⊢ x ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : x ∈ cumul_image f B
⊢ x ∈ D
Tactic:
define at h2
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
⊢ x ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
⊢ x ∈ D
Tactic:
obtain (m : Nat) (h3 : x ∈ rep_image f m B) from h2
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
⊢ x ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
⊢ x ∈ D
Tactic:
have h4 : rep_image f m B ⊆ D :=
  rep_image_sub_closed h1.left h1.right m
Proof state after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
h4 : rep_image f m B ⊆ D
⊢ x ∈ D
Theorem: HTPI.Theorem_6_5_1
Proof state before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
h4 : rep_image f m B ⊆ D
⊢ x ∈ D
Tactic:
show x ∈ D from h4 h3
Proof state after:
no goals
Theorem: HTPI.mod_succ_lt
Proof state before:
a n : ℕ
⊢ a % (n + 1) < n + 1
Tactic:
have h : n + 1 > 0 := Nat.succ_pos n
Proof state after:
a n : ℕ
h : n + 1 > 0
⊢ a % (n + 1) < n + 1
Theorem: HTPI.mod_succ_lt
Proof state before:
a n : ℕ
h : n + 1 > 0
⊢ a % (n + 1) < n + 1
Tactic:
show a % (n + 1) < n + 1 from Nat.mod_lt a h
Proof state after:
no goals
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ d ∣ a % b
Tactic:
set q : Nat := a / b
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
⊢ d ∣ a % b
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
⊢ d ∣ a % b
Tactic:
have h3 : b * q + a % b = a := Nat.div_add_mod a b
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
⊢ d ∣ a % b
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
⊢ d ∣ a % b
Tactic:
obtain (j : Nat) (h4 : a = d * j) from h1
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
⊢ d ∣ a % b
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
⊢ d ∣ a % b
Tactic:
obtain (k : Nat) (h5 : b = d * k) from h2
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ d ∣ a % b
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ d ∣ a % b
Tactic:
define
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, a % b = d * c
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, a % b = d * c
Tactic:
apply Exists.intro (j - k * q)
Proof state after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a % b = d * (j - k * q)
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a % b = d * (j - k * q)
Tactic:
show a % b = d * (j - k * q) from
  calc a % b
    _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm
    _ = a - b * q := by rw [h3]
    _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]
    _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm
Proof state after:
no goals
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ b * q + a % b - b * q = a - b * q
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.dvd_mod_of_dvd_a_b
Proof state before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a - b * q = d * j - d * (k * q)
Tactic:
rw [h4, h5, mul_assoc]
Proof state after:
no goals
Theorem: HTPI.gcd_base
Proof state before:
a : ℕ
⊢ gcd a 0 = a
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
⊢ gcd a b = gcd b (a % b)
Tactic:
obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd a b = gcd b (a % b)
Theorem: HTPI.gcd_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd a b = gcd b (a % b)
Tactic:
rewrite [h2]
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd a (n + 1) = gcd (n + 1) (a % (n + 1))
Theorem: HTPI.gcd_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd a (n + 1) = gcd (n + 1) (a % (n + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.mod_nonzero_lt
Proof state before:
a b : ℕ
h : b ≠ 0
⊢ a % b < b
Tactic:
have h1 : b > 0 := Nat.pos_of_ne_zero h
Proof state after:
a b : ℕ
h : b ≠ 0
h1 : b > 0
⊢ a % b < b
Theorem: HTPI.mod_nonzero_lt
Proof state before:
a b : ℕ
h : b ≠ 0
h1 : b > 0
⊢ a % b < b
Tactic:
show a % b < b from Nat.mod_lt a h1
Proof state after:
no goals
Theorem: HTPI.dvd_self
Proof state before:
n : ℕ
⊢ n ∣ n
Tactic:
apply Exists.intro 1
Proof state after:
n : ℕ
⊢ n = n * 1
Theorem: HTPI.dvd_self
Proof state before:
n : ℕ
⊢ n = n * 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.gcd_dvd
Proof state before:
⊢ ∀ (b a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
by_strong_induc
Proof state after:
⊢ ∀ (b : ℕ), (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
⊢ ∀ (b : ℕ), (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
fix b : Nat
Proof state after:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1
Proof state after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
⊢ ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
⊢ ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
fix a : Nat
Proof state after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
⊢ gcd a b ∣ a ∧ gcd a b ∣ b