awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m k : ℕ
P : ℕ → Prop
inst : DecidablePred P
zero : ∀ {m : ℕ}, findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
have succ : ∀ (k : ℕ) (ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) {m : ℕ},
  findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: induction k generalizing m with
  | zero =>
    rw [eq_comm, Iff.comm]
    simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩
  | succ k ihk =>
    by_cases hk : P (k + 1)
    · rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]
    · rw [findGreatest_of_not hk, ihk]
      grind
Cleared hypotheses: m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ 0 < findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
have rw : (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
Tactic: rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
have push : (Exists fun ⦃n : ℕ⦄ ↦ 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)
have pos : ∀ (h : findGreatest P n = 0), P (findGreatest P n)
Tactic: by_cases h : Nat.findGreatest P n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
pos : ∀ (h : findGreatest P n = 0), P (findGreatest P n)
⊢ P (findGreatest P n)
have neg : ∀ (h : ¬findGreatest P n = 0), P (findGreatest P n)
Tactic: by_cases h : Nat.findGreatest P n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)
have pos : ∀ (hmb : 0 ≤ n) (hm : P 0), P (findGreatest P n)
Tactic: cases m
Cleared hypotheses: m, hmb, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
pos : ∀ (hmb : 0 ≤ n) (hm : P 0), P (findGreatest P n)
⊢ P (findGreatest P n)
have pos₁ : ∀ (n_1 : ℕ) (hmb : n_1 + 1 ≤ n) (hm : P (n_1 + 1)), P (findGreatest P n)
Tactic: cases m
Cleared hypotheses: m, hmb, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
⊢ findGreatest P m ≤ if P (m_1 + 1) then m_1 + 1 else findGreatest P m_1
have pos : P (m_1 + 1) → findGreatest P m ≤ m_1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
pos : P (m_1 + 1) → findGreatest P m ≤ m_1 + 1
⊢ findGreatest P m ≤ if P (m_1 + 1) then m_1 + 1 else findGreatest P m_1
have neg : ¬P (m_1 + 1) → findGreatest P m ≤ findGreatest P m_1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n : ℕ
hmn : m ≤ n
⊢ findGreatest P m ≤ findGreatest P n
have refl : findGreatest P m ≤ findGreatest P m
Tactic: induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n : ℕ
hmn : m ≤ n
refl : findGreatest P m ≤ findGreatest P m
⊢ findGreatest P m ≤ findGreatest P n
have step : ∀ {m_1 : ℕ} (hmk : m.le m_1) (ih : findGreatest P m ≤ findGreatest P m_1), findGreatest P m ≤ findGreatest P m_1.succ
Tactic: induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
have pos : ∀ (h : P (n + 1)), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Tactic: by_cases h : P (n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
pos : ∀ (h : P (n + 1)), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
have neg : ∀ (h : ¬P (n + 1)), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Tactic: by_cases h : P (n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
have pos : n + 1 ≤ findGreatest Q (n + 1)
Tactic: rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
pos : n + 1 ≤ findGreatest Q (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
have pos₁ : n + 1 ≤ n + 1
Tactic: rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
have neg : findGreatest P n ≤ findGreatest Q (n + 1)
Tactic: rw [findGreatest_of_not h]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
⊢ findGreatest P n ≤ findGreatest Q n
have zero : findGreatest P 0 ≤ findGreatest P 0
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
zero : findGreatest P 0 ≤ findGreatest P 0
⊢ findGreatest P n ≤ findGreatest Q n
have succ : ∀ (n : ℕ) (hn : findGreatest P n ≤ findGreatest Q n), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inl : (HPow.hPow (α := ℕ) 0 c - 1) % (HPow.hPow (α := ℕ) 0 b - 1) = HPow.hPow (α := ℕ) 0 (c % b) - 1
Tactic: rcases eq_zero_or_pos a with rfl | ha0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
inl : (HPow.hPow (α := ℕ) 0 c - 1) % (HPow.hPow (α := ℕ) 0 b - 1) = HPow.hPow (α := ℕ) 0 (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : ∀ (ha0 : a > 0), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Tactic: rcases eq_zero_or_pos a with rfl | ha0
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
⊢ (HPow.hPow (α := ℕ) 0 c - 1) % (HPow.hPow (α := ℕ) 0 b - 1) = HPow.hPow (α := ℕ) 0 (c % b) - 1
have inl : HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
  HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
Tactic: simp [zero_pow_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have pos₂ : ¬c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
pos₂ : ¬c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have neg₂ : ¬c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
pos₂ : ¬c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg₂ : ¬c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have pos₃ : ¬c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
pos₂ : ¬c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg₂ : ¬c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₃ : ¬c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
have neg₃ : ¬c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : ∀ (ha0 : succ 0 > 0), (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1
Tactic: rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1
Cleared hypotheses: a, ha0
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
inr : ∀ (ha0 : succ 0 > 0), (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr₁ : ∀ (ha1 : succ 0 < a), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Tactic: rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : (a ^ c - 1) % (HPow.hPow (β := ℕ) a 0 - 1) = a ^ (c % 0) - 1
Tactic: rcases eq_zero_or_pos b with rfl | hb0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
inr : (a ^ c - 1) % (HPow.hPow (β := ℕ) a 0 - 1) = a ^ (c % 0) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr₁ : ∀ (hb0 : b > 0), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Tactic: rcases eq_zero_or_pos b with rfl | hb0
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : ∀ (h : c < b), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Tactic: rcases lt_or_ge c b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
inr : ∀ (h : c < b), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr₁ : ∀ (h : b ≤ c), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Tactic: rcases lt_or_ge c b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : a ^ c - 1 < a ^ b - 1
Tactic: rw [mod_eq_of_lt, mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 < a ^ b - 1
have inr : a ^ c < a ^ b
Tactic: rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₄ : (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
    (a ^ b - 1) =
  a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₄ :
  (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₅ : (a ^ (c - b) % (a ^ b - 1) * 0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₄ :
  (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1
rw₅ :
  (a ^ (c - b) % (a ^ b - 1) * 0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₆ : (0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₄ :
  (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1
rw₅ :
  (a ^ (c - b) % (a ^ b - 1) * 0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₆ : (0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₇ : (0 + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Tactic: rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]