awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
isTrue :
  v ≤ u →
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
isFalse :
  ¬v ≤ u →
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) =
      HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
⊢ (if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)

Tactic:
split
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
isTrue : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isTrue₁ : HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) < (↑n : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)

Tactic:
rw [Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) < (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
isFalse : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
isFalse₁ : HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) < (↑n : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)

Tactic:
rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt, Int.emod_eq_add_self_emod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) < (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
rw :
  (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
⊢ (↑(↑(u + v) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)

Tactic:
rw [Fin.add_def]

Premises used: Fin.add_def
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
isTrue :
  (↑u : ℕ) + (↑v : ℕ) < n →
    (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isFalse :
  ¬(↑u : ℕ) + (↑v : ℕ) < n →
    (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
      HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)

Tactic:
split
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
isTrue : (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isTrue₁ : LE.le (α := ℤ) 0 (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ)
isTrue₂ : LT.lt (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt, Int.natCast_emod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
⊢ (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
⊢ LE.le (α := ℤ) 0 (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
⊢ LT.lt (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
isFalse :
  HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
isFalse₁ : 0 ≤ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)
isFalse₂ : HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)

Tactic:
rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt, Int.natCast_emod, Int.emod_eq_sub_self_emod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
⊢ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
⊢ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(u + v) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ (↑1 : ℕ) = 1 % n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
simp : 1 < n ↔ 2 ≤ n
⊢ Nontrivial (Fin n) ↔ 2 ≤ n

Tactic:
simp [← not_subsingleton_iff_nontrivial, subsingleton_iff_le_one]

Premises used: Fin.subsingleton_iff_le_one, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
⊢ 1 < n ↔ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
inst : n.AtLeastTwo
⊢ Nontrivial (Fin n)

Tactic:
nontrivial_iff_two_le.2 Nat.AtLeastTwo.one_lt

Premises used: Iff.mpr, Nat.AtLeastTwo.one_lt, Fin.nontrivial_iff_two_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
h : 2 < n
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
h : 2 < n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by lia⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
h : 2 < n
this : NeZero n
rcases : ∀ (i : ℕ) (hi : i < n), ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ j
⊢ ∃ (k : Fin n), k ≠ i ∧ k ≠ j

Tactic:
rcases i with ⟨i, hi⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
j : Fin n
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
rcases : ∀ (j : ℕ) (hj : j < n), ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩
⊢ ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ j

Tactic:
rcases j with ⟨j, hj⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
simp_rw : ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
⊢ ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩

Tactic:
simp_rw [← Fin.val_ne_iff]

Premises used: Fin.val_ne_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
pos : ∀ (h0 : 0 ≠ i ∧ 0 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
neg : ∀ (h0 : ¬(0 ≠ i ∧ 0 ≠ j)), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
by_cases h0 : 0 ≠ i ∧ 0 ≠ j
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
⟨0, h0⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
exact ⟨0, h0⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
pos : ∀ (h1 : 1 ≠ i ∧ 1 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
neg : ∀ (h1 : ¬(1 ≠ i ∧ 1 ≠ j)), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
by_cases h1 : 1 ≠ i ∧ 1 ≠ j
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ 1 < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
exact ⟨⟨1, by lia⟩, h1⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
neg : (↑(⟨2, ⋯⟩ : Fin n) : ℕ) ≠ i ∧ (↑(⟨2, ⋯⟩ : Fin n) : ℕ) ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j

Tactic:
refine ⟨⟨2, by lia⟩, ?_⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 ≠ i ∧ 2 ≠ j

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n_1 m n : ℕ
rw : NeZero (n + 1)
⊢ NeZero (1 + n)

Tactic:
rw [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n_1 m n : ℕ
⊢ NeZero (n + 1)

Tactic:
infer_instance
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) default 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
rw : ((↑a : ℕ) + (↑b : ℕ)) % n = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₁ :
  (if n ≤ (↑a : ℕ) % n + (↑b : ℕ) % n then (↑a : ℕ) % n + (↑b : ℕ) % n - n else (↑a : ℕ) % n + (↑b : ℕ) % n) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₂ :
  (if n ≤ (↑a : ℕ) + (↑b : ℕ) % n then (↑a : ℕ) + (↑b : ℕ) % n - n else (↑a : ℕ) + (↑b : ℕ) % n) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₃ rw₄ :
  (if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
⊢ (↑(a + b) : ℕ) = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)

Tactic:
rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]

Premises used: Fin.val_add, Fin.isLt, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
huv : (↑a : ℕ) + (↑b : ℕ) < n
rw : ((↑a : ℕ) + (↑b : ℕ)) % n = (↑a : ℕ) + (↑b : ℕ)
⊢ (↑(a + b) : ℕ) = (↑a : ℕ) + (↑b : ℕ)

Tactic:
rw [val_add]

Premises used: Fin.val_add
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
huv : (↑a : ℕ) + (↑b : ℕ) < n
⊢ ((↑a : ℕ) + (↑b : ℕ)) % n = (↑a : ℕ) + (↑b : ℕ)

Tactic:
simp [Nat.mod_eq_of_lt huv]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
isTrue : b ≤ a → (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
isFalse : ¬b ≤ a → (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑(if b ≤ a then 0 else n) : ℤ)

Tactic:
split
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : b ≤ a
isTrue isTrue₁ :
  LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) →
    (if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
      else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) =
      HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)

Tactic:
fin_omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : ¬b ≤ a
isFalse isFalse₁ :
  ¬LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) →
    (if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
      else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) =
      HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
fin_omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
⊢ (↑(j - i) : ℕ) < n - (↑i : ℕ)

Tactic:
simp [sub_val_of_le hij, Nat.sub_lt_sub_right hij j.isLt]

Premises used: Fin.sub_val_of_le, Nat.sub_lt_sub_right, Fin.isLt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n_1 m n : ℕ
i j : Fin n
hij : i < j
⊢ n - (↑i : ℕ) ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ (j - i).castLT ⋯ ≠ 0

Tactic:
Ne.symm (ne_of_val_ne ?_)

Premises used: Fin.ne_of_val_ne, Ne.symm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i < j
refine : (↑0 : ℕ) ≠ (↑((j - i).castLT ⋯) : ℕ)
⊢ (j - i).castLT ⋯ ≠ 0

Tactic:
refine Ne.symm (ne_of_val_ne ?_)

Premises used: Fin.ne_of_val_ne, Ne.symm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i < j
simp : ¬0 = (↑j : ℕ) - (↑i : ℕ)
⊢ (↑0 : ℕ) ≠ (↑((j - i).castLT ⋯) : ℕ)

Tactic:
simp [coe_sub_iff_le.mpr (Fin.le_of_lt hij)]

Premises used: Iff.mpr, Fin.le_of_lt, Fin.coe_sub_iff_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ ¬0 = (↑j : ℕ) - (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ NeZero n

Tactic:
have := i.neZero
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin n
this : NeZero n
hi : i ≠ 0
obtain : ∀ (n : ℕ) {i : Fin n.succ} (this : NeZero n.succ) (hi : i ≠ 0), (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
rw : (↑i : ℕ) - (↑1 : ℕ) = (↑i : ℕ) - 1
rw₁ : (↑i : ℕ) - 1 % n.succ = (↑i : ℕ) - 1
rw₂ rw₃ : (↑i : ℕ) - 1 = (↑i : ℕ) - 1
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1

Tactic:
rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]

Premises used: Fin.sub_val_of_le, Iff.mpr, Fin.val_one', Fin.one_le_of_ne_zero, nontrivial_of_ne, Nat.mod_eq_of_lt, Iff.mp, OfNat.ofNat, Nat.succ_le_iff, Fin.nontrivial_iff_two_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : ℕ
⊢ Fin.ofNat n a = (↑a : Fin n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
a n : ℕ
inst : NeZero n
⊢ (↑(↑a : Fin n) : ℕ) = a % n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : ℕ
h : a < n
⊢ (↑(↑a : Fin n) : ℕ) = a

Tactic:
Nat.mod_eq_of_lt h

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin n
⊢ (↑(↑a : ℕ) : Fin n) = a

Tactic:
have := a.neZero
  Fin.ext <| val_cast_of_lt a.isLt

Premises used: Fin.isLt, Fin.neZero, Fin.ext, Fin.val_cast_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
h : (↑(↑n : Fin n) : ℕ) = (↑0 : ℕ)
⊢ Eq (α := Fin n) (↑n : Fin n) 0

Tactic:
ext
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ (↑(↑n : Fin n) : ℕ) = (↑0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Basic
Goal:
a n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (↑a : Fin n) 0 ↔ n ∣ a

Tactic:
simp [Fin.ext_iff, Nat.dvd_iff_mod_eq_zero]

Premises used: Fin.ext_iff, Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (↑0 : Fin n) 0

Tactic:
simp
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : (↑(↑n : Fin (n + 1)) : ℕ) = (↑(last n) : ℕ)
⊢ (↑n : Fin (n + 1)) = last n

Tactic:
ext
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
⊢ (↑(↑n : Fin (n + 1)) : ℕ) = (↑(last n) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Basic
Goal:
m n : ℕ
h : m < n
⊢ have this := ⋯;
  (↑m : Fin n) = (⟨m, h⟩ : Fin n)

Tactic:
Fin.val_inj.mp (Nat.mod_eq_of_lt h)

Premises used: Nat.mod_eq_of_lt, Iff.mp, Fin.val_inj
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
h : 1 < n
⊢ have this := ⋯;
  1 = (⟨1, h⟩ : Fin n)

Tactic:
Fin.val_inj.mp (Nat.mod_eq_of_lt h)

Premises used: Nat.mod_eq_of_lt, Iff.mp, Fin.val_inj
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
rw : i ≤ last n
⊢ i ≤ (↑n : Fin (n + 1))

Tactic:
rw [Fin.natCast_eq_last]

Premises used: Fin.natCast_eq_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n

Tactic:
Fin.le_last i

Premises used: Fin.le_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n

Tactic:
exact Fin.le_last i

Premises used: Fin.le_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ a < n.succ

Tactic:
rw [← Nat.lt_succ_iff] at han hbn

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
han₁ : a < n.succ
⊢ b < n.succ

Tactic:
rw [← Nat.lt_succ_iff] at han hbn

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ LE.le (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a ≤ b

Tactic:
simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

Premises used: Nat.mod_eq_of_lt, Fin.val_fin_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ LT.lt (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a < b

Tactic:
simp [lt_def, Nat.mod_eq_of_lt, han, hbn]

Premises used: Nat.mod_eq_of_lt, Fin.lt_def
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
hbn : b ≤ n
hab : a ≤ b
⊢ LE.le (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1))

Tactic:
(natCast_le_natCast (hab.trans hbn) hbn).2 hab

Premises used: Iff.mpr, LE.le.trans, Fin.natCast_le_natCast
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a b : ℕ
hbn : b ≤ n
hab : a < b
⊢ LT.lt (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1))

Tactic:
(natCast_lt_natCast (hab.le.trans hbn) hbn).2 hab

Premises used: Iff.mpr, LT.lt.le, LE.le.trans, Fin.natCast_lt_natCast
-- Module: Mathlib.Data.Fin.Basic
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ℕ
h₁ : (↑(castLE h (↑a : Fin m)) : ℕ) = (↑(↑(a % m) : Fin n) : ℕ)
⊢ castLE h (↑a : Fin m) = (↑(a % m) : Fin n)

Tactic:
ext
-- Module: Mathlib.Data.Fin.Basic
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ℕ
h₁ h₂ : a % m = a % m
⊢ a % m = a % m % n

Tactic:
rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]

Premises used: Nat.mod_eq_of_lt, Nat.mod_lt, Nat.pos_of_neZero, lt_of_lt_of_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
h : (↑i.rev.modNat : ℕ) = (↑i.modNat.rev : ℕ)
⊢ i.rev.modNat = i.modNat.rev

Tactic:
ext
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
⊢ (↑i : ℕ) % n + 1 ≤ n

Tactic:
have H₁ : i % n + 1 ≤ n := i.modNat.is_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
⊢ (↑i : ℕ) / n < m

Tactic:
have H₂ : i / n < m := i.divNat.is_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
rw rw₁ : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) + 1)) % n
⊢ (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n

Tactic:
rw [Nat.div_add_mod']

Premises used: Nat.div_add_mod'
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
rw : n ≤ (m - (↑i : ℕ) / n) * n
⊢ (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n = ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n

Tactic:
rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]

Premises used: Nat.sub_sub, Nat.mul_sub_right_distrib, Nat.add_assoc, Nat.sub_add_sub_cancel, Nat.one_mul
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ n ≤ (m - (↑i : ℕ) / n) * n

Tactic:
Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

Premises used: Nat.le_sub_of_add_le', Nat.le_mul_of_pos_left
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ n ≤ (m - (↑i : ℕ) / n) * n

Tactic:
exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

Premises used: Nat.le_sub_of_add_le', Nat.le_mul_of_pos_left
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
rw : n - ((↑i : ℕ) % n + 1) < n
⊢ ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n = n - ((↑i : ℕ) % n + 1)

Tactic:
rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]

Premises used: Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ n - ((↑i : ℕ) % n + 1) < n

Tactic:
i.modNat.rev.is_lt

Premises used: Fin.is_lt, Fin.modNat, Fin.rev
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ n - ((↑i : ℕ) % n + 1) < n

Tactic:
exact i.modNat.rev.is_lt

Premises used: Fin.is_lt, Fin.modNat, Fin.rev
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
n₁ : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n
n₂ : (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n = ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n
n₃ : ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n = n - ((↑i : ℕ) % n + 1)
⊢ (↑i.rev.modNat : ℕ) = n - ((↑i.modNat : ℕ) + 1)

Tactic:
calc
    (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
    _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
    _ = n - (i % n + 1) := by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Fin.val, HMod.hMod, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
obtain : ∀ (i : ℕ) (hi : i < n), motive ⟨i, hi⟩
⊢ motive i

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
j : ℕ
hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩
hi : j < n
⊢ motive ⟨j, hi⟩

Tactic:
h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)

Premises used: Fin.mk, Fin.val, _private.0.Fin.strong_induction_on.match_1
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
j : ℕ
hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩
hi : j < n
⊢ motive ⟨j, hi⟩

Tactic:
exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : ℕ
hi : i < n
h₁ : ∀ (j : ℕ) (hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩) (hi : j < n), motive ⟨j, hi⟩
⊢ motive ⟨i, hi⟩

Tactic:
induction i using Nat.strong_induction_on with
  | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
mp : ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
mpr : (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f
⊢ ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

Tactic:
constructor
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f
i : Fin n
⊢ r (f i.castSucc) (f i.succ)

Tactic:
H i.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ