awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
x : M
h_1 : Membership.mem (γ := Submonoid M) (closure s) x
h :
  Membership.mem (γ := Submonoid M)
    (mrange (F := FreeMonoid { x : M // x ∈ s } →* M)
      ((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
          (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
        FreeMonoid { x : M // x ∈ s } →* M))
    x
⊢ motive x h_1
have obtain : ∀ (l : FreeMonoid { x : M // x ∈ s })
  (h :
    Membership.mem (α := M) (γ := Submonoid M) (closure s)
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
              FreeMonoid { x : M // x ∈ s } →* M) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          l :
        M)),
  motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      l)
    h
Tactic: obtain ⟨l, rfl⟩ := h
Cleared hypotheses: x, h_1, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
x : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure s)
        ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                  (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
                FreeMonoid { x : M // x ∈ s } →* M) :
              (a : FreeMonoid { x : M // x ∈ s }) → M)
            y :
          M)),
    motive
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure s)
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        (FreeMonoid.of x * y) :
      M)
⊢ motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      (FreeMonoid.of x * y))
    h
have mul_of : motive
  (HMul.hMul (β := M) (↑x : M)
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        y :
      M))
  sorry
Tactic: simp only [map_mul, FreeMonoid.lift_eval_of]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
x : { x : M // x ∈ s }
y : FreeMonoid { x : M // x ∈ s }
ih :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure s)
        ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                  (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
                FreeMonoid { x : M // x ∈ s } →* M) :
              (a : FreeMonoid { x : M // x ∈ s }) → M)
            y :
          M)),
    motive
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        y)
      h
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure s)
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        (FreeMonoid.of x * y) :
      M)
⊢ motive
    (HMul.hMul (β := M) (↑x : M)
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
              FreeMonoid { x : M // x ∈ s } →* M) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          y :
        M))
    ⋯
have mul_of : Membership.mem (α := M) (γ := Submonoid M) (closure s)
  ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      y :
    M)
Tactic: refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
l : FreeMonoid { x : M // x ∈ s }
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure s)
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        l :
      M)
⊢ motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      l)
    h
have one₁ : ∀
  (h :
    Membership.mem (α := M) (γ := Submonoid M) (closure s)
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
              FreeMonoid { x : M // x ∈ s } →* M) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          1 :
        M)),
  motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      1)
    h
Tactic: induction l using FreeMonoid.inductionOn' with
  | one => exact one
  | mul_of x y ih =>
    simp only [map_mul, FreeMonoid.lift_eval_of]
    refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
    simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ motive x
have have : ∀ (this : Membership.mem (γ := Submonoid M) (closure s) x), motive x
Tactic: have : x ∈ closure s := by simp [hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
this : Membership.mem (γ := Submonoid M) (closure s) x
one₁ : motive 1
⊢ motive x
have mul_left₁ : ∀ (x : M) (hx : x ∈ s) (y : M), Membership.mem (γ := Submonoid M) (closure s) y → ∀ (ih : motive y), motive (x * y)
Tactic: induction this using closure_induction_left with
  | one => exact one
  | mul_left x hx y _ ih => exact mul_left x hx y ih
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_right :
  ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : Membership.mem (γ := Submonoid M) (closure s) x
m : Mᵐᵒᵖ
hm : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) m
⊢ Membership.mem (γ := Submonoid M) (closure s) (MulOpposite.unop m)
have rwa : ∀ (hm : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (Submonoid.op (closure s)) m),
  Membership.mem (γ := Submonoid M) (closure s) (MulOpposite.unop m)
Tactic: rwa [← op_closure] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_right :
  ∀ (x : M) (hx : Membership.mem (γ := Submonoid M) (closure s) x) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : Membership.mem (γ := Submonoid M) (closure s) x
⊢ Membership.mem (γ := Submonoid Mᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) { unop' := x : PreOpposite M }
have rwa : Membership.mem (γ := Submonoid Mᵐᵒᵖ) (Submonoid.op (closure s)) { unop' := x : PreOpposite M }
Tactic: rwa [← op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive x
have have : ∀ (this : Membership.mem (γ := Submonoid M) (closure s) x), motive x
Tactic: have : x ∈ closure s := by simp [hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : M → Prop
hs : Eq (α := Submonoid M) (closure s) ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
this : Membership.mem (γ := Submonoid M) (closure s) x
one₁ : motive 1
⊢ motive x
have mul_right₁ : ∀ (x : M), Membership.mem (γ := Submonoid M) (closure s) x → ∀ (y : M) (hy : y ∈ s) (ih : motive x), motive (x * y)
Tactic: induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a n_1 n : M
i : ℕ
⊢ (fun (x : ℕ) ↦ n_1 ^ x) i = n ↔
    (((powersHom M : (a : M) → Multiplicative ℕ →* M) n_1 : Multiplicative ℕ →* M) : (a : Multiplicative ℕ) → M) i = n
have simp : n_1 ^ i = n ↔ HPow.hPow (β := ℕ) n_1 ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) i : ℕ) = n
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
n : M
⊢ Eq (α := Submonoid M) (powers n) (closure {n})
have h : ∀ (x : M), Membership.mem (γ := Submonoid M) (powers n) x ↔ Membership.mem (γ := Submonoid M) (closure {n}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} (HMul.hMul (α := M) 1 1)
have inl : Membership.mem (γ := Set M) {1, a} 1
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
⊢ Membership.mem (γ := Set M) {1, b} (1 * b)
have inl : Membership.mem (γ := Set M) {1, b} b
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} (a * 1)
have inr : Membership.mem (γ := Set M) {1, a} a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
⊢ Membership.mem (γ := Set M) {1, b} (b * b)
have inr : Membership.mem (γ := Set M) {1, b} b
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x_1 : M
n : ℕ
hpos : 0 < n
hx : x_1 ^ n = 1
m : ℕ
x : ↥(powers x_1)
⊢ (↑(x ^ Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) : M) = (↑(x ^ Int.natMod (↑m : ℤ) (↑n : ℤ) * x) : M)
have obtain : ∀ (k : ℕ),
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) sorry ^
          Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) sorry ^
            Int.natMod (↑m : ℤ) (↑n : ℤ) *
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k)
            sorry) :
      M)
Tactic: obtain ⟨_, k, rfl⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
            ⋯ ^
          Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) :
      M) =
    (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
              ⋯ ^
            Int.natMod (↑m : ℤ) (↑n : ℤ) *
          Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
      M)
have simp : x ^ (k * (HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat) =
  x ^ (k * (HMod.hMod (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat) * x ^ k
Tactic: simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat) =
    x ^ (k * (HMod.hMod (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat) * x ^ k
have norm_cast : x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
have rw : (x ^ m.succ) ^ k = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
Tactic: rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ m.succ) ^ k = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
have rw : (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
Tactic: rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
have iterate : (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
Tactic: iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₂ : (x ^ m.succ) ^ k = (x ^ k) ^ m * x ^ k
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
rw₂ : (x ^ m.succ) ^ k = (x ^ k) ^ m * x ^ k
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₃ : (x ^ m.succ) ^ k = (x ^ k) ^ (m + 1)
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
rw₂ : (x ^ m.succ) ^ k = (x ^ k) ^ m * x ^ k
rw₃ : (x ^ m.succ) ^ k = (x ^ k) ^ (m + 1)
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₄ : x ^ (m.succ * k) = (x ^ k) ^ (m + 1)
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
rw₂ : (x ^ m.succ) ^ k = (x ^ k) ^ m * x ^ k
rw₃ : (x ^ m.succ) ^ k = (x ^ k) ^ (m + 1)
rw₄ : x ^ (m.succ * k) = (x ^ k) ^ (m + 1)
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₅ : x ^ (k * m.succ) = (x ^ k) ^ (m + 1)
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
rw : (x ^ m.succ) ^ k = x ^ (m * k) * x ^ k
rw₁ : (x ^ m.succ) ^ k = x ^ (k * m) * x ^ k
rw₂ : (x ^ m.succ) ^ k = (x ^ k) ^ m * x ^ k
rw₃ : (x ^ m.succ) ^ k = (x ^ k) ^ (m + 1)
rw₄ : x ^ (m.succ * k) = (x ^ k) ^ (m + 1)
rw₅ : x ^ (k * m.succ) = (x ^ k) ^ (m + 1)
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
have rw₆ : (x ^ k) ^ m.succ = (x ^ k) ^ (m + 1)
Tactic: rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x_1 : M
n : ℕ
hpos : 0 < n
hx : x_1 ^ n = 1
m : ℕ
x : ↥(powers x_1)
⊢ (↑(x ^ (Int.negSucc m).natMod (↑n : ℤ)) : M) = (↑((x ^ Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) ^ (n - 1)) : M)
have obtain : ∀ (k : ℕ),
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) sorry ^
          (Int.negSucc m).natMod (↑n : ℤ)) :
      M) =
    (↑((Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) sorry ^
            Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) ^
          (n - 1)) :
      M)
Tactic: obtain ⟨_, k, rfl⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
            ⋯ ^
          (Int.negSucc m).natMod (↑n : ℤ)) :
      M) =
    (↑((Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
              ⋯ ^
            Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) ^
          (n - 1)) :
      M)
have simp : x ^ (k * (Int.negSucc m % (↑n : ℤ)).toNat) = x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
Tactic: simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (Int.negSucc m % (↑n : ℤ)).toNat) = x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
have rw : x ^ (k * ((-(↑m.succ : ℤ) + HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑n : ℤ)) % (↑n : ℤ)).toNat) =
  x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
Tactic: rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * ((-(↑m.succ : ℤ) + HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑n : ℤ)) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
have nth_rw : x ^ (k * ((-HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) 1 + HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑n : ℤ)) % (↑n : ℤ)).toNat) =
  x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
Tactic: nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * ((-HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) 1 + HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑n : ℤ)) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
have rw : x ^ (k * (HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑(n - 1) : ℤ) % (↑n : ℤ)).toNat) =
  x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
Tactic: rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑(n - 1) : ℤ) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
have norm_cast : x ^ (k * Int.toNat (↑((m + 1) * (n - 1) % n) : ℤ)) = x ^ (k * (Int.toNat (↑(m.succ % n) : ℤ) * (n - 1)))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * Int.toNat (↑((m + 1) * (n - 1) % n) : ℤ)) = x ^ (k * (Int.toNat (↑(m.succ % n) : ℤ) * (n - 1)))
have simp : x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
Tactic: simp only [Int.toNat_natCast]