internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
⊢ denum (Univ ℚ)
Tactic:
have h1 : Univ Nat ∼ I := unbdd_subset_nat image_fqn_unbdd
Proof state after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ denum (Univ ℚ)
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ denum (Univ ℚ)
Tactic:
have h2 : image fqn (Univ Rat) = I := by rfl
Proof state after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
⊢ denum (Univ ℚ)
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
⊢ denum (Univ ℚ)
Tactic:
have h3 : Univ Rat ∼ I :=
  equinum_image (one_one_on_of_one_one fqn_one_one (Univ Rat)) h2
Proof state after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
⊢ denum (Univ ℚ)
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
⊢ denum (Univ ℚ)
Tactic:
have h4 : I ∼ Univ Rat := Theorem_8_1_3_2 h3
Proof state after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
h4 : I ∼ Univ ℚ
⊢ denum (Univ ℚ)
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
h4 : I ∼ Univ ℚ
⊢ denum (Univ ℚ)
Tactic:
show denum (Univ Rat) from Theorem_8_1_3_3 h1 h4
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_6
Proof state before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ image fqn (Univ ℚ) = I
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.eq_zero_of_I_zero_equinum
Proof state before:
n : ℕ
h1 : I 0 ∼ I n
⊢ n = 0
Tactic:
rewrite [←numElts_def, zero_elts_iff_empty] at h1
Proof state after:
n : ℕ
h1 : empty (I n)
⊢ n = 0
Theorem: HTPI.eq_zero_of_I_zero_equinum
Proof state before:
n : ℕ
h1 : empty (I n)
⊢ n = 0
Tactic:
contradict h1 with h2
Proof state after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ ∃ x, x ∈ I n
Theorem: HTPI.eq_zero_of_I_zero_equinum
Proof state before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ ∃ x, x ∈ I n
Tactic:
apply Exists.intro 0
Proof state after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 ∈ I n
Theorem: HTPI.eq_zero_of_I_zero_equinum
Proof state before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 ∈ I n
Tactic:
define
Proof state after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 < n
Theorem: HTPI.eq_zero_of_I_zero_equinum
Proof state before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 < n
Tactic:
show 0 < n from Nat.pos_of_ne_zero h2
Proof state after:
no goals
Theorem: HTPI.eq_of_I_equinum
Proof state before:
⊢ ∀ ⦃m n : ℕ⦄, I m ∼ I n → m = n
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ ∀ ⦃n : ℕ⦄, I 0 ∼ I n → 0 = n

case Induction_Step

⊢ ∀ (m : ℕ), (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Base_Case

⊢ ∀ ⦃n : ℕ⦄, I 0 ∼ I n → 0 = n
Tactic:
fix n : Nat
Proof state after:
case Base_Case
n : ℕ
⊢ I 0 ∼ I n → 0 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Base_Case
n : ℕ
⊢ I 0 ∼ I n → 0 = n
Tactic:
assume h1 : I 0 ∼ I n
Proof state after:
case Base_Case
n : ℕ
h1 : I 0 ∼ I n
⊢ 0 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Base_Case
n : ℕ
h1 : I 0 ∼ I n
⊢ 0 = n
Tactic:
show 0 = n from (eq_zero_of_I_zero_equinum h1).symm
Proof state after:
no goals
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step

⊢ ∀ (m : ℕ), (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
fix m : Nat
Proof state after:
case Induction_Step
m : ℕ
⊢ (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
⊢ (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
assume ih : ∀ ⦃n : Nat⦄, I m ∼ I n → m = n
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
⊢ ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
⊢ ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
⊢ I (m + 1) ∼ I n → m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
⊢ I (m + 1) ∼ I n → m + 1 = n
Tactic:
assume h1 : I (m + 1) ∼ I n
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ m + 1 = n
Tactic:
have h2 : n ≠ 0 := by
  by_contra h2
  have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
  rewrite [h2] at h3
  have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
  linarith
  done
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
⊢ m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
⊢ m + 1 = n
Tactic:
obtain (k : Nat) (h3 : n = k + 1) from exists_eq_add_one_of_ne_zero h2
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
k : ℕ
h3 : n = k + 1
⊢ m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
k : ℕ
h3 : n = k + 1
⊢ m + 1 = n
Tactic:
rewrite [h3] at h1
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = n
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = n
Tactic:
rewrite [h3]
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = k + 1
Tactic:
have h4 : m ∈ I (m + 1) := I_max m
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
⊢ m + 1 = k + 1
Tactic:
have h5 : k ∈ I (k + 1) := I_max k
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
⊢ m + 1 = k + 1
Tactic:
have h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k} :=
  remove_one_equinum h1 h4 h5
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k}
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k}
⊢ m + 1 = k + 1
Tactic:
rewrite [I_diff, I_diff] at h6
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
⊢ m + 1 = k + 1
Tactic:
have h7 : m = k := ih h6
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ m + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ m + 1 = k + 1
Tactic:
rewrite [h7]
Proof state after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ k + 1 = k + 1
Theorem: HTPI.eq_of_I_equinum
Proof state before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ k + 1 = k + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.eq_of_I_equinum
Proof state before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ n ≠ 0
Tactic:
by_contra h2
Proof state after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
⊢ False
Theorem: HTPI.eq_of_I_equinum
Proof state before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
⊢ False
Tactic:
have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
Proof state after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I n ∼ I (m + 1)
⊢ False
Theorem: HTPI.eq_of_I_equinum
Proof state before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I n ∼ I (m + 1)
⊢ False
Tactic:
rewrite [h2] at h3
Proof state after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
⊢ False
Theorem: HTPI.eq_of_I_equinum
Proof state before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
⊢ False
Tactic:
have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
Proof state after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
h4 : m + 1 = 0
⊢ False
Theorem: HTPI.eq_of_I_equinum
Proof state before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
h4 : m + 1 = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.numElts_unique
Proof state before:
U : Type
A : Set U
m n : ℕ
h1 : numElts A m
h2 : numElts A n
⊢ m = n
Tactic:
rewrite [numElts_def] at h1
Proof state after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : numElts A n
⊢ m = n
Theorem: HTPI.numElts_unique
Proof state before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : numElts A n
⊢ m = n
Tactic:
rewrite [numElts_def] at h2
Proof state after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
⊢ m = n
Theorem: HTPI.numElts_unique
Proof state before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
⊢ m = n
Tactic:
have h3 : A ∼ I n := Theorem_8_1_3_2 h2
Proof state after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
⊢ m = n
Theorem: HTPI.numElts_unique
Proof state before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
⊢ m = n
Tactic:
have h4 : I m ∼ I n := Theorem_8_1_3_3 h1 h3
Proof state after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
h4 : I m ∼ I n
⊢ m = n
Theorem: HTPI.numElts_unique
Proof state before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
h4 : I m ∼ I n
⊢ m = n
Tactic:
show m = n from eq_of_I_equinum h4
Proof state after:
no goals
Theorem: HTPI.Set_rp_below_def
Proof state before:
a m : ℕ
⊢ a ∈ Set_rp_below m ↔ rel_prime m a ∧ a < m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.neb_phi
Proof state before:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (phi m)
Tactic:
rewrite [phi_def]
Proof state after:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Theorem: HTPI.neb_phi
Proof state before:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Tactic:
have h1 : m ≤ m := by linarith
Proof state after:
m : ℕ
h1 : m ≤ m
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Theorem: HTPI.neb_phi
Proof state before:
m : ℕ
h1 : m ≤ m
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Tactic:
show num_elts_below (Set_rp_below m) m (num_rp_below m m) from
  neb_nrpb m h1
Proof state after:
no goals
Theorem: HTPI.neb_phi
Proof state before:
m : ℕ
⊢ m ≤ m
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.phi_is_numElts
Proof state before:
m : ℕ
⊢ numElts (Set_rp_below m) (phi m)
Tactic:
rewrite [numElts_def]
Proof state after:
m : ℕ
⊢ I (phi m) ∼ Set_rp_below m
Theorem: HTPI.phi_is_numElts
Proof state before:
m : ℕ
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
have h1 : ∀ n ∈ Set_rp_below m, n < m := by
  fix n : Nat
  assume h2 : n ∈ Set_rp_below m
  define at h2
  show n < m from h2.right
  done
Proof state after:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
⊢ I (phi m) ∼ Set_rp_below m
Theorem: HTPI.phi_is_numElts
Proof state before:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
have h2 : num_elts_below (Set_rp_below m) m (phi m) := neb_phi m
Proof state after:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
h2 : num_elts_below (Set_rp_below m) m (phi m)
⊢ I (phi m) ∼ Set_rp_below m
Theorem: HTPI.phi_is_numElts
Proof state before:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
h2 : num_elts_below (Set_rp_below m) m (phi m)
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
show I (phi m) ∼ Set_rp_below m from bdd_subset_nat h1 h2
Proof state after:
no goals
Theorem: HTPI.phi_is_numElts
Proof state before:
m : ℕ
⊢ ∀ n ∈ Set_rp_below m, n < m
Tactic:
fix n : Nat
Proof state after:
m n : ℕ
⊢ n ∈ Set_rp_below m → n < m
Theorem: HTPI.phi_is_numElts
Proof state before:
m n : ℕ
⊢ n ∈ Set_rp_below m → n < m
Tactic:
assume h2 : n ∈ Set_rp_below m
Proof state after:
m n : ℕ
h2 : n ∈ Set_rp_below m
⊢ n < m
Theorem: HTPI.phi_is_numElts
Proof state before:
m n : ℕ
h2 : n ∈ Set_rp_below m
⊢ n < m
Tactic:
define at h2
Proof state after:
m n : ℕ
h2 : rel_prime m n ∧ n < m
⊢ n < m
Theorem: HTPI.phi_is_numElts
Proof state before:
m n : ℕ
h2 : rel_prime m n ∧ n < m
⊢ n < m
Tactic:
show n < m from h2.right
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b ≡ ↑a (MOD m)
Tactic:
define
Proof state after:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ ∃ c, t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * c
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ ∃ c, t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * c
Tactic:
apply Exists.intro (s * (b - a))
Proof state after:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * (s * (↑b - ↑a))
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * (s * (↑b - ↑a))
Tactic:
show t * n * a + s * m * b - a = m * (s * (b - a)) from
  calc t * n * a + s * m * b - a
    _ = (t * n - 1) * a + s * m * b := by ring
    _ = (t * n - (s * m + t * n)) * a + s * m * b := by rw [h]
    _ = m * (s * (b - a)) := by ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = (t * ↑n - 1) * ↑a + s * ↑m * ↑b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ (t * ↑n - 1) * ↑a + s * ↑m * ↑b = (t * ↑n - (s * ↑m + t * ↑n)) * ↑a + s * ↑m * ↑b
Tactic:
rw [h]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7_aux
Proof state before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ (t * ↑n - (s * ↑m + t * ↑n)) * ↑a + s * ↑m * ↑b = ↑m * (s * (↑b - ↑a))
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set s : Int := gcd_c1 m n
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set t : Int := gcd_c2 m n
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h4 : s * m + t * n = gcd m n := gcd_lin_comb n m
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
define at h1
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [h1, Nat.cast_one] at h4
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set x : Int := t * n * a + s * m * b
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h5 : x ≡ a (MOD m) := Lemma_7_4_7_aux h4 a b
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [add_comm] at h4
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h6 : s * m * b + t * n * a ≡ b (MOD n) :=
  Lemma_7_4_7_aux h4 b a
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h7 : s * m * b + t * n * a = x := by ring
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [h7] at h6
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h8 : m * n ≠ 0 := mul_ne_zero (NeZero.ne m) (NeZero.ne n)
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : m * n ≠ 0
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Theorem: HTPI.Lemma_7_4_7
Proof state before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : m * n ≠ 0
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [←neZero_iff] at h8
Proof state after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)