awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
S : Type u_7
α : Type u_8
β : Type u_9
inst : SMul α β
inst_1 : SetLike S α
s : S
x : ↥s
t : Set β
⊢ x • t = (↑x : α) • t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
S : Type u_6
inst : Monoid M
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
h : Ne (α := ℕ) 1 0
H : S
⊢ HPow.hPow (β := ℕ) (↑H : Set M) 1 = (↑H : Set M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
S : Type u_6
inst : Monoid M
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
n : ℕ
h : n + 2 ≠ 0
H : S
rw : (↑H : Set M) ^ (n + 1) * (↑H : Set M) = (↑H : Set M)
rw₁ : (↑H : Set M) * (↑H : Set M) = (↑H : Set M)
rw₂ rw₃ : (↑H : Set M) = (↑H : Set M)
⊢ (↑H : Set M) ^ (n + 2) = (↑H : Set M)

Tactic:
rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

Premises used: coe_mul_coe, pow_succ, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s t : Set M
S : Submonoid M
hs : s ⊆ (↑S : Set M)
ht : t ⊆ (↑S : Set M)
⊢ s * t ⊆ (↑S : Set M)

Tactic:
mul_subset_iff.2 fun _x hx _y hy ↦ mul_mem (hs hx) (ht hy)

Premises used: Iff.mpr, Set.mul_subset_iff, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
S : Submonoid M
n : ℕ
hs : s ⊆ (↑S : Set M)
zero : HPow.hPow (β := ℕ) s 0 ⊆ (↑S : Set M)
succ : ∀ (n : ℕ), s ^ n ⊆ (↑S : Set M) → s ^ (n + 1) ⊆ (↑S : Set M)
⊢ s ^ n ⊆ (↑S : Set M)

Tactic:
induction n
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ (↑S : Set M)
⊢ HPow.hPow (β := ℕ) s 0 ⊆ (↑S : Set M)

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ (↑S : Set M)
n : ℕ
h : s ^ n ⊆ (↑S : Set M)
⊢ s ^ (n + 1) ⊆ (↑S : Set M)

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s t u : Set M
hs : s ⊆ u
ht : t ⊆ u
⊢ s * t ⊆ (↑(closure u) : Set M)

Tactic:
mul_subset (Subset.trans hs Submonoid.subset_closure) (Subset.trans ht Submonoid.subset_closure)

Premises used: Set.Subset.trans, Submonoid.mul_subset, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Submonoid M
⊢ (↑s : Set M) * (↑s : Set M) = (↑s : Set M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
S T : Set M
⊢ LE.le (α := Submonoid M) (closure (S * T)) (closure S ⊔ closure T)

Tactic:
sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ => hx ▸
    (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
      (SetLike.le_def.mp le_sup_right <| subset_closure ht)

Premises used: Submonoid.mul_mem, le_sup_left, Set.Mem, SetLike.le_def, Membership.mem, Eq.rec, le_sup_right, SetLike.coe, Max.max, _private.0.Submonoid.closure_mul_le.match_1, sInf_le, Submonoid.closure, Iff.mp, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
n : ℕ
⊢ LE.le (α := Submonoid M) (closure (s ^ n)) (closure s)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
m n : ℕ
hmn : m ∣ n
obtain : ∀ (k : ℕ), LE.le (α := Submonoid M) (closure (s ^ (m * k))) (closure (s ^ m))
⊢ LE.le (α := Submonoid M) (closure (s ^ n)) (closure (s ^ m))

Tactic:
obtain ⟨k, rfl⟩ := hmn

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
m k : ℕ
⊢ LE.le (α := Submonoid M) (closure (s ^ (m * k))) (closure (s ^ m))

Tactic:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
grw grw₁ : LE.le (α := Submonoid M) (closure s) (closure s)
⊢ LE.le (α := Submonoid M) (closure s) (closure (s ^ n))

Tactic:
grw [← subset_pow hs hn]

Premises used: Set.subset_pow
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
H K : Submonoid M
rw : H ⊔ closure (↑K : Set M) ≤ H ⊔ K
rw₁ rw₂ : H ⊔ K ≤ H ⊔ K
⊢ closure (↑H : Set M) ⊔ closure (↑K : Set M) ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

Premises used: Submonoid.closure_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
N : Type u_7
inst : CommMonoid N
H K : Submonoid N
h : ∀ (x : N), x ∈ (↑(H ⊔ K) : Set N) ↔ x ∈ (↑H : Set N) * (↑K : Set N)
⊢ (↑(H ⊔ K) : Set N) = (↑H : Set N) * (↑K : Set N)

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
N : Type u_7
inst : CommMonoid N
H K : Submonoid N
x : N
⊢ x ∈ (↑(H ⊔ K) : Set N) ↔ x ∈ (↑H : Set N) * (↑K : Set N)

Tactic:
simp [mem_sup, Set.mem_mul]

Premises used: Submonoid.mem_sup, Set.mem_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x : N
hx : x ∈ s
rw rw₁ : (fun (x : N) ↦ r • x) x = r • x
⊢ (fun (x : N) ↦ r • x) x = HPow.hPow (β := ℕ) r 1 • x

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x : N
hx : x ∈ s
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)

Tactic:
exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
⊢ Membership.mem (γ := Submonoid N) (closure (r • s)) (HSMul.hSMul (β := N) (HPow.hPow (β := ℕ) r 0) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (HSMul.hSMul (β := N) (r ^ n) 1)

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
mul :
  ∀ (nx : ℕ) (hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)) (ny : ℕ)
    (hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)),
    ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))

Tactic:
obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy

Premises used: And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
h : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ (ny + nx) • (x * y))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))

Tactic:
use ny + nx
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
h : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y * r ^ nx • x)
⊢ Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ (ny + nx) • (x * y))

Tactic:
rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]

Premises used: pow_add, smul_mul_assoc, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
⊢ Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y * r ^ nx • x)

Tactic:
mul_mem hy hx

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
⊢ Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y * r ^ nx • x)

Tactic:
exact mul_mem hy hx

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
hx : Membership.mem (γ := Submonoid N) (closure s) x
mem : ∀ (x : N) (hx : x ∈ s), ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
one : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (HSMul.hSMul (β := N) (r ^ n) 1)
mul :
  ∀ (x y : N),
    Membership.mem (γ := Submonoid N) (closure s) x →
      Membership.mem (γ := Submonoid N) (closure s) y →
        ∀ (hx : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x))
          (hy : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)),
          ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)

Tactic:
induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simp⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx

Premises used: Submonoid.mul, pow_add, smul_mul_assoc, mul_comm, Submonoid.one, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
a b : G
ha : a ∈ (↑S : Set G)⁻¹
hb : b ∈ (↑S : Set G)⁻¹
rw : b⁻¹ * a⁻¹ ∈ (↑S : Set G)
⊢ a * b ∈ (↑S : Set G)⁻¹

Tactic:
rw [mem_inv, mul_inv_rev]

Premises used: mul_inv_rev, Set.mem_inv
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
a b : G
ha : a ∈ (↑S : Set G)⁻¹
hb : b ∈ (↑S : Set G)⁻¹
⊢ b⁻¹ * a⁻¹ ∈ (↑S : Set G)

Tactic:
mul_mem hb ha

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
a b : G
ha : a ∈ (↑S : Set G)⁻¹
hb : b ∈ (↑S : Set G)⁻¹
⊢ b⁻¹ * a⁻¹ ∈ (↑S : Set G)

Tactic:
exact mul_mem hb ha

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
rw : 1 ∈ (↑S : Set G)
⊢ 1⁻¹ ∈ (↑S : Set G)

Tactic:
rw [inv_one]

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
⊢ 1 ∈ (↑S : Set G)

Tactic:
S.one_mem'

Premises used: Set.Mem, Submonoid.one_mem'
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
⊢ 1 ∈ (↑S : Set G)

Tactic:
exact S.one_mem'

Premises used: Submonoid.one_mem'
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Submonoid G
⊢ (↑S⁻¹ : Set G) = (↑S : Set G)⁻¹

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
S : Submonoid G
⊢ g ∈ S⁻¹ ↔ g⁻¹ ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
S T : Submonoid G
⊢ S⁻¹ ≤ T⁻¹ ↔ S ≤ T

Tactic:
SetLike.coe_subset_coe.symm.trans Set.inv_subset_inv

Premises used: SetLike.coe_subset_coe, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
S T : Submonoid G
⊢ S⁻¹ ≤ T ↔ S ≤ T⁻¹

Tactic:
SetLike.coe_subset_coe.symm.trans Set.inv_subset

Premises used: SetLike.coe_subset_coe, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
a : LE.le (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
a₁ : LE.le (α := Submonoid G) (closure s)⁻¹ (closure s⁻¹)
⊢ Eq (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
a : s ⊆ (↑(closure s) : Set G)
⊢ LE.le (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹

Tactic:
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]

Premises used: Submonoid.coe_inv, inv_inv, Set.inv_subset, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ s ⊆ (↑(closure s) : Set G)

Tactic:
subset_closure

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ s ⊆ (↑(closure s) : Set G)

Tactic:
exact subset_closure

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
a : s⁻¹ ⊆ (↑(closure s⁻¹) : Set G)
⊢ LE.le (α := Submonoid G) (closure s)⁻¹ (closure s⁻¹)

Tactic:
rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]

Premises used: Submonoid.coe_inv, Submonoid.inv_le, Set.inv_subset, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ s⁻¹ ⊆ (↑(closure s⁻¹) : Set G)

Tactic:
subset_closure

Premises used: Set.Mem, setOf, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ s⁻¹ ⊆ (↑(closure s⁻¹) : Set G)

Tactic:
exact subset_closure

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
x : G
rw : Membership.mem (γ := Submonoid G) (closure s)⁻¹ x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
rw₁ rw₂ : Membership.mem (γ := Submonoid G) (closure s) x⁻¹ ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
⊢ Membership.mem (γ := Submonoid G) (closure s⁻¹) x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹

Tactic:
rw [closure_inv, mem_inv]

Premises used: Submonoid.mem_inv, Submonoid.closure_inv
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
S T : Submonoid G
⊢ (S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹

Tactic:
SetLike.coe_injective Set.inter_inv

Premises used: Set.inter_inv, SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
S T : Submonoid G
⊢ (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹

Tactic:
(invOrderIso : Submonoid G ≃o Submonoid G).map_sup S T

Premises used: Set.Mem, Submonoid.invOrderIso, setOf, OrderIso.map_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Submonoid G) ⊥⁻¹ ⊥

Tactic:
SetLike.coe_injective <| (Set.inv_singleton 1).trans <| congr_arg _ inv_one

Premises used: inv_one, SetLike.coe_injective, congr_arg, Set.inv_singleton, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
⊢ Eq.{u_2 + 1} (α := Submonoid G) ⊤⁻¹ ⊤

Tactic:
SetLike.coe_injective <| Set.inv_univ

Premises used: SetLike.coe_injective, Set.inv_univ
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_7
S : ι → Submonoid G
⊢ Eq.{u_2 + 1} (α := Submonoid G) (⨅ (i : ι), S i)⁻¹ (⨅ (i : ι), (S i)⁻¹)

Tactic:
(invOrderIso : Submonoid G ≃o Submonoid G).map_iInf _

Premises used: Submonoid.invOrderIso, OrderIso.map_iInf
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_7
S : ι → Submonoid G
⊢ Eq.{u_2 + 1} (α := Submonoid G) (⨆ (i : ι), S i)⁻¹ (⨆ (i : ι), (S i)⁻¹)

Tactic:
(invOrderIso : Submonoid G ≃o Submonoid G).map_iSup _

Premises used: Submonoid.invOrderIso, OrderIso.map_iSup
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : Monoid α
inst_3 : MulDistribMulAction α M
S : Submonoid M
⊢ map (F := Monoid.End M)
      (((MulDistribMulAction.toMonoidEnd α M : MonoidHom.{u_1, u_3} α (Monoid.End M)) : (a : α) → Monoid.End M) 1) S =
    S

Tactic:
simpa only [map_one] using S.map_id

Premises used: Submonoid.map_id, map_one
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
a : α
S : Submonoid M
⊢ (↑(a • S) : Set M) = a • (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
m : M
a : α
S : Submonoid M
⊢ m ∈ S → a • m ∈ a • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : Monoid α
inst_3 : MulDistribMulAction α M
⊢ CovariantClass α (Submonoid M) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => image_mono⟩

Premises used: CovariantClass.mk, Set.image_mono
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
m : M
a : α
S : Submonoid M
⊢ m ∈ a • S ↔ ∃ s ∈ S, a • s = m

Tactic:
(Set.mem_smul_set : m ∈ a • (S : Set M) ↔ _)

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
a : α
⊢ HSMul.hSMul (β := Submonoid M) a ⊥ = ⊥

Tactic:
map_bot _

Premises used: Submonoid.map_bot
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
a : α
S T : Submonoid M
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Set.Mem, setOf, Submonoid.map_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
a : α
s : Set M
⊢ HSMul.hSMul (β := Submonoid M) a (closure s) = closure (a • s)

Tactic:
MonoidHom.map_mclosure _ _

Premises used: MonoidHom.map_mclosure
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction α M
inst_3 : MulDistribMulAction.{u_1, u_3} αᵐᵒᵖ M
inst_4 : IsCentralScalar α M
⊢ IsCentralScalar.{u_1, u_3} α (Submonoid M)

Tactic:
⟨fun _ S => (congr_arg fun f : Monoid.End M => S.map f) <| MonoidHom.ext <| op_smul_eq_smul _⟩

Premises used: MonoidHom.ext, congr_arg, Submonoid.map, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S : Submonoid M
x : M
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S : Submonoid M
x : M
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S : Submonoid M
x : M
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S T : Submonoid M
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S T : Submonoid M
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction α M
a : α
S T : Submonoid M
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.Group.Submonoid.Pointwise
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
rw : IsPWO.{u_1} (α := α) (List.prod '' {l : List α | ∀ x ∈ l, x ∈ s})
⊢ (↑(Submonoid.closure s) : Set α).IsPWO

Tactic:
rw [Submonoid.closure_eq_image_prod]

Premises used: Submonoid.closure_eq_image_prod