awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw : x ^ ((m + 1) * (n - 1) % n * k) = 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]
-- 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 + 1) * (n - 1) % n * k) = x ^ (k * (m.succ % n * (n - 1)))
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₁ : (x ^ ((m + 1) * (n - 1) % n)) ^ k = 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]
-- 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 + 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)))
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₂ : (x ^ ((m + 1) * (n - 1))) ^ k = 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]
-- 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 + 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)))
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₃ : (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * (n - 1) * k)
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]
-- 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 + 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)
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₄ : (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * ((n - 1) * k))
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]
-- 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 + 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))
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₅ : (x ^ ((m + 1) * (n - 1))) ^ k = (x ^ (m.succ % n)) ^ ((n - 1) * k)
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]
-- 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 + 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)
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₆ : (x ^ ((m + 1) * (n - 1))) ^ k = (x ^ m.succ) ^ ((n - 1) * k)
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]
-- 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 + 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)
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₇ : ((x ^ (m + 1)) ^ (n - 1)) ^ k = (x ^ m.succ) ^ ((n - 1) * k)
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]
-- 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 + 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)
⊢ x ^ (k * ((m + 1) * (n - 1) % n)) = x ^ (k * (m.succ % n * (n - 1)))
have rw₈ : ((x ^ (m + 1)) ^ (n - 1)) ^ k = ((x ^ m.succ) ^ (n - 1)) ^ k
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]
-- 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
y : ↥(powers x)
⊢ (↑(y ^ (n - 1) * y) : M) = (↑1 : M)
have obtain : ∀ (k : ℕ),
  (↑(Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1) ((fun (x_1 : ℕ) ↦ x ^ x_1) k)
              sorry ^
            (n - 1) *
          Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) sorry) :
      M) =
    (↑1 : M)
Tactic: obtain ⟨_, k, rfl⟩ := y
Cleared hypotheses: y
-- 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
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)
have simp : (x ^ k) ^ (n - 1) * x ^ k = 1
Tactic: simp only [coe_one, coe_mul, 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
k : ℕ
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw : (x ^ k) ^ (n - 1 + 1) = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
k : ℕ
rw : (x ^ k) ^ (n - 1 + 1) = 1
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₁ : (x ^ k) ^ n = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
k : ℕ
rw : (x ^ k) ^ (n - 1 + 1) = 1
rw₁ : (x ^ k) ^ n = 1
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₂ : x ^ (k * n) = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
k : ℕ
rw : (x ^ k) ^ (n - 1 + 1) = 1
rw₁ : (x ^ k) ^ n = 1
rw₂ : x ^ (k * n) = 1
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₃ : x ^ (n * k) = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
k : ℕ
rw : (x ^ k) ^ (n - 1 + 1) = 1
rw₁ : (x ^ k) ^ n = 1
rw₂ : x ^ (k * n) = 1
rw₃ : x ^ (n * k) = 1
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₄ : (x ^ n) ^ k = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
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
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₅ : HPow.hPow (α := M) 1 k = 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_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
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
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
have rw₆ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 α
have 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)
Tactic: refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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)
⊢ IsScalarTower M N α
have 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
Tactic: refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 : α
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := M) 1 y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)
have refine_1 : y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)
Tactic: rw [one_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := M) 1 y • z = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z)
have refine_1₁ : y • z = y • z
Tactic: rw [one_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 : α
⊢ ((x * x') • y) • z = (x * x') • y • z
have refine_2 : (x • x' • y) • z = (x * x') • y • z
Tactic: rw [mul_smul, mul_smul, hs x hx, hx']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ ((x * x') • y) • z = (x * x') • y • z
have refine_2₁ : (x • x' • y) • z = x • x' • y • z
Tactic: rw [mul_smul, mul_smul, hs x hx, hx']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ ((x * x') • y) • z = (x * x') • y • z
have refine_2₂ : x • (x' • y) • z = x • x' • y • z
Tactic: rw [mul_smul, mul_smul, hs x hx, hx']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ ((x * x') • y) • z = (x * x') • y • z
have refine_2₃ : x • x' • y • z = x • x' • y • z
Tactic: rw [mul_smul, mul_smul, hs x hx, hx']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 α
have 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
Tactic: refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ SMulCommClass M N α
have 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
Tactic: refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 : α
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z) = y • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 z
have refine_1 : y • z = y • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 z
Tactic: rw [one_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (y • z) = y • HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 z
have refine_1₁ : y • z = y • z
Tactic: rw [one_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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 : α
⊢ (x * x') • y • z = y • (x * x') • z
have refine_2 : x • x' • y • z = y • (x * x') • z
Tactic: rw [mul_smul, mul_smul, hx', hs x hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ (x * x') • y • z = y • (x * x') • z
have refine_2₁ : x • x' • y • z = y • x • x' • z
Tactic: rw [mul_smul, mul_smul, hx', hs x hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ (x * x') • y • z = y • (x * x') • z
have refine_2₂ : x • y • x' • z = y • x • x' • z
Tactic: rw [mul_smul, mul_smul, hx', hs x hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
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
⊢ (x * x') • y • z = y • (x * x') • z
have refine_2₃ : y • x • x' • z = y • x • x' • z
Tactic: rw [mul_smul, mul_smul, hx', hs x hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₁ : s ⊔ t =
  map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₂ : s ⊔ t =
  map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
    map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₃ : s ⊔ t =
  mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
    map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]