awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n x : M
⊢ Membership.mem (γ := Submonoid M) (powers n) x ↔ Membership.mem (γ := Submonoid M) (closure {n}) x

Tactic:
mem_closure_singleton.symm

Premises used: Set.Mem, setOf, Submonoid.mem_closure_singleton, Set.range, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n x : M
⊢ Membership.mem (γ := Submonoid M) (powers n) x ↔ Membership.mem (γ := Submonoid M) (closure {n}) x

Tactic:
exact mem_closure_singleton.symm

Premises used: Submonoid.mem_closure_singleton, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n : M
P : Submonoid M
⊢ powers n ≤ P ↔ n ∈ P

Tactic:
simp [powers_eq_closure]

Premises used: Submonoid.powers_eq_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (powers 1) ⊥

Tactic:
bot_unique <| powers_le.2 <| one_mem _

Premises used: Iff.mpr, bot_unique, OneMemClass.one_mem, Submonoid.powers_le
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
inl : Membership.mem (γ := Set M) {1, a} 1
⊢ Membership.mem (γ := Set M) {1, a} (HMul.hMul (α := M) 1 1)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} 1

Tactic:
.inl rfl

Premises used: Set.insert, Set.Mem, setOf, Or.inl, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} 1

Tactic:
exact .inl rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
inl : Membership.mem (γ := Set M) {1, b} b
⊢ Membership.mem (γ := Set M) {1, b} (1 * b)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
⊢ Membership.mem (γ := Set M) {1, b} b

Tactic:
.inr rfl

Premises used: Set.insert, Set.Mem, setOf, Or.inr, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
⊢ Membership.mem (γ := Set M) {1, b} b

Tactic:
exact .inr rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
inr : Membership.mem (γ := Set M) {1, a} a
⊢ Membership.mem (γ := Set M) {1, a} (a * 1)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} a

Tactic:
.inr rfl

Premises used: Set.insert, Set.Mem, setOf, Or.inr, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
⊢ Membership.mem (γ := Set M) {1, a} a

Tactic:
exact .inr rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
b : M
ha : IsIdempotentElem b
inr : Membership.mem (γ := Set M) {1, b} b
⊢ Membership.mem (γ := Set M) {1, b} (b * b)

Tactic:
rw [ha]
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ Membership.mem (γ := Submonoid M) (powers a) 1

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
ha : IsIdempotentElem x
S : Submonoid M := { carrier := {1, x}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ Membership.mem (γ := Submonoid M) (powers x) x

Tactic:
Submonoid.mem_powers _

Premises used: Submonoid.mem_powers
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ Membership.mem (γ := Submonoid M) (powers a) 1

Tactic:
exacts [one_mem _, Submonoid.mem_powers _]

Premises used: Submonoid.mem_powers, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
z : ↥(powers x)
⊢ z ^ Int.natMod 0 (↑n : ℤ) = 1

Tactic:
simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]

Premises used: pow_zero, Int.toNat_zero, Int.zero_emod, Int.natMod
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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)
obtain :
  ∀ (k : ℕ),
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) ⋯ ^
            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)
                ⋯ ^
              Int.natMod (↑m : ℤ) (↑n : ℤ) *
            Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k)
              ⋯) :
        M)
⊢ (↑(x ^ Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) : M) = (↑(x ^ Int.natMod (↑m : ℤ) (↑n : ℤ) * x) : M)

Tactic:
obtain ⟨_, k, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
simp :
  x ^ (k * (HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat) =
    x ^ (k * (HMod.hMod (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat) * x ^ 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)

Tactic:
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]

Premises used: pow_mul, SubmonoidClass.coe_pow, Submonoid.coe_mul, Int.natMod
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
norm_cast : x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
⊢ x ^ (k * (HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat) =
    x ^ (k * (HMod.hMod (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat) * x ^ k

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k
⊢ x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k

Tactic:
rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]

Premises used: Int.toNat_natCast, pow_eq_pow_mod, pow_mul, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k

Tactic:
rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]

Premises used: Int.toNat_natCast, pow_eq_pow_mod, pow_mul, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
iterate : (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
⊢ x ^ (k * Int.toNat (↑(m.succ % n) : ℤ)) = x ^ (k * Int.toNat (↑(m % n) : ℤ)) * x ^ k

Tactic:
iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]

Premises used: Int.toNat_natCast, pow_eq_pow_mod, pow_mul, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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)
rw₆ rw₇ : (x ^ k) ^ m.succ = (x ^ k) ^ (m + 1)
⊢ (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]

Premises used: pow_succ, pow_mul, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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)
obtain :
  ∀ (k : ℕ),
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers x_1) x) ((fun (x : ℕ) ↦ x_1 ^ x) k) ⋯ ^
            (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)
                ⋯ ^
              Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) ^
            (n - 1)) :
        M)
⊢ (↑(x ^ (Int.negSucc m).natMod (↑n : ℤ)) : M) = (↑((x ^ Int.natMod (↑m.succ : ℤ) (↑n : ℤ)) ^ (n - 1)) : M)

Tactic:
obtain ⟨_, k, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
simp :
  x ^ (k * (Int.negSucc m % (↑n : ℤ)).toNat) = x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
⊢ (↑(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)

Tactic:
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]

Premises used: pow_mul, SubmonoidClass.coe_pow, Int.natMod
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 ^ (k * ((-(↑m.succ : ℤ) + HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑n : ℤ)) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
⊢ x ^ (k * (Int.negSucc m % (↑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 : ℕ))]

Premises used: Nat.cast, Int.natCast_succ, HAdd.hAdd, Int.add_mul_emod_self_right, Int.negSucc_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
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)))
⊢ x ^ (k * ((-(↑m.succ : ℤ) + 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 : ℕ) : ℤ)]

Premises used: Nat.cast, HAdd.hAdd, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 ^ (k * (HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑(n - 1) : ℤ) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))
⊢ 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:
rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]

Premises used: sub_eq_neg_add, Int.mul_sub, Int.natCast_pred_of_pos
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
norm_cast : x ^ (k * Int.toNat (↑((m + 1) * (n - 1) % n) : ℤ)) = x ^ (k * (Int.toNat (↑(m.succ % n) : ℤ) * (n - 1)))
⊢ x ^ (k * (HMul.hMul (α := ℤ) (↑(m + 1) : ℤ) (↑(n - 1) : ℤ) % (↑n : ℤ)).toNat) =
    x ^ (k * ((HMod.hMod (α := ℤ) (↑m.succ : ℤ) (↑n : ℤ)).toNat * (n - 1)))

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 : ℕ
simp : x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
⊢ x ^ (k * Int.toNat (↑((m + 1) * (n - 1) % n) : ℤ)) = x ^ (k * (Int.toNat (↑(m.succ % n) : ℤ) * (n - 1)))

Tactic:
simp only [Int.toNat_natCast]

Premises used: Int.toNat_natCast
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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 + 1) * (n - 1) % n * k) = x ^ (k * (m.succ % n * (n - 1)))
rw₁ : (x ^ ((m + 1) * (n - 1) % n)) ^ k = x ^ (k * (m.succ % n * (n - 1)))
rw₂ : (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (k * (m.succ % n * (n - 1)))
rw₃ : (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * (n - 1) * k)
rw₄ : (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * ((n - 1) * k))
rw₅ : (x ^ ((m + 1) * (n - 1))) ^ k = (x ^ (m.succ % n)) ^ ((n - 1) * k)
rw₆ : (x ^ ((m + 1) * (n - 1))) ^ k = (x ^ m.succ) ^ ((n - 1) * k)
rw₇ : ((x ^ (m + 1)) ^ (n - 1)) ^ k = (x ^ m.succ) ^ ((n - 1) * k)
rw₈ rw₉ : ((x ^ (m + 1)) ^ (n - 1)) ^ k = ((x ^ m.succ) ^ (n - 1)) ^ k
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))

Tactic:
rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
      ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]

Premises used: pow_eq_pow_mod, mul_assoc, pow_mul, HMod.hMod, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
y : ↥(powers x)
obtain :
  ∀ (k : ℕ),
    (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
                ⋯ ^
              (n - 1) *
            Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        M) =
      (↑1 : M)
⊢ (↑(y ^ (n - 1) * y) : M) = (↑1 : M)

Tactic:
obtain ⟨_, k, rfl⟩ := y

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
k : ℕ
simp : (x ^ k) ^ (n - 1) * x ^ k = 1
⊢ (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
              ⋯ ^
            (n - 1) *
          Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
      M) =
    (↑1 : M)

Tactic:
simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]

Premises used: Submonoid.coe_one, SubmonoidClass.coe_pow, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
k : ℕ
rw : (x ^ k) ^ (n - 1 + 1) = 1
rw₁ : (x ^ k) ^ n = 1
rw₂ : x ^ (k * n) = 1
rw₃ : x ^ (n * k) = 1
rw₄ : (x ^ n) ^ k = 1
rw₅ : HPow.hPow (α := M) 1 k = 1
rw₆ rw₇ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1

Tactic:
rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]

Premises used: one_pow, pow_succ, pow_mul, Nat.sub_add_cancel, mul_comm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n : M
m : ℕ
⊢ Eq (α := ↥(powers n)) (pow n m)
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (powers n) x) (n ^ m) ⋯)

Tactic:
rfl

Premises used: Set.Mem, Multiplicative, Submonoid.pow, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
inst_1 : DecidableEq M
n : M
p : ↥(powers n)
⊢ pow n (log p) = p

Tactic:
Subtype.ext <| Nat.find_spec p.prop

Premises used: Subtype.prop, Nat.find_spec, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
n : M
⊢ (Function.Injective.{1, u_1 + 1} (β := M) fun (m : ℕ) ↦ n ^ m) ↔ Function.Injective (β := ↥(powers n)) (pow n)

Tactic:
Subtype.coe_injective.of_comp_iff (pow n)

Premises used: Subtype.coe_injective, Submonoid.pow, Function.Injective.of_comp_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
inst_1 : DecidableEq M
n : M
h : Function.Injective.{1, u_1 + 1} (β := M) fun (m : ℕ) ↦ n ^ m
m : ℕ
⊢ log (pow n m) = m

Tactic:
pow_right_injective_iff_pow_injective.mp h <| pow_log_eq_self _

Premises used: Submonoid.pow_log_eq_self, Submonoid.pow_right_injective_iff_pow_injective, Iff.mp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid M
a : M
inst_1 : DecidableEq M
n : M
h : Function.Injective.{1, u_1 + 1} (β := M) fun (m : ℕ) ↦ n ^ m
x x_1 : Multiplicative ℕ
⊢ pow n ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) (x * x_1)) =
    HMul.hMul (α := ↥(powers n)) (pow n ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) x))
      (pow n ((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ) x_1))

Tactic:
simp only [pow, map_mul, ofAdd_add, toAdd_mul]

Premises used: toAdd_mul, ofAdd_add, map_mul, Submonoid.pow
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
inst_1 : DecidableEq M
n : M
h : Function.Injective.{1, u_1 + 1} (β := M) fun (m : ℕ) ↦ n ^ m
x y : ↥(powers n)
⊢ log (x * y) = log x + log y

Tactic:
map_mul (powLogEquiv h).symm x y

Premises used: Submonoid.log, Multiplicative, map_mul, Nat.find, MulEquiv.symm, Submonoid.powLogEquiv
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
x : ℤ
h : 1 < x.natAbs
m : ℕ
⊢ log (pow x m) = m

Tactic:
(powLogEquiv (Int.pow_right_injective h)).symm_apply_apply _

Premises used: Submonoid.log, Multiplicative, Nat.find, MulEquiv.symm_apply_apply, Submonoid.powLogEquiv, Int.pow_right_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
N : Type u_4
F : Type u_5
inst_1 : Monoid N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
m : M
⊢ Eq (α := Submonoid N) (map f (powers m)) (powers ((f : (a : M) → N) m))

Tactic:
simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

Premises used: Set.image_singleton, Submonoid.powers_eq_closure, MonoidHom.map_mclosure
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : MulAction M N
inst_2 : SMul N α
inst_3 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ IsScalarTower M N α

Tactic:
⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩

Premises used: Submonoid.induction_of_closure_eq_top_left, IsScalarTower.mk
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : MulAction M N
inst_2 : SMul N α
inst_3 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
refine_1 :
  ∀ (x : M) (y : N) (z : α),
    HSMul.hSMul.{u_1, u_4, u_4} (α := M) 1 y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)
refine_2 :
  ∀ (x x : M),
    x ∈ s →
      ∀ (y : M),
        (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) →
          ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
⊢ IsScalarTower M N α

Tactic:
refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : MulAction M N
inst_2 : SMul N α
inst_3 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
refine_1 : y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)
refine_1₁ refine_1₂ : y • z = y • z
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := M) 1 y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)

Tactic:
rw [one_smul, one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : MulAction M N
inst_2 : SMul N α
inst_3 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
z : α
refine_2 : (x • x' • y) • z = (x * x') • y • z
refine_2₁ : (x • x' • y) • z = x • x' • y • z
refine_2₂ : x • (x' • y) • z = x • x' • y • z
refine_2₃ refine_2₄ : x • x' • y • z = x • x' • y • z
⊢ ((x * x') • y) • z = (x * x') • y • z

Tactic:
rw [mul_smul, mul_smul, hs x hx, hx']

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : SMul N α
inst_2 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ SMulCommClass M N α

Tactic:
⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩

Premises used: Submonoid.induction_of_closure_eq_top_left, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : SMul N α
inst_2 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
refine_1 :
  ∀ (x : M) (n : N) (a : α),
    HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (n • a) = n • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 a
refine_2 :
  ∀ (x x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
⊢ SMulCommClass M N α

Tactic:
refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : SMul N α
inst_2 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
refine_1 : y • z = y • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 z
refine_1₁ refine_1₂ : y • z = y • z
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z) = y • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 z

Tactic:
rw [one_smul, one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
inst : Monoid M
inst_1 : SMul N α
inst_2 : MulAction M α
s : Set M
htop : Eq (α := Submonoid M) (Submonoid.closure s) ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
refine_2 : x • x' • y • z = y • (x * x') • z
refine_2₁ : x • x' • y • z = y • x • x' • z
refine_2₂ : x • y • x' • z = y • x • x' • z
refine_2₃ refine_2₄ : y • x • x' • z = y • x • x' • z
⊢ (x * x') • y • z = y • (x * x') • z

Tactic:
rw [mul_smul, mul_smul, hx', hs x hx]

Premises used: SemigroupAction.mul_smul