internlm/Lean-Github huggingface dataset:
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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)
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof 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)
Theorem: div_of_qpoly_div
Proof 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']
Proof 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)
Theorem: div_of_qpoly_div
Proof 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]
Proof 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)
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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]
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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 _
Proof 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)
Theorem: div_of_qpoly_div
Proof 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))
Proof 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)
Theorem: div_of_qpoly_div
Proof 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]
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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]
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof 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
Theorem: div_of_qpoly_div
Proof 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
Proof state after:
no goals