awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
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
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ Eq.{u + 1} (α := LeftCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, 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, toIsLeftCancelMul := toIsLeftCancelMul_1 }
have e_toMonoid : toSemigroup = toSemigroup_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
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
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
⊢ Eq.{u + 1} (α := LeftCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, 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, toIsLeftCancelMul := toIsLeftCancelMul_1 }
have e_toMonoid₁ : toOne = toOne_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
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
toIsLeftCancelMul_1 : IsLeftCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
e_toMonoid₁ : toOne = toOne_1
⊢ Eq.{u + 1} (α := LeftCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, 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, toIsLeftCancelMul := toIsLeftCancelMul_1 }
have e_toMonoid₂ : npow = npow_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
toIsRightCancelMul : IsRightCancelMul 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
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
⊢ Eq.{u + 1} (α := RightCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, toIsRightCancelMul := toIsRightCancelMul }
    { 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, toIsRightCancelMul := toIsRightCancelMul_1 }
have e_toMonoid : toSemigroup = toSemigroup_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
toIsRightCancelMul : IsRightCancelMul 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
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
⊢ Eq.{u + 1} (α := RightCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, toIsRightCancelMul := toIsRightCancelMul }
    { 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, toIsRightCancelMul := toIsRightCancelMul_1 }
have e_toMonoid₁ : toOne = toOne_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
toIsRightCancelMul : IsRightCancelMul 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
toIsRightCancelMul_1 : IsRightCancelMul M
h : Eq.{u + 1} (α := Monoid M) toMonoid toMonoid
e_toMonoid : toSemigroup = toSemigroup_1
e_toMonoid₁ : toOne = toOne_1
⊢ Eq.{u + 1} (α := RightCancelMonoid M)
    { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, npow := npow,
      npow_zero := npow_zero, npow_succ := npow_succ, toIsRightCancelMul := toIsRightCancelMul }
    { 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, toIsRightCancelMul := toIsRightCancelMul_1 }
have e_toMonoid₂ : npow = npow_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
Goal:
M : Type u
m₁ m₂ : CancelMonoid M
h : Eq.{u + 1} (α := RightCancelMonoid M) toRightCancelMonoid toRightCancelMonoid
⊢ m₁ = m₂
have h_mul : Eq (α := M → M → M) HMul.hMul HMul.hMul
Tactic: apply CancelMonoid.ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
⊢ 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 }
have 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 }
Tactic: cases h
Cleared hypotheses: toSemigroup_1, toOne_1, one_mul_1, mul_one_1, npow_1, npow_zero_1, npow_succ_1, mul_comm_1, toIsLeftCancelMul_1, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
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
⊢ m₁ = m₂
have h_mon : Eq.{u_1 + 1} (α := Monoid M) toMonoid toMonoid
Tactic: have h_mon := Monoid.ext h_mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
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
⊢ m₁ = m₂
have h₁ : Eq.{u_1 + 1} (α := M) One.one One.one
Tactic: have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
have h : ∀ (m : ℤ) (x : M), DivInvMonoid.zpow m x = DivInvMonoid.zpow m x
Tactic: ext m x
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
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₁ = m₂
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
have h : ∀ (a b : M), Div.div a b = Div.div a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
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
⊢ m₁ = m₂
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (goal)
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
⊢ m₁ = m₂
have 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₂
Tactic: rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
Cleared hypotheses: m₁, h_mul, h_inv, h_mon, h₁, f, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Group.Ext (hypothesis)
Goal:
G : Type u_1
g₁ g₂ : Group G
h_mul : Eq (α := G → G → G) HMul.hMul HMul.hMul
⊢ g₁ = g₂
have h₁ : Eq.{u_1 + 1} (α := G) One.one One.one
Tactic: have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n_1 n : ℕ
inst : NeZero n
x : Fin n
a : ℕ
ha : a < n
⊢ (n - (↑(⟨a, ha⟩ : Fin n) : ℕ) + a) % n = (↑0 : ℕ)
have rw : (↑(⟨a, ha⟩ : Fin n) : ℕ) ≤ n
Tactic: rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ a < a - b ↔ a < b
have fin_omega : ((↑(↑a : ℕ) : ℤ) <
    if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) ↔
  LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
Tactic: fin_omega
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ a - b ≤ a ↔ b ≤ a
have rw : ¬a - b ≤ a ↔ ¬b ≤ a
Tactic: rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ¬a - b ≤ a ↔ ¬b ≤ a
⊢ a - b ≤ a ↔ b ≤ a
have rw₁ : a < a - b ↔ ¬b ≤ a
Tactic: rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ¬a - b ≤ a ↔ ¬b ≤ a
rw₁ : a < a - b ↔ ¬b ≤ a
⊢ a - b ≤ a ↔ b ≤ a
have rw₂ : a < a - b ↔ a < b
Tactic: rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ¬a - b ≤ a ↔ ¬b ≤ a
rw₁ : a < a - b ↔ ¬b ≤ a
rw₂ : a < a - b ↔ a < b
⊢ a - b ≤ a ↔ b ≤ a
have rw₃ : a < b ↔ a < b
Tactic: rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0
have zero : ∀ {k : Fin (HAdd.hAdd (α := ℕ) 0 1)}, k ≤ k - 1 ↔ k = 0
Tactic: cases n
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
k : Fin (n + 1)
zero : ∀ {k : Fin (HAdd.hAdd (α := ℕ) 0 1)}, k ≤ k - 1 ↔ k = 0
⊢ k ≤ k - 1 ↔ k = 0
have succ : ∀ (n : ℕ) {k : Fin (n + 1 + 1)}, k ≤ k - 1 ↔ k = 0
Tactic: cases n
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
k : Fin (n + 1 + 1)
⊢ (↑k : ℕ) ≤ (↑(k - 1) : ℕ) ↔ k = 0
have succ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ (a + b).rev = a.rev - b
have zero : ∀ (a b : Fin 0), (a + b).rev = a.rev - b
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
zero : ∀ (a b : Fin 0), (a + b).rev = a.rev - b
⊢ (a + b).rev = a.rev - b
have succ : ∀ (n : ℕ) (a b : Fin (n + 1)), (a + b).rev = a.rev - b
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
⊢ (a + b).rev = a.rev - b
have succ : last n - (a + b) = a.rev - b
Tactic: rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
succ : last n - (a + b) = a.rev - b
⊢ (a + b).rev = a.rev - b
have succ₁ : last n - (a + b) = last n - a - b
Tactic: rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
succ : last n - (a + b) = a.rev - b
succ₁ : last n - (a + b) = last n - a - b
⊢ (a + b).rev = a.rev - b
have succ₂ : last n - a - b = last n - a - b
Tactic: rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ (a - b).rev = a.rev + b
have rw : a - b = (a.rev + b).rev
Tactic: rw [rev_eq_iff, rev_add, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : a - b = (a.rev + b).rev
⊢ (a - b).rev = a.rev + b
have rw₁ : a - b = a.rev.rev - b
Tactic: rw [rev_eq_iff, rev_add, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : a - b = (a.rev + b).rev
rw₁ : a - b = a.rev.rev - b
⊢ (a - b).rev = a.rev + b
have rw₂ : a - b = a - b
Tactic: rw [rev_eq_iff, rev_add, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
ha : (↑a : ℕ) + 1 < n
⊢ a < a + 1
have rw : (↑a : ℕ) < (↑a : ℕ) + 1
Tactic: rw [lt_def, val_add, coe_ofNat_eq_mod, Nat.add_mod_mod, Nat.mod_eq_of_lt ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ a + b < a ↔ b.rev < a
have rw : a.rev < (a + b).rev ↔ b.rev < a
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : a.rev < (a + b).rev ↔ b.rev < a
⊢ a + b < a ↔ b.rev < a
have rw₁ : b.rev < a ↔ a.rev < (a + b).rev
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : a.rev < (a + b).rev ↔ b.rev < a
rw₁ : b.rev < a ↔ a.rev < (a + b).rev
⊢ a + b < a ↔ b.rev < a
have rw₂ : a.rev < b.rev.rev ↔ a.rev < (a + b).rev
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
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
⊢ a + b < a ↔ b.rev < a
have rw₃ : a.rev < b.rev.rev ↔ a.rev < a.rev - b
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
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
⊢ a + b < a ↔ b.rev < a
have rw₄ : a.rev < b.rev.rev ↔ a.rev < b
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Basic (goal)
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
⊢ a + b < a ↔ b.rev < a
have rw₅ : a.rev < b ↔ a.rev < b
Tactic: rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
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 ∧ 1 = i.removeNth (α := α) (Pi.mulSingle (M := α) i x)
have 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)
Tactic: unfold removeNth
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
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)
⊢ i.insertNth (α := α) x p / i.insertNth (α := α) y p = Pi.mulSingle (M := α) i (x / y)
have simp_rw : i.insertNth (α := α) (x / y) (p / p) = Pi.mulSingle (M := α) i (x / y)
Tactic: simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
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)
⊢ i.insertNth (α := α) x p / i.insertNth (α := α) y p = Pi.mulSingle (M := α) i (x / y)
have simp_rw₁ : i.insertNth (α := α) (x / y) (p / p) = i.insertNth (α := α) (x / y) 1
Tactic: simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
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
⊢ i.insertNth (α := α) x p / i.insertNth (α := α) y p = Pi.mulSingle (M := α) i (x / y)
have simp_rw₂ : (i.insertNth (α := α) (x / y) fun (i_1 : Fin n) ↦ p i_1 / p i_1) = i.insertNth (α := α) (x / y) 1
Tactic: simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
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
⊢ i.insertNth (α := α) x p / i.insertNth (α := α) y p = Pi.mulSingle (M := α) i (x / y)
have simp_rw₃ : (i.insertNth (α := α) (x / y) fun (i_1 : Fin n) ↦ 1) = i.insertNth (α := α) (x / y) 1
Tactic: simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
have h : ∀ (i : Fin n.succ), (x • vecCons y v) i = vecCons (x • y) (x • v) i
Tactic: ext i