Theorem: div_of_qpoly_div (FormalBook/Chapter_06.lean)

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
H : q ^ k - 1 ∣ q ^ n - 1
⊢ k ∣ n
Tactic:
revert H
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
⊢ q ^ k - 1 ∣ q ^ n - 1 → k ∣ n

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
⊢ q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
revert hn
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
apply Nat.strongInductionOn n
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ ∀ (n : ℕ), (∀ m < n, 0 < m → q ^ k - 1 ∣ q ^ m - 1 → k ∣ m) → 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ ∀ (n : ℕ), (∀ m < n, 0 < m → q ^ k - 1 ∣ q ^ m - 1 → k ∣ m) → 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
intro m h hm H
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
⊢ k ∣ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
⊢ k ∣ m
Tactic:
have hq' := zero_lt_of_lt hq
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
⊢ k ∣ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
⊢ k ∣ m
Tactic:
by_cases hkeqm : k = m
State after:
case pos
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : k = m
⊢ k ∣ m

case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
⊢ k ∣ m
Tactic:
have hkm : k ≤ m := by
  have : 0 < q ^ m - 1 := by
    have : 1 < q ^ m := by
      calc
        _ < q := hq
        _ = q^1 := (Nat.pow_one q).symm
        _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
    exact Nat.sub_pos_of_lt this
  have : q ^ k - 1 ≤ q ^ m - 1 := Nat.le_of_dvd this H
  have :  q ^ k ≤ q ^ m  := by
    zify at this
    simp at this
    simpa [Nat.sub_add_cancel <| one_le_pow m q hq'] using this
  exact (pow_le_pow_iff_right hq).mp this
State after:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ k ∣ m
Tactic:
have : q ^ m - 1 = q^(m - k)*(q ^ k - 1) + (q^(m - k) - 1) := by
  zify
  simp [one_le_pow m q hq', one_le_pow k q hq', one_le_pow (m - k) q hq']
  push_cast
  rw [mul_sub, mul_one]
  ring_nf
  simp only [ge_iff_le, add_right_inj]
  exact (pow_sub_mul_pow (q : ℤ) hkm).symm
State after:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ k ∣ m
Tactic:
have h1 : q ^ k - 1 ∣ q ^ (m - k) - 1 := by
  refine' (@Nat.dvd_add_iff_right (q ^ k - 1 ) (q ^ (m - k) * (q ^ k - 1)) (q ^ (m - k) - 1) _ ).mpr _
  exact Nat.dvd_mul_left (q ^ k - 1) (q ^ (m - k))
  rw [← this]
  exact H
State after:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ∣ m
Tactic:
have hmk : m - k < m := by
  zify
  rw [cast_sub]
  linarith
  exact hkm
State after:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
⊢ k ∣ m
Tactic:
have h0mk : 0 < m - k := by exact Nat.sub_pos_of_lt <| Nat.lt_of_le_of_ne hkm hkeqm
State after:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
h0mk : 0 < m - k
⊢ k ∣ m

State before:
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
h0mk : 0 < m - k
⊢ k ∣ m
Tactic:
convert Nat.dvd_add_self_right.mpr (h (m - k) hmk h0mk h1)
State after:
case h.e'_4
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
h0mk : 0 < m - k
⊢ m = m - k + k

State before:
case h.e'_4
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
h0mk : 0 < m - k
⊢ m = m - k + k
Tactic:
exact Nat.eq_add_of_sub_eq hkm rfl
State after:
no goals

State before:
case pos
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : k = m
⊢ k ∣ m
Tactic:
exact Eq.dvd hkeqm
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
⊢ k ≤ m
Tactic:
have : 0 < q ^ m - 1 := by
  have : 1 < q ^ m := by
    calc
      _ < q := hq
      _ = q^1 := (Nat.pow_one q).symm
      _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
  exact Nat.sub_pos_of_lt this
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this : 0 < q ^ m - 1
⊢ k ≤ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this : 0 < q ^ m - 1
⊢ k ≤ m
Tactic:
have : q ^ k - 1 ≤ q ^ m - 1 := Nat.le_of_dvd this H
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : q ^ k - 1 ≤ q ^ m - 1
⊢ k ≤ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : q ^ k - 1 ≤ q ^ m - 1
⊢ k ≤ m
Tactic:
have :  q ^ k ≤ q ^ m  := by
  zify at this
  simp at this
  simpa [Nat.sub_add_cancel <| one_le_pow m q hq'] using this
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝¹ : 0 < q ^ m - 1
this✝ : q ^ k - 1 ≤ q ^ m - 1
this : q ^ k ≤ q ^ m
⊢ k ≤ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝¹ : 0 < q ^ m - 1
this✝ : q ^ k - 1 ≤ q ^ m - 1
this : q ^ k ≤ q ^ m
⊢ k ≤ m
Tactic:
exact (pow_le_pow_iff_right hq).mp this
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
⊢ 0 < q ^ m - 1
Tactic:
have : 1 < q ^ m := by
  calc
    _ < q := hq
    _ = q^1 := (Nat.pow_one q).symm
    _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this : 1 < q ^ m
⊢ 0 < q ^ m - 1

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this : 1 < q ^ m
⊢ 0 < q ^ m - 1
Tactic:
exact Nat.sub_pos_of_lt this
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
⊢ 1 < q ^ m
Tactic:
calc
  _ < q := hq
  _ = q^1 := (Nat.pow_one q).symm
  _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : q ^ k - 1 ≤ q ^ m - 1
⊢ q ^ k ≤ q ^ m
Tactic:
zify at this
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : ↑(q ^ k - 1) ≤ ↑(q ^ m - 1)
⊢ q ^ k ≤ q ^ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : ↑(q ^ k - 1) ≤ ↑(q ^ m - 1)
⊢ q ^ k ≤ q ^ m
Tactic:
simp at this
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : q ^ k ≤ q ^ m - 1 + 1
⊢ q ^ k ≤ q ^ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
this✝ : 0 < q ^ m - 1
this : q ^ k ≤ q ^ m - 1 + 1
⊢ q ^ k ≤ q ^ m
Tactic:
simpa [Nat.sub_add_cancel <| one_le_pow m q hq'] using this
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
Tactic:
zify
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑(q ^ m - 1) = ↑q ^ (m - k) * ↑(q ^ k - 1) + ↑(q ^ (m - k) - 1)

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑(q ^ m - 1) = ↑q ^ (m - k) * ↑(q ^ k - 1) + ↑(q ^ (m - k) - 1)
Tactic:
simp [one_le_pow m q hq', one_le_pow k q hq', one_le_pow (m - k) q hq']
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m - 1 = ↑q ^ (m - k) * (↑q ^ k - 1) + (↑q ^ (m - k) - 1)

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m - 1 = ↑q ^ (m - k) * (↑q ^ k - 1) + (↑q ^ (m - k) - 1)
Tactic:
rw [mul_sub, mul_one]
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m - 1 = ↑q ^ (m - k) * ↑q ^ k - ↑q ^ (m - k) + (↑q ^ (m - k) - 1)

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m - 1 = ↑q ^ (m - k) * ↑q ^ k - ↑q ^ (m - k) + (↑q ^ (m - k) - 1)
Tactic:
ring_nf
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ -1 + ↑q ^ m = -1 + ↑q ^ (m - k) * ↑q ^ k

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ -1 + ↑q ^ m = -1 + ↑q ^ (m - k) * ↑q ^ k
Tactic:
simp only [ge_iff_le, add_right_inj]
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m = ↑q ^ (m - k) * ↑q ^ k

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
⊢ ↑q ^ m = ↑q ^ (m - k) * ↑q ^ k
Tactic:
exact (pow_sub_mul_pow (q : ℤ) hkm).symm
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) - 1
Tactic:
refine' (@Nat.dvd_add_iff_right (q ^ k - 1 ) (q ^ (m - k) * (q ^ k - 1)) (q ^ (m - k) - 1) _ ).mpr _
State after:
case refine'_1
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1)

case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)

State before:
case refine'_1
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1)

case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
Tactic:
exact Nat.dvd_mul_left (q ^ k - 1) (q ^ (m - k))
State after:
case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)

State before:
case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
Tactic:
rw [← this]
State after:
case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ m - 1

State before:
case refine'_2
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
⊢ q ^ k - 1 ∣ q ^ m - 1
Tactic:
exact H
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ m - k < m
Tactic:
zify
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ ↑(m - k) < ↑m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ ↑(m - k) < ↑m
Tactic:
rw [cast_sub]
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ ↑m - ↑k < ↑m

R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ≤ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ ↑m - ↑k < ↑m

R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ≤ m
Tactic:
linarith
State after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ≤ m

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
⊢ k ≤ m
Tactic:
exact hkm
State after:
no goals

State before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
⊢ 0 < m - k
Tactic:
exact Nat.sub_pos_of_lt <| Nat.lt_of_le_of_ne hkm hkeqm
State after:
no goals