awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
m₁ m₂ : CancelMonoid M
h : Eq.{u + 1} (α := RightCancelMonoid M) toRightCancelMonoid toRightCancelMonoid
⊢ Eq (α := M → M → M) HMul.hMul HMul.hMul

Tactic:
exact congrArg (fun m : Monoid M => (letI := m; HMul.hMul : M → M → M)) <|
    congrArg (@RightCancelMonoid.toMonoid M) h

Premises used: HMul.hMul, congrArg, RightCancelMonoid.toMonoid
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
mul_comm : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul : IsLeftCancelMul M
toSemigroup_1 : Semigroup M
toOne_1 : One M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_1 : ℕ → M → M
npow_zero_1 : ∀ (x : M), npow_1 0 x = 1
npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x * x
mul_comm_1 : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := CommMonoid M) toCommMonoid toCommMonoid
refl :
  ∀ (one_mul_2 : ∀ (a : M), 1 * a = a) (mul_one_2 : ∀ (a : M), a * 1 = a)
    (npow_succ_2 : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x) (npow_zero_2 : ∀ (x : M), npow 0 x = 1)
    (mul_comm_2 : ∀ (a b : M), a * b = b * a) [toIsLeftCancelMul_2 : IsLeftCancelMul M],
    Eq.{u + 1} (α := CancelCommMonoid M)
      { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
        npow_zero := npow_zero, npow_succ := npow_succ, mul_comm := mul_comm, toIsLeftCancelMul := toIsLeftCancelMul }
      { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul_2, mul_one := mul_one_2, npow := npow,
        npow_zero := npow_zero_2, npow_succ := npow_succ_2, mul_comm := mul_comm_2,
        toIsLeftCancelMul := toIsLeftCancelMul_2 }
⊢ Eq.{u + 1} (α := CancelCommMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, mul_comm := mul_comm, toIsLeftCancelMul := toIsLeftCancelMul }
    { toSemigroup := toSemigroup_1, toOne := toOne_1, one_mul := one_mul_1, mul_one := mul_one_1, npow := npow_1,
      npow_zero := npow_zero_1, npow_succ := npow_succ_1, mul_comm := mul_comm_1,
      toIsLeftCancelMul := toIsLeftCancelMul_1 }

Tactic:
cases h
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u
toSemigroup : Semigroup M
toOne : One M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero : ∀ (x : M), npow 0 x = 1
npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
mul_comm : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul : IsLeftCancelMul M
one_mul_1 : ∀ (a : M), 1 * a = a
mul_one_1 : ∀ (a : M), a * 1 = a
npow_succ_1 : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x
npow_zero_1 : ∀ (x : M), npow 0 x = 1
mul_comm_1 : ∀ (a b : M), a * b = b * a
toIsLeftCancelMul_1 : IsLeftCancelMul M
⊢ Eq.{u + 1} (α := CancelCommMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, mul_comm := mul_comm, toIsLeftCancelMul := toIsLeftCancelMul }
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul_1, mul_one := mul_one_1, npow := npow,
      npow_zero := npow_zero_1, npow_succ := npow_succ_1, mul_comm := mul_comm_1,
      toIsLeftCancelMul := toIsLeftCancelMul_1 }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : CancelCommMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
⊢ m₁ = m₂

Tactic:
CancelCommMonoid.toCommMonoid_injective <| CommMonoid.ext h_mul

Premises used: CancelCommMonoid.toCommMonoid_injective, CommMonoid.ext
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
⊢ Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid

Tactic:
have h_mon := Monoid.ext h_mul
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
⊢ Eq.{u_1 + 1} (α := M) One.one One.one

Tactic:
have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
h : ∀ (m : ℤ) (x : M), DivInvMonoid.zpow m x = DivInvMonoid.zpow m x
⊢ Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow

Tactic:
ext m x
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
m : ℤ
x : M
⊢ DivInvMonoid.zpow m x = DivInvMonoid.zpow m x

Tactic:
@MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m

Premises used: MonoidHom.map_zpow', congr_fun
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
m : ℤ
x : M
⊢ DivInvMonoid.zpow m x = DivInvMonoid.zpow m x

Tactic:
exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m

Premises used: MonoidHom.map_zpow', congr_fun
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow

Tactic:
have : m₁.zpow = m₂.zpow := by
    ext m x
    exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
h : ∀ (a b : M), Div.div a b = Div.div a b
⊢ Eq.{u_1 + 1} (α := M → M → M) Div.div Div.div

Tactic:
ext a b
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
a b : M
⊢ Div.div a b = Div.div a b

Tactic:
(@div_eq_mul_inv _ m₁ a b).trans
      (((congr_fun (congr_fun h_mul a) _).trans
        (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)

Premises used: div_eq_mul_inv, congr_arg, congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
a b : M
⊢ Div.div a b = Div.div a b

Tactic:
exact (@div_eq_mul_inv _ m₁ a b).trans
      (((congr_fun (congr_fun h_mul a) _).trans
        (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)

Premises used: div_eq_mul_inv, congr_arg, congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
⊢ Eq.{u_1 + 1} (α := M → M → M) Div.div Div.div

Tactic:
have : m₁.div = m₂.div := by
    ext a b
    exact (@div_eq_mul_inv _ m₁ a b).trans
      (((congr_fun (congr_fun h_mul a) _).trans
        (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this_1 : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
this : Eq.{u_1 + 1} (α := M → M → M) Div.div Div.div
rcases :
  ∀ [toMonoid : Monoid M] (zpow : ℤ → M → M) (zpow_zero' : ∀ (a : M), zpow 0 a = 1)
    (zpow_succ' : ∀ (n : ℕ) (a : M), zpow (↑n.succ : ℤ) a = zpow (↑n : ℤ) a * a) (inv : M → M)
    (zpow_neg' : ∀ (n : ℕ) (a : M), zpow (Int.negSucc n) a = (zpow (↑n.succ : ℤ) a)⁻¹) (div : M → M → M)
    (div_eq_mul_inv : ∀ (a b : M), a / b = a * b⁻¹) (h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul)
    (h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv)
    (h_mon : Eq.{u_1 + 1} (α := Monoid M) DivInvMonoid.toMonoid DivInvMonoid.toMonoid)
    (h₁ : Eq.{u_1 + 1} (α := M) One.one One.one)
    (this : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow)
    (this : Eq.{u_1 + 1} (α := M → M → M) Div.div Div.div),
    { toMonoid := toMonoid, inv := inv, div := div, div_eq_mul_inv := div_eq_mul_inv, zpow := zpow,
        zpow_zero' := zpow_zero', zpow_succ' := zpow_succ', zpow_neg' := zpow_neg' : DivInvMonoid M } =
      m₂
⊢ m₁ = m₂

Tactic:
rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
-- Module: Mathlib.Algebra.Group.Ext
Goal:
M : Type u_1
m₂ : DivInvMonoid M
toMonoid : Monoid M
zpow : ℤ → M → M
zpow_zero' : ∀ (a : M), zpow 0 a = 1
zpow_succ' : ∀ (n : ℕ) (a : M), zpow (↑n.succ : ℤ) a = zpow (↑n : ℤ) a * a
inv : M → M
zpow_neg' : ∀ (n : ℕ) (a : M), zpow (Int.negSucc n) a = (zpow (↑n.succ : ℤ) a)⁻¹
div : M → M → M
div_eq_mul_inv : ∀ (a b : M), a / b = a * b⁻¹
h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
h_inv : Eq.{u_1 + 1} (α := M → M) Inv.inv Inv.inv
h_mon : Eq.{u_1 + 1} (α := Monoid M) DivInvMonoid.toMonoid DivInvMonoid.toMonoid
h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this_1 : Eq.{u_1 + 1} (α := ℤ → M → M) DivInvMonoid.zpow DivInvMonoid.zpow
this : Eq.{u_1 + 1} (α := M → M → M) Div.div Div.div
⊢ { toMonoid := toMonoid, inv := inv, div := div, div_eq_mul_inv := div_eq_mul_inv, zpow := zpow,
      zpow_zero' := zpow_zero', zpow_succ' := zpow_succ', zpow_neg' := zpow_neg' : DivInvMonoid M } =
    m₂

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
toDivInvMonoid : DivInvMonoid G
inv_mul_cancel inv_mul_cancel_1 : ∀ (a : G), a⁻¹ * a = 1
⊢ { toDivInvMonoid := toDivInvMonoid, inv_mul_cancel := inv_mul_cancel : Group G } =
    { toDivInvMonoid := toDivInvMonoid, inv_mul_cancel := inv_mul_cancel_1 }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
g₁ g₂ : Group G
h_mul : Eq (α := G → G → G) HMul.hMul HMul.hMul
⊢ Eq.{u_1 + 1} (α := G) One.one One.one

Tactic:
have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
g₁ g₂ : Group G
h_mul : Eq (α := G → G → G) HMul.hMul HMul.hMul
h₁ : Eq.{u_1 + 1} (α := G) One.one One.one
f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ g₁ = g₂

Tactic:
Group.toDivInvMonoid_injective
      (DivInvMonoid.ext h_mul
        (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))

Premises used: funext, MonoidHom.map_inv, DivInvMonoid.ext, Group.toDivInvMonoid_injective
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
g₁ g₂ : Group G
h_mul : Eq (α := G → G → G) HMul.hMul HMul.hMul
h₁ : Eq.{u_1 + 1} (α := G) One.one One.one
f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ g₁ = g₂

Tactic:
exact
    Group.toDivInvMonoid_injective
      (DivInvMonoid.ext h_mul
        (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))

Premises used: funext, MonoidHom.map_inv, DivInvMonoid.ext, Group.toDivInvMonoid_injective
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
toGroup : Group G
mul_comm mul_comm_1 : ∀ (a b : G), a * b = b * a
⊢ { toGroup := toGroup, mul_comm := mul_comm : CommGroup G } = { toGroup := toGroup, mul_comm := mul_comm_1 }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Ext
Goal:
G : Type u_1
g₁ g₂ : CommGroup G
h_mul : Eq (α := G → G → G) HMul.hMul HMul.hMul
⊢ g₁ = g₂

Tactic:
CommGroup.toGroup_injective <| Group.ext h_mul

Premises used: CommGroup.toGroup_injective, Group.ext
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)

Tactic:
simp [add_def, Nat.add_assoc]

Premises used: Fin.add_def, Nat.add_assoc
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
⊢ ∀ (a b : Fin n), a + b = b + a

Tactic:
simp [add_def, Nat.add_comm]

Premises used: Fin.add_def, Nat.add_comm
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
inst : NeZero n
x x_1 : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
⊢ (↑((⟨a, ha⟩ : Fin n) - (⟨b, hb⟩ : Fin n)) : ℕ) = (↑((⟨a, ha⟩ : Fin n) + -(⟨b, hb⟩ : Fin n)) : ℕ)

Tactic:
simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]

Premises used: Fin.add_def, Fin.neg_def, Fin.sub_def, Nat.add_comm
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
inst : NeZero n
x : Fin n
a : ℕ
ha : a < n
rw : (↑(⟨a, ha⟩ : Fin n) : ℕ) ≤ n
⊢ (n - (↑(⟨a, ha⟩ : Fin n) : ℕ) + a) % n = (↑0 : ℕ)

Tactic:
rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]

Premises used: Nat.mod_self, Nat.sub_add_cancel, Fin.val_zero
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
inst : NeZero n
x : Fin n
a : ℕ
ha : a < n
⊢ (↑(⟨a, ha⟩ : Fin n) : ℕ) ≤ n

Tactic:
le_of_lt ha

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n_1 n : ℕ
inst : NeZero n
x : Fin n
a : ℕ
ha : a < n
⊢ (↑(⟨a, ha⟩ : Fin n) : ℕ) ≤ n

Tactic:
exact le_of_lt ha

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
x : ℤ
⊢ Eq (α := Fin n) (↑x : Fin n) (if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n))

Tactic:
Fin.intCast_def _

Premises used: Fin.intCast_def
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin n
fin_omega fin_omega₁ :
  ((↑(↑a : ℕ) : ℤ) <
      if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
      else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) ↔
    LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
⊢ a < a - b ↔ a < b

Tactic:
fin_omega
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin n
rw : ¬a - b ≤ a ↔ ¬b ≤ a
rw₁ : a < a - b ↔ ¬b ≤ a
rw₂ : a < a - b ↔ a < b
rw₃ rw₄ : a < b ↔ a < b
⊢ a - b ≤ a ↔ b ≤ a

Tactic:
rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]

Premises used: not_iff_not, Fin.not_le, Fin.lt_sub_iff
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
x : Fin (n + 2)
⊢ x < 1 ↔ x = 0

Tactic:
simp [lt_def]

Premises used: Fin.lt_def
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
k : Fin (n + 1)
zero : ∀ {k : Fin (HAdd.hAdd (α := ℕ) 0 1)}, k ≤ k - 1 ↔ k = 0
succ : ∀ (n : ℕ) {k : Fin (n + 1 + 1)}, k ≤ k - 1 ↔ k = 0
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
k : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
simp [fin_one_eq_zero k]

Premises used: Fin.fin_one_eq_zero
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
k : Fin (n + 1 + 1)
succ : k = k + 1 → k = 0
⊢ (↑k : ℕ) ≤ (↑(k - 1) : ℕ) ↔ k = 0

Tactic:
rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
    eq_comm, sub_eq_iff_eq_add]

Premises used: Fin.val_fin_lt, or_iff_left_iff_imp, Fin.lt_sub_one_iff, eq_comm, le_iff_lt_or_eq, sub_eq_iff_eq_add, Fin.val_inj
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
k : Fin (n + 1 + 1)
⊢ k = k + 1 → k = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
k : Fin (n + 1)
⊢ ¬k - 1 < k ↔ ¬0 < k

Tactic:
simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

Premises used: Fin.le_sub_one_iff, Fin.lt_def, not_lt, Fin.le_zero_iff, Fin.val_fin_le
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
⊢ -last n = 1

Tactic:
simp [neg_eq_iff_add_eq_zero]

Premises used: neg_eq_iff_add_eq_zero
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) (-(↑n : Fin (n + 1))) 1

Tactic:
simp only [natCast_eq_last, neg_last]

Premises used: Fin.neg_last, Fin.natCast_eq_last
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin n
zero : ∀ (a b : Fin 0), (a + b).rev = a.rev - b
succ : ∀ (n : ℕ) (a b : Fin (n + 1)), (a + b).rev = a.rev - b
⊢ (a + b).rev = a.rev - b

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
a b : Fin 0
⊢ (a + b).rev = a.rev - b

Tactic:
a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
a b : Fin 0
⊢ (a + b).rev = a.rev - b

Tactic:
exact a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
succ : last n - (a + b) = a.rev - b
succ₁ : last n - (a + b) = last n - a - b
succ₂ succ₃ : last n - a - b = last n - a - b
⊢ (a + b).rev = a.rev - b

Tactic:
rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]

Premises used: Fin.last_sub, sub_add_eq_sub_sub
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin n
rw : a - b = (a.rev + b).rev
rw₁ : a - b = a.rev.rev - b
rw₂ rw₃ : a - b = a - b
⊢ (a - b).rev = a.rev + b

Tactic:
rw [rev_eq_iff, rev_add, rev_rev]

Premises used: Fin.rev_add, Fin.rev_rev, Fin.rev_eq_iff
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : Fin n
ha : (↑a : ℕ) + 1 < n
rw : (↑a : ℕ) < (↑a : ℕ) + 1
⊢ a < a + 1

Tactic:
rw [lt_def, val_add, coe_ofNat_eq_mod, Nat.add_mod_mod, Nat.mod_eq_of_lt ha]

Premises used: Fin.val_add, Nat.add_mod_mod, Nat.mod_eq_of_lt, Fin.lt_def, Fin.coe_ofNat_eq_mod
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : Fin n
ha : (↑a : ℕ) + 1 < n
⊢ (↑a : ℕ) < (↑a : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Fin.Basic
Goal:
n : ℕ
a b : Fin n
rw : a.rev < (a + b).rev ↔ b.rev < a
rw₁ : b.rev < a ↔ a.rev < (a + b).rev
rw₂ : a.rev < b.rev.rev ↔ a.rev < (a + b).rev
rw₃ : a.rev < b.rev.rev ↔ a.rev < a.rev - b
rw₄ : a.rev < b.rev.rev ↔ a.rev < b
rw₅ rw₆ : a.rev < b ↔ a.rev < b
⊢ a + b < a ↔ b.rev < a

Tactic:
rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]

Premises used: Fin.rev_add, Fin.lt_sub_iff, Iff.comm, Fin.rev_rev, Fin.rev_lt_rev
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
unfold :
  x = Pi.mulSingle (M := α) i x i ∧
    Eq.{u_1 + 1} (α := (i_1 : Fin n) → α (i.succAbove i_1)) 1 fun (i_1 : Fin n) ↦
      Pi.mulSingle (M := α) i x (i.succAbove i_1)
⊢ x = Pi.mulSingle (M := α) i x i ∧ 1 = i.removeNth (α := α) (Pi.mulSingle (M := α) i x)

Tactic:
unfold removeNth

Premises used: Fin.removeNth
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle (M := α) i x i ∧
    Eq.{u_1 + 1} (α := (i_1 : Fin n) → α (i.succAbove i_1)) 1 fun (i_1 : Fin n) ↦
      Pi.mulSingle (M := α) i x (i.succAbove i_1)

Tactic:
simp [succAbove_ne, Pi.one_def]

Premises used: Fin.succAbove_ne, Pi.one_def
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (j : Fin (n + 1)) → Mul (α j)
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth (α := α) (x * y) (p * q) = i.insertNth (α := α) x p * i.insertNth (α := α) y q

Tactic:
insertNth_binop (fun _ ↦ (· * ·)) i x y p q

Premises used: HMul.hMul, Fin.insertNth_binop
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (j : Fin (n + 1)) → Div (α j)
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth (α := α) (x / y) (p / q) = i.insertNth (α := α) x p / i.insertNth (α := α) y q

Tactic:
insertNth_binop (fun _ ↦ (· / ·)) i x y p q

Premises used: Fin.insertNth_binop, HDiv.hDiv
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
simp_rw : i.insertNth (α := α) (x / y) (p / p) = Pi.mulSingle (M := α) i (x / y)
simp_rw₁ : i.insertNth (α := α) (x / y) (p / p) = i.insertNth (α := α) (x / y) 1
simp_rw₂ : (i.insertNth (α := α) (x / y) fun (i_1 : Fin n) ↦ p i_1 / p i_1) = i.insertNth (α := α) (x / y) 1
simp_rw₃ : (i.insertNth (α := α) (x / y) fun (i_1 : Fin n) ↦ 1) = i.insertNth (α := α) (x / y) 1
⊢ i.insertNth (α := α) x p / i.insertNth (α := α) y p = Pi.mulSingle (M := α) i (x / y)

Tactic:
simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]

Premises used: Pi.div_def, Fin.insertNth_one_right, div_self', Fin.insertNth_div, Pi.one_def
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
inst : SMul M α
x : M
v : Fin 0 → α
⊢ x • v = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
h : ∀ (i : Fin n.succ), (x • vecCons y v) i = vecCons (x • y) (x • v) i
⊢ x • vecCons y v = vecCons (x • y) (x • v)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
h : (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0
h₁ : ∀ (i : Fin n), (x • vecCons y v) i.succ = vecCons (x • y) (x • v) i.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (x • vecCons y v) i.succ = vecCons (x • y) (x • v) i.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
inst : Add α
v w : Fin 0 → α
⊢ v + w = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
h : ∀ (i : Fin n.succ), (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases