Theorem: Usa1982P4.some_useful_mod_lemma (Compfiles/Usa1982P4.lean)

State before:
⊢ ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → d ^ n ≡ d ^ a [MOD c]
Tactic:
intros n a b c d h1 h2
State after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
⊢ d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
wlog h : n ≤ a with H
State after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]

n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]

State before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
have han : a ≤ n := (Nat.le_total n a).resolve_left h
State after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ n ≡ d ^ a [MOD c]

State before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
symm
State after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ a ≡ d ^ n [MOD c]

State before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ a ≡ d ^ n [MOD c]
Tactic:
apply H a n b c d h1.symm h2 han
State after:
no goals

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [(by simp : d ^ n = 1 * d ^ n)]
State after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ 1 * d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
have ann : a = (a - n + n) := by exact (Nat.sub_eq_iff_eq_add h).mp rfl
State after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [←(zero_add n : 0 + n = n)] at h1
State after:
n a b c d : ℕ
h1 : 0 + n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h1 : 0 + n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [ann] at h1
State after:
n a b c d : ℕ
h1 : 0 + n ≡ a - n + n [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h1 : 0 + n ≡ a - n + n [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
apply Nat.ModEq.add_right_cancel' at h1
State after:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ a [MOD c]

State before:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [ann, pow_add]
State after:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ (a - n) * d ^ n [MOD c]

State before:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ (a - n) * d ^ n [MOD c]
Tactic:
apply Nat.ModEq.mul
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]
Tactic:
swap
State after:
case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

State before:
case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Tactic:
rfl
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Tactic:
unfold Nat.ModEq
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Tactic:
unfold Nat.ModEq at h2
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Tactic:
rw [←(Nat.div_add_mod' (a - n) b)]
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + (a - n) % b) % c

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + (a - n) % b) % c
Tactic:
rw [←h1]
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + 0 % b) % c

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + 0 % b) % c
Tactic:
simp only [Nat.zero_mod, add_zero]
State after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b) % c

State before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b) % c
Tactic:
rw [mul_comm, pow_mul, Nat.pow_mod, h2, ←Nat.pow_mod, one_pow]
State after:
no goals

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n = 1 * d ^ n
Tactic:
simp
State after:
no goals

State before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ a = a - n + n
Tactic:
exact (Nat.sub_eq_iff_eq_add h).mp rfl
State after:
no goals