internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Euler's_theorem
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
have h2 : [a]_m ^ (phi m) = [1]_m := Theorem_7_4_2 h1
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a]_m ^ phi m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Theorem: HTPI.Euler's_theorem
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a]_m ^ phi m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
rewrite [Exercise_7_4_5_Nat m a (phi m)] at h2
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a ^ phi m]_m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Theorem: HTPI.Euler's_theorem
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a ^ phi m]_m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
show a ^ (phi m) ≡ 1 (MOD m) from (cc_eq_iff_congr _ _ _).ltr h2
Proof state after:
no goals
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
⊢ phi p = p - 1
Tactic:
have h2 : 1 ≤ p := prime_pos h1
Proof state after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
⊢ phi p = p - 1
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
⊢ phi p = p - 1
Tactic:
have h3 : p - 1 + 1 = p := Nat.sub_add_cancel h2
Proof state after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ phi p = p - 1
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ phi p = p - 1
Tactic:
have h4 : p - 1 < p := by linarith
Proof state after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
⊢ phi p = p - 1
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
⊢ phi p = p - 1
Tactic:
have h5 : num_rp_below p (p - 1 + 1) = p - 1 :=
  num_rp_prime h1 (p - 1) h4
Proof state after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p (p - 1 + 1) = p - 1
⊢ phi p = p - 1
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p (p - 1 + 1) = p - 1
⊢ phi p = p - 1
Tactic:
rewrite [h3] at h5
Proof state after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p p = p - 1
⊢ phi p = p - 1
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p p = p - 1
⊢ phi p = p - 1
Tactic:
show phi p = p - 1 from h5
Proof state after:
no goals
Theorem: HTPI.phi_prime
Proof state before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ p - 1 < p
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2_Int
Proof state before:
a c : ℕ
b : ℤ
h1 : ↑c ∣ ↑a * b
h2 : rel_prime a c
⊢ ↑c ∣ b
Tactic:
rewrite [Int.coe_nat_dvd_left, Int.natAbs_mul,
  Int.natAbs_ofNat] at h1
Proof state after:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ ↑c ∣ b
Theorem: HTPI.Theorem_7_2_2_Int
Proof state before:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ ↑c ∣ b
Tactic:
rewrite [Int.coe_nat_dvd_left]
Proof state after:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ c ∣ Int.natAbs b
Theorem: HTPI.Theorem_7_2_2_Int
Proof state before:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ c ∣ Int.natAbs b
Tactic:
show c ∣ Int.natAbs b from Theorem_7_2_2 h1 h2
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) ↔ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) → a ≡ b (MOD m) ∧ a ≡ b (MOD n)

case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n) → a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) → a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
assume h2 : a ≡ b (MOD m * n)
Proof state after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
obtain (j : Int) (h3 : a - b = (m * n) * j) from h2
Proof state after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
apply And.intro
Proof state after:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m)

case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m)
Tactic:
apply Exists.intro (n * j)
Proof state after:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑m * (↑n * j)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑m * (↑n * j)
Tactic:
show a - b = m * (n * j) from
  calc a - b
    _ = m * n * j := h3
    _ = m * (n * j) := by ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ ↑m * ↑n * j = ↑m * (↑n * j)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD n)
Tactic:
apply Exists.intro (m * j)
Proof state after:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑n * (↑m * j)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑n * (↑m * j)
Tactic:
show a - b = n * (m * j) from
  calc a - b
    _ = m * n * j := h3
    _ = n * (m * j) := by ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ ↑m * ↑n * j = ↑n * (↑m * j)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n) → a ≡ b (MOD m * n)
Tactic:
assume h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
⊢ a ≡ b (MOD m * n)
Tactic:
obtain (j : Int) (h3 : a - b = m * j) from h2.left
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
⊢ a ≡ b (MOD m * n)
Tactic:
have h4 : (↑n : Int) ∣ a - b := h2.right
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ a - b
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ a - b
⊢ a ≡ b (MOD m * n)
Tactic:
rewrite [h3] at h4
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
⊢ a ≡ b (MOD m * n)
Tactic:
have h5 : ↑n ∣ j := Theorem_7_2_2_Int h4 h1
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
⊢ a ≡ b (MOD m * n)
Tactic:
obtain (k : Int) (h6 : j = n * k) from h5
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a ≡ b (MOD m * n)
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a ≡ b (MOD m * n)
Tactic:
apply Exists.intro k
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑(m * n) * k
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑(m * n) * k
Tactic:
rewrite [Nat.cast_mul]
Proof state after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑m * ↑n * k
Theorem: HTPI.Lemma_7_4_5
Proof state before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑m * ↑n * k
Tactic:
show a - b = (m * n) * k from
  calc a - b
    _ = m * j := h3
    _ = m * (n * k) := by rw [h6]
    _ = (m * n) * k := by ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ ↑m * j = ↑m * (↑n * k)
Tactic:
rw [h6]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_5
Proof state before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ ↑m * (↑n * k) = ↑m * ↑n * k
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.prime_NeZero
Proof state before:
p : ℕ
h : prime p
⊢ NeZero p
Tactic:
rewrite [neZero_iff]
Proof state after:
p : ℕ
h : prime p
⊢ p ≠ 0
Theorem: HTPI.prime_NeZero
Proof state before:
p : ℕ
h : prime p
⊢ p ≠ 0
Tactic:
define at h
Proof state after:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 0
Theorem: HTPI.prime_NeZero
Proof state before:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h4 : m ^ e ≡ c (MOD p) := Exists.intro t h3
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h5 : [m ^ e]_p = [c]_p := (cc_eq_iff_congr _ _ _).rtl h4
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m ^ e]_p = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m ^ e]_p = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
rewrite [←Exercise_7_4_5_Nat] at h5
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
by_cases h6 : p ∣ m
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)

case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h7 : m ≡ 0 (MOD p) := by
  obtain (j : Nat) (h8 : m = p * j) from h6
  apply Exists.intro (↑j : Int)   rewrite [h8, Nat.cast_mul]
  ring
  done
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h8 : [m]_p = [0]_p := (cc_eq_iff_congr _ _ _).rtl h7
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h9 : 0 < (e * d) := by
  rewrite [h2]
  have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
  linarith
  done
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h11 : [c ^ d]_p = [m]_p :=
  calc [c ^ d]_p
    _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
    _ = ([m]_p ^ e) ^ d := by rw [h5]
    _ = [m]_p ^ (e * d) := by ring
    _ = [0]_p ^ (e * d) := by rw [h8]
    _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
    _ = [0]_p := by rw [h10]
    _ = [m]_p := by rw [h8]
Proof state after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
show c ^ d ≡ m (MOD p)  from (cc_eq_iff_congr _ _ _).ltr h11
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑m ≡ 0 (MOD p)
Tactic:
obtain (j : Nat) (h8 : m = p * j) from h6
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m ≡ 0 (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m ≡ 0 (MOD p)
Tactic:
apply Exists.intro (↑j : Int)
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m - 0 = ↑p * ↑j
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m - 0 = ↑p * ↑j
Tactic:
rewrite [h8, Nat.cast_mul]
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑p * ↑j - 0 = ↑p * ↑j
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑p * ↑j - 0 = ↑p * ↑j
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < e * d
Tactic:
rewrite [h2]
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < (p - 1) * s + 1
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < (p - 1) * s + 1
Tactic:
have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
Proof state after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h10 : 0 ≤ (p - 1) * s
⊢ 0 < (p - 1) * s + 1
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h10 : 0 ≤ (p - 1) * s
⊢ 0 < (p - 1) * s + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑c ^ d]_p = [↑c]_p ^ d
Tactic:
rw [Exercise_7_4_5_Nat]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑c]_p ^ d = ([↑m]_p ^ e) ^ d
Tactic:
rw [h5]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ([↑m]_p ^ e) ^ d = [↑m]_p ^ (e * d)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑m]_p ^ (e * d) = [0]_p ^ (e * d)
Tactic:
rw [h8]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [0 ^ (e * d)]_p = [0]_p
Tactic:
rw [h10]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [0]_p = [↑m]_p
Tactic:
rw [h8]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
Proof state after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h8 : rel_prime p m := rel_prime_symm h7
Proof state after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h9 : NeZero p := prime_NeZero h1
Proof state after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Theorem: HTPI.Lemma_7_5_1
Proof state before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h10 : (1 : Int) ^ s = 1 := by ring
Proof state after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ↑c ^ d ≡ ↑m (MOD p)