awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact H i.castSucc_lt_succ

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

Tactic:
fun H i => Fin.induction (fun h ↦ ?_) ?_

Premises used: Fin.induction, Relator.LiftFun
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
mpr :
  ∀ (H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)) (i : Fin (n + 1)) (h : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i 0),
    r (f i) (f 0)
mpr₁ :
  ∀ (H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)) (i : Fin (n + 1)) (i_1 : Fin n),
    ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f

Tactic:
refine fun H i => Fin.induction (fun h ↦ ?_) ?_
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
h : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i 0
⊢ r (f i) (f 0)

Tactic:
simp at h
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i < j.succ
⊢ i ≤ j.castSucc

Tactic:
rw [← le_castSucc_iff] at hij

Premises used: Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
mpr : ∀ (hij : (↑i : ℕ) = (↑j.castSucc : ℕ)), r (f i) (f j.succ)
mpr₁ : ∀ (hij : (↑i : ℕ) < (↑j.castSucc : ℕ)), r (f i) (f j.succ)
⊢ r (f i) (f j.succ)

Tactic:
obtain hij | hij := (le_def.1 hij).eq_or_lt

Premises used: LE.le.eq_or_lt, Fin.le_def, Iff.mp
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij_1 : i ≤ j.castSucc
hij : (↑i : ℕ) = (↑j.castSucc : ℕ)
mpr :
  ∀ (ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) j.castSucc j.castSucc → r (f j.castSucc) (f j.castSucc))
    (hij : j.castSucc ≤ j.castSucc) (hij : (↑j.castSucc : ℕ) = (↑j.castSucc : ℕ)), r (f j.castSucc) (f j.succ)
⊢ r (f i) (f j.succ)

Tactic:
obtain rfl := Fin.ext hij

Premises used: Fin.ext, rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) j.castSucc j.castSucc → r (f j.castSucc) (f j.castSucc)
hij_1 : j.castSucc ≤ j.castSucc
hij : (↑j.castSucc : ℕ) = (↑j.castSucc : ℕ)
⊢ r (f j.castSucc) (f j.succ)

Tactic:
H _
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) j.castSucc j.castSucc → r (f j.castSucc) (f j.castSucc)
hij_1 : j.castSucc ≤ j.castSucc
hij : (↑j.castSucc : ℕ) = (↑j.castSucc : ℕ)
⊢ r (f j.castSucc) (f j.succ)

Tactic:
exact H _
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij_1 : i ≤ j.castSucc
hij : (↑i : ℕ) < (↑j.castSucc : ℕ)
⊢ r (f i) (f j.succ)

Tactic:
_root_.trans (ihj hij) (H j)

Premises used: trans
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij_1 : i ≤ j.castSucc
hij : (↑i : ℕ) < (↑j.castSucc : ℕ)
⊢ r (f i) (f j.succ)

Tactic:
exact _root_.trans (ihj hij) (H j)

Premises used: trans
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : Fin 1
⊢ n = 0

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Fin.Basic
Goal:
i : Fin 2
hi : i ≠ 0
⊢ i = 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
zero : (↑(-1) : ℕ) = 0
succ : ∀ (n : ℕ), (↑(-1) : ℕ) = n + 1
⊢ (↑(-1) : ℕ) = n

Tactic:
cases n
-- Module: Mathlib.Data.Fin.Basic
Goal:
⊢ (↑(-1) : ℕ) = 0

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

Tactic:
rw [Fin.val_neg', Fin.val_one, Nat.add_one_sub_one, Nat.mod_eq_of_lt]

Premises used: Nat.add_one_sub_one, Fin.val_one, Nat.mod_eq_of_lt, Fin.val_neg'
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
⊢ n + 1 < n + 1 + 1

Tactic:
constructor
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
rw : (↑(last n) : ℕ) - (↑i : ℕ) = (↑i.rev : ℕ)
rw₁ : n - (↑i : ℕ) = (↑i.rev : ℕ)
rw₂ : n - (↑i : ℕ) = n + 1 - ((↑i : ℕ) + 1)
rw₃ rw₄ : n - (↑i : ℕ) = n - (↑i : ℕ)
⊢ (↑(last n - i) : ℕ) = (↑i.rev : ℕ)

Tactic:
rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

Premises used: Iff.mpr, Fin.val_rev, Nat.succ_sub_succ_eq_sub, Fin.coe_sub_iff_le, Fin.val_last, Fin.le_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
zero : ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b), a + 1 ≤ b
succ : ∀ (n : ℕ) {a b : Fin (n + 1 + 1)} (h : a < b), a + 1 ≤ b
⊢ a + 1 ≤ b

Tactic:
cases n
-- Module: Mathlib.Data.Fin.Basic
Goal:
a b : Fin (HAdd.hAdd (α := ℕ) 0 1)
h : a < b
zero zero₁ :
  ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
    (if LT.lt (α := ℤ) (↑((↑a : ℕ) + (↑1 : ℕ)) : ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then
        HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑1 : ℕ) : ℤ)
      else HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑1 : ℕ) : ℤ) - (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) ≤
      (↑(↑b : ℕ) : ℤ)
⊢ a + 1 ≤ b

Tactic:
fin_omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
succ succ₁ :
  ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
    (if LT.lt (α := ℤ) (↑((↑a : ℕ) + 1) : ℤ) (↑(n + 1 + 1) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑1 : ℤ)
      else HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 1 + 1) : ℤ)) ≤
      (↑(↑b : ℕ) : ℤ)
⊢ a + 1 ≤ b

Tactic:
fin_omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ (k : ℕ), (↑b : ℕ) = (↑a : ℕ) + k

Tactic:
Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
obtain : ∀ (k : ℕ) (hk : (↑b : ℕ) = (↑a : ℕ) + k), ∃ (k : Fin n), k ≤ b ∧ b = a + k
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, Fin.val
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
⊢ k ≤ (↑b : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
⊢ k ≤ (↑b : ℕ)

Tactic:
have hkb : k ≤ b := by lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
hkb : k ≤ (↑b : ℕ)
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k

Tactic:
⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩

Premises used: Fin.mk, Fin.is_lt, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
hkb : k ≤ (↑b : ℕ)
refine : b = a + (⟨k, ⋯⟩ : Fin n)
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k

Tactic:
refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
hkb : k ≤ (↑b : ℕ)
⊢ b = a + (⟨k, ⋯⟩ : Fin n)

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

Premises used: Fin.val_add, Fin.ext_iff, Fin.is_lt, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
zero :
  ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b),
    ∃ (k : Fin (HAdd.hAdd (α := ℕ) 0 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
succ : ∀ (n : ℕ) {a b : Fin (n + 1 + 1)} (h : a < b), ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
⊢ ∃ (k : Fin (n + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
cases n
-- Module: Mathlib.Data.Fin.Basic
Goal:
a b : Fin (HAdd.hAdd (α := ℕ) 0 1)
h : a < b
⊢ ∃ (k : Fin (HAdd.hAdd (α := ℕ) 0 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
⊢ ∃ (k : ℕ), (↑b : ℕ) = (↑a : ℕ) + k + 1

Tactic:
Nat.exists_eq_add_of_lt h

Premises used: Nat.exists_eq_add_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
succ : ∀ (k : ℕ) (hk : (↑b : ℕ) = (↑a : ℕ) + k + 1), ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
⊢ ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h

Premises used: Fin.val, Nat.exists_eq_add_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
⊢ k < (↑b : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
⊢ k < (↑b : ℕ)

Tactic:
have hkb : k < b := by lia
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
hkb : k < (↑b : ℕ)
fin_omega fin_omega₁ :
  ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
    (if LT.lt (α := ℤ) (↑(k + 1) : ℤ) (↑(n + 1 + 1) : ℤ) then HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)
      else HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ) - (↑(n + 1 + 1) : ℤ)) ≤
      (↑(↑b : ℕ) : ℤ)
⊢ (⟨k, ⋯⟩ : Fin (n + 1 + 1)) + 1 ≤ b

Tactic:
fin_omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
hkb : k < (↑b : ℕ)
succ : b = a + (⟨k, ⋯⟩ : Fin (n + 1 + 1)) + 1
⊢ ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
hkb : k < (↑b : ℕ)
⊢ b = a + (⟨k, ⋯⟩ : Fin (n + 1 + 1)) + 1

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

Premises used: Fin.val_add, Fin.ext_iff, Fin.is_lt, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin (n + 1)
h : a ≠ 0
⊢ 0 < a

Tactic:
Nat.pos_of_ne_zero (val_ne_of_ne h)

Premises used: Nat.pos_of_ne_zero, Fin.val_ne_of_ne, Nat.mod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin (n + 2)
h : u < v
fin_omega fin_omega₁ :
  ∀ (h : LT.lt (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)),
    (if
          (if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
            else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)) ≤
            (↑(↑v : ℕ) : ℤ) then
        (↑(↑v : ℕ) : ℤ) -
          if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
          else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)
      else
        ((↑(↑v : ℕ) : ℤ) -
            if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
            else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)) +
          (↑(n + 2) : ℤ)) <
      if LE.le (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑v : ℕ) : ℤ) (↑(↑u : ℕ) : ℤ)
      else HSub.hSub (α := ℤ) (↑(↑v : ℕ) : ℤ) (↑(↑u : ℕ) : ℤ) + (↑(n + 2) : ℤ)
⊢ v - (u + 1) < v - u

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin n
h : (↑i : ℕ) + 1 < n
⊢ (↑i : ℕ) + 1 < n

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

Tactic:
simpa [add_def] using Nat.mod_eq_of_lt (by lia)

Premises used: Fin.add_def, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
this : m % (n + m) = m
⊢ NeZero (R := Fin (n + OfNat.ofNat m)) (OfNat.ofNat m)

Tactic:
simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using NeZero.ne m

Premises used: Fin.ext_iff, OfNat.ofNat, neZero_iff, NeZero.ne
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
suffices : m % (n + m) = m
⊢ NeZero (R := Fin (n + OfNat.ofNat m)) (OfNat.ofNat m)

Tactic:
suffices m % (n + m) = m by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using NeZero.ne m
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
h : m < n + m
⊢ m % (n + m) = m

Tactic:
apply Nat.mod_eq_of_lt

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
⊢ m < n + m

Tactic:
simpa using zero_lt_of_ne_zero (NeZero.ne n)

Premises used: Nat.zero_lt_of_ne_zero, NeZero.ne
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
⊢ Eq (α := { i : ℕ // i < n } ↪ ℕ) (Embedding.trans (Equiv.toEmbedding (Equiv.symm equivSubtype)) valEmbedding)
    (Embedding.subtype fun (x : ℕ) ↦ x < n)

Tactic:
rfl

Premises used: Function.Embedding.trans, Function.Embedding.subtype, rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
⊢ Eq (α := (a : Fin n) → Fin (n + 1)) (⇑(succEmb n) : (a : Fin n) → Fin (n + 1)) succ

Tactic:
rfl

Premises used: Fin.succ, rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
m n : ℕ
hmn : m ≤ n
⊢ (⇑(castLEEmb hmn) : (a : Fin m) → Fin n) = castLE hmn

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩

Premises used: Fin.castLEEmb, Nonempty.intro, Iff.intro
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
refine : ∀ (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩
-- Module: Mathlib.Data.Fin.Embedding
Goal:
m : ℕ
h : Nonempty (Fin 0 ↪ Fin m)
⊢ 0 ≤ m

Tactic:
m.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Fin.Embedding
Goal:
m : ℕ
h : Nonempty (Fin 0 ↪ Fin m)
⊢ 0 ≤ m

Tactic:
exact m.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
succ : ∀ (e : Fin (n + 1) ↪ Fin m), n + 1 ≤ m
⊢ n + 1 ≤ m

Tactic:
obtain ⟨e⟩ := h
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
succ : ∀ (m : ℕ) (e : Fin (n + 1) ↪ Fin m.succ), n + 1 ≤ m.succ
⊢ n + 1 ≤ m

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩

Premises used: Iff.mpr, inferInstance, LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, Fin.pos_iff_nonempty, Nonempty.map, DFunLike.coe, rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ

Tactic:
Nat.succ_le_succ <| ihn ⟨?_⟩

Premises used: Nonempty.intro, Nat.succ_le_succ
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
succ : Fin n ↪ Fin m
⊢ n + 1 ≤ m.succ

Tactic:
refine Nat.succ_le_succ <| ihn ⟨?_⟩

Premises used: Nonempty.intro, Nat.succ_le_succ
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
succ :
  ∀ (i j : Fin n)
    (h :
      Eq (α := Fin m) ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) ⋯) i)
        ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) ⋯) j)),
    i = j
⊢ Fin n ↪ Fin m

Tactic:
refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h :
  Eq (α := Fin m) ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) ⋯) i)
    ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) ⋯) j)
⊢ i = j

Tactic:
simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

Premises used: Fin.pred_inj, Fin.succ_inj, EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
zero : ∀ {m : ℕ} (h : Nonempty (Fin 0 ↪ Fin m)), 0 ≤ m
succ :
  ∀ (n : ℕ) (ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m) {m : ℕ} (h : Nonempty (Fin (n + 1) ↪ Fin m)),
    n + 1 ≤ m
⊢ n ≤ m

Tactic:
induction n generalizing m with
  | zero => exact m.zero_le
  | succ n ihn =>
    obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

Premises used: Nat.zero_le, Fin.succ, Fin.pred_inj, Fin.succ_inj, EmbeddingLike.apply_eq_iff_eq, Nat.zero, rfl, Nat.succ_le_succ
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
⊢ Nonempty (Fin m ≃ Fin n) ↔ m = n

Tactic:
⟨fun ⟨e⟩ ↦ le_antisymm (nonempty_embedding_iff.1 ⟨e⟩) (nonempty_embedding_iff.1 ⟨e.symm⟩),
    fun h ↦ h ▸ ⟨.refl _⟩⟩

Premises used: Fin.nonempty_embedding_iff, Eq.rec, Nonempty.intro, le_antisymm, Equiv.toEmbedding, Iff.intro, Iff.mp, _private.0.Fin.equiv_iff_eq.match_1, Equiv.symm, Fin, Equiv.refl, Eq
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
⊢ Eq (α := (a : Fin n) → Fin (n + m)) (⇑(castAddEmb m) : (a : Fin n) → Fin (n + m)) (castAdd m)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
i : Fin n
⊢ (castAddEmb m : (a : Fin n) → Fin (n + m)) i = castAdd m i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
⊢ Eq (α := (a : Fin n) → Fin (n + 1)) (⇑castSuccEmb : (a : Fin n) → Fin (n + 1)) castSucc

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
i : Fin n
⊢ (castSuccEmb : (a : Fin n) → Fin (n + 1)) i = i.castSucc

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m_1 m : ℕ
a b : Fin n
⊢ Eq (α := Fin (n + m)) ((fun (x : Fin n) ↦ x.addNat m) a) ((fun (x : Fin n) ↦ x.addNat m) b) → a = b

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n_1 m_1 n m : ℕ
a b : Fin m
⊢ natAdd n a = natAdd n b → a = b

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n : ℕ
p : Fin (n + 1)
⊢ (⇑p.succAboveEmb : (a : Fin n) → Fin (n + 1)) = p.succAbove

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
p : Fin (n + 1)
hmn : n ≤ m
⊢ n + (m - n) = m

Tactic:
lia
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
simp :
  Eq (α := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m))
    {i : Fin m | m ≤ (↑i : ℕ) + n}
⊢ Eq (α := Set (Fin m)) (Set.range (ι := Fin n) (⇑(natAdd_castLEEmb hmn) : (a : Fin n) → Fin m))
    {i : Fin m | m - n ≤ (↑i : ℕ)}

Tactic:
simp only [natAdd_castLEEmb, Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add, Fin.natAdd_castLEEmb
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
h :
  ∀ (y : Fin m),
    Membership.mem (γ := Set (Fin m))
        (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m))
        y ↔
      Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y
⊢ Eq (α := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m))
    {i : Fin m | m ≤ (↑i : ℕ) + n}

Tactic:
ext y
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
y : Fin m
h :
  Membership.mem (γ := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m)) y
x : Fin n
hx : (Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding : (a : Fin n) → Fin m) x = y
simp : m ≤ (↑x : ℕ) + (m - n) + n
⊢ Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y

Tactic:
simp [← hx]
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
y : Fin m
h :
  Membership.mem (γ := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m)) y
x : Fin n
hx : (Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding : (a : Fin n) → Fin m) x = y
⊢ m ≤ (↑x : ℕ) + (m - n) + n

Tactic:
lia
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
y : Fin m
xin : Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y
⊢ (Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding : (a : Fin n) → Fin m)
      (subNat (m - n) (Fin.cast ⋯ y) ⋯) =
    y

Tactic:
simp
-- Module: Mathlib.Data.Fin.Embedding
Goal:
n m : ℕ
hmn : n ≤ m
y : Fin m
⊢ Membership.mem (γ := Set (Fin m))
      (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m))
      y ↔
    Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y

Tactic:
exact ⟨fun ⟨x, hx⟩ ↦ by simp [← hx]; lia,
    fun xin ↦ ⟨subNat (m - n) (y.cast (Nat.add_sub_of_le hmn).symm)
    (Nat.sub_le_of_le_add xin), by simp⟩⟩
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
⊢ IsLT 0 n.succ

Tactic:
⟨succ_pos _⟩

Premises used: Fin2.IsLT.mk, Nat.succ_pos
-- Module: Mathlib.Data.Fin.Fin2
Goal:
m n : ℕ
l : IsLT m n
⊢ IsLT m.succ n.succ

Tactic:
⟨succ_lt_succ l.h⟩

Premises used: Nat.succ_lt_succ, Fin2.IsLT.mk, Fin2.IsLT.h
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
zero : Eq (α := Fin2 (HAdd.hAdd (α := ℕ) 0 1)) (rev last) fz
succ : ∀ (n : ℕ), Eq (α := Fin2 (n + 1)) (rev last) fz → Eq (α := Fin2 (n + 1 + 1)) (rev last) fz
⊢ Eq (α := Fin2 (n + 1)) (rev last) fz

Tactic:
induction n
-- Module: Mathlib.Data.Fin.Fin2
Goal:
⊢ Eq (α := Fin2 (HAdd.hAdd (α := ℕ) 0 1)) (rev last) fz

Tactic:
simp_all [rev, castSucc, last]

Premises used: Fin2.castSucc, Fin2.rev, Fin2.last
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
h : Eq (α := Fin2 (n + 1)) (rev last) fz
⊢ Eq (α := Fin2 (n + 1 + 1)) (rev last) fz

Tactic:
simp_all [rev, castSucc, last]

Premises used: Fin2.castSucc, Fin2.rev, Fin2.last
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1 + 1)) (rev (castSucc Fin2.fz)) (Fin2.fs (rev Fin2.fz))
fs : ∀ {n : ℕ} (a : Fin2 n), a.castSucc.rev = a.rev.fs → a.fs.castSucc.rev = a.fs.rev.fs
⊢ i.castSucc.rev = i.rev.fs

Tactic:
induction i
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
⊢ Eq (α := Fin2 (n_1 + 1 + 1)) (rev (castSucc fz)) (fs (rev fz))

Tactic:
simp_all [rev, castSucc, last]

Premises used: Fin2.castSucc, Fin2.rev, Fin2.last