awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul :
  HMul.hMul (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t ∪ u, x ^ g x) =
    HMul.hMul (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ u, x ^ g x)
⊢ ∏ a ∈ t ∪ u, a ^ (f + g) a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)

Tactic:
simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, pow_add, Pi.add_apply
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : Eq (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t, x ^ f x)
mul₁ : Eq (α := M) (∏ x ∈ t ∪ u, x ^ g x) (∏ x ∈ u, x ^ g x)
⊢ HMul.hMul (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t ∪ u, x ^ g x) =
    HMul.hMul (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ u, x ^ g x)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : Eq (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ t ∪ u, x ^ f x)
⊢ Eq (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t, x ^ f x)

Tactic:
symm
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : Eq (α := M) (∏ x ∈ u, x ^ g x) (∏ x ∈ t ∪ u, x ^ g x)
⊢ Eq (α := M) (∏ x ∈ t ∪ u, x ^ g x) (∏ x ∈ u, x ^ g x)

Tactic:
symm
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ t ∪ u, x ^ f x)

Tactic:
Finset.prod_subset Finset.subset_union_left ?_

Premises used: Finset.subset_union_left, Finset.prod_subset
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : ∀ x ∈ t ∪ u, x ∉ t → x ^ f x = 1
⊢ Eq (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ t ∪ u, x ^ f x)

Tactic:
refine Finset.prod_subset Finset.subset_union_left ?_

Premises used: Finset.subset_union_left, Finset.prod_subset
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ ∀ x ∈ t ∪ u, x ∉ t → x ^ f x = 1

Tactic:
simp +contextual [Function.support_subset_iff'.1 hf]

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ u, x ^ g x) (∏ x ∈ t ∪ u, x ^ g x)

Tactic:
Finset.prod_subset Finset.subset_union_right ?_

Premises used: Finset.prod_subset, Finset.subset_union_right
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : ∀ x ∈ t ∪ u, x ∉ u → x ^ g x = 1
⊢ Eq (α := M) (∏ x ∈ u, x ^ g x) (∏ x ∈ t ∪ u, x ^ g x)

Tactic:
refine Finset.prod_subset Finset.subset_union_right ?_

Premises used: Finset.prod_subset, Finset.subset_union_right
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ ∀ x ∈ t ∪ u, x ∉ u → x ^ g x = 1

Tactic:
simp +contextual [Function.support_subset_iff'.1 hg]

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
mem :
  ∀ (x : M) (hx : x ∈ s),
    ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
mul :
  ∀ (x y : M),
    Membership.mem (γ := Submonoid M) (closure s) x →
      Membership.mem (γ := Submonoid M) (closure s) y →
        ∀
          (hx :
            ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x)
          (hy :
            ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y),
          ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

Premises used: Finset.prod_mul_distrib, Submonoid.mul, pow_add, Finset.subset_union_left, Finset.prod_subset, Pi.add_apply, Submonoid.one, Finset.subset_union_right, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
mem :
  ∀ (x : M) (hx : x ∈ s),
    ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
mul :
  ∀ (x y : M),
    Membership.mem (γ := Submonoid M) (closure s) x →
      Membership.mem (γ := Submonoid M) (closure s) y →
        ∀
          (hx :
            ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x)
          (hy :
            ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y),
          ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

Premises used: Finset.prod_mul_distrib, Submonoid.mul, pow_add, Finset.subset_union_left, Finset.prod_subset, Pi.add_apply, Submonoid.one, Finset.subset_union_right, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Set M
n : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
⊢ Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ n a)

Tactic:
prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _

Premises used: Submonoid.prod_mem, pow_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Set M
n : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
⊢ Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ n a)

Tactic:
exact prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _

Premises used: Submonoid.prod_mem, pow_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Finset M
rw :
  (∃ (f : M → ℕ) (t : Finset M),
      (↑t : Set M) ⊆ (↑s : Set M) ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x) →
    ∃ (f : M → ℕ), Function.support f ⊆ (↑s : Set M) ∧ ∏ a ∈ s, a ^ f a = x
⊢ Membership.mem (γ := Submonoid M) (closure (↑s : Set M)) x →
    ∃ (f : M → ℕ), Function.support f ⊆ (↑s : Set M) ∧ ∏ a ∈ s, a ^ f a = x

Tactic:
rw [mem_closure_iff_exists_finset_subset]

Premises used: Submonoid.mem_closure_iff_exists_finset_subset
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
⊢ ∃ (f_1 : M → ℕ), Function.support f_1 ⊆ (↑s : Set M) ∧ Eq (α := M) (∏ a ∈ s, a ^ f_1 a) (∏ a ∈ t, a ^ f a)

Tactic:
⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩

Premises used: HasSubset.Subset.trans, Finset.prod_subset, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
refine : ∀ x ∈ s, x ∉ t → x ^ f x = 1
⊢ ∃ (f_1 : M → ℕ), Function.support f_1 ⊆ (↑s : Set M) ∧ Eq (α := M) (∏ a ∈ s, a ^ f_1 a) (∏ a ∈ t, a ^ f a)

Tactic:
refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
⊢ ∀ x ∈ s, x ∉ t → x ^ f x = 1

Tactic:
simp +contextual [Function.support_subset_iff'.1 hf]

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
n : M → ℕ
⊢ Membership.mem (γ := Submonoid M) (closure (↑s : Set M)) (∏ a ∈ s, a ^ n a)

Tactic:
prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _

Premises used: Submonoid.prod_mem, pow_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
n : M → ℕ
⊢ Membership.mem (γ := Submonoid M) (closure (↑s : Set M)) (∏ a ∈ s, a ^ n a)

Tactic:
exact prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _

Premises used: Submonoid.prod_mem, pow_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
S : Type u_3
M : Type u_4
inst : One M
inst_1 : SetLike S M
inst_2 : OneMemClass S M
s : S
⊢ (↑s : Set M).Nonempty

Tactic:
⟨1, one_mem s⟩

Premises used: Set.Nonempty, Exists.intro, OneMemClass.one_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
rw : 1 ∈ S
⊢ HPow.hPow (β := ℕ) x 0 ∈ S

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S

Tactic:
OneMemClass.one_mem S

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S

Tactic:
exact OneMemClass.one_mem S

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
rw : x ^ n * x ∈ S
⊢ x ^ (n + 1) ∈ S

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S

Tactic:
mul_mem (pow_mem hx n) hx

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S

Tactic:
exact mul_mem (pow_mem hx n) hx

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : Submonoid M
s : Subsemigroup M
hs : 1 ∈ s.carrier
t : Subsemigroup M
ht : 1 ∈ t.carrier
⊢ { toSubsemigroup := s, one_mem' := hs : Submonoid M }.toSubsemigroup =
      { toSubsemigroup := t, one_mem' := ht }.toSubsemigroup →
    { toSubsemigroup := s, one_mem' := hs : Submonoid M } = { toSubsemigroup := t, one_mem' := ht }

Tactic:
congr!
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s t : Submonoid M
⊢ s.toSubsemigroup = t.toSubsemigroup ↔ s = t

Tactic:
toSubsemigroup_injective.eq_iff

Premises used: Function.Injective.eq_iff, Submonoid.toSubsemigroup_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
x : M
⊢ x ∈ s.toSubsemigroup ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
x : M
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s : Subsemigroup M
x : M
h_one : 1 ∈ s.carrier
⊢ x ∈ { toSubsemigroup := s, one_mem' := h_one : Submonoid M } ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s : Subsemigroup M
h_one : 1 ∈ s.carrier
⊢ (↑{ toSubsemigroup := s, one_mem' := h_one : Submonoid M } : Set M) = (↑s : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
s t : Subsemigroup M
h_one : 1 ∈ s.carrier
h_one' : 1 ∈ t.carrier
⊢ { toSubsemigroup := s, one_mem' := h_one : Submonoid M } ≤ { toSubsemigroup := t, one_mem' := h_one' } ↔ s ≤ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
h : ∀ (x : M), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
s : Set M
hs : s = (↑S : Set M)
⊢ (↑(S.copy s hs) : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
s : Set M
hs : s = (↑S : Set M)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ 1 ∈ S

Tactic:
one_mem S

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
x y : M
⊢ x ∈ S → y ∈ S → x * y ∈ S

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
ha : Membership.mem (γ := Set M) {1} a
hb : Membership.mem (γ := Set M) {1} b
⊢ b = 1

Tactic:
push _ ∈ _ at *
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
ha : Membership.mem (γ := Set M) {1} a
hb : Membership.mem (γ := Set M) {1} b
hb₁ : b = 1
⊢ a = 1

Tactic:
push _ ∈ _ at *
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
hb : b = 1
ha : a = 1
rw : 1 * b = 1
rw₁ : HMul.hMul (α := M) 1 1 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ a * b = 1

Tactic:
rw [ha, hb, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
x : M
⊢ Membership.mem (γ := Submonoid M) ⊥ x ↔ x = 1

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
x : M
⊢ Membership.mem (γ := Submonoid M) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
⊢ (↑⊤ : Set M) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
⊢ (↑⊥ : Set M) = {1}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid M } = ⊤ ↔ toSubsemigroup = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid M } = ⊥ ↔ (↑toSubsemigroup : Set M) = {1}

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
p p' : Submonoid M
⊢ (↑(p ⊓ p') : Set M) = (↑p : Set M) ∩ (↑p' : Set M)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
p p' : Submonoid M
x : M
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
h : Subsingleton M
x y : Submonoid M
i : M
⊢ i ∈ x ↔ i ∈ y

Tactic:
simp [← Subsingleton.elim 1 i]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Nontrivial.{u_1} (Submonoid M) ↔ Nontrivial M

Tactic:
not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
      not_nontrivial_iff_subsingleton.symm)

Premises used: not_iff_not, not_nontrivial_iff_subsingleton, Iff.mp, Submonoid.subsingleton_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
inst_1 : Nontrivial M
⊢ Nontrivial.{u_1} (Submonoid M)

Tactic:
nontrivial_iff.mpr ‹_›

Premises used: Iff.mpr, Submonoid.nontrivial_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
inst_1 : MulOneClass N
f g : M →* N
a b : M
hx : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((g : (a : M) → N) a : N)
hy : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) b : N) ((g : (a : M) → N) b : N)
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
    (a * b)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
inst_1 : MulOneClass N
f g : M →* N
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N)
rw₁ : Eq.{u_2 + 1} (α := N) (1 : N) ((g : (a : M) → N) 1 : N)
rw₂ rw₃ : Eq.{u_2 + 1} (α := N) 1 1
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)} 1

Tactic:
rw [Set.mem_setOf_eq, f.map_one, g.map_one]

Premises used: Set.mem_setOf_eq, MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f g : M →* N
x : M
⊢ x ∈ f.eqLocusM g ↔ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
⊢ f.eqLocusM f = ⊤

Tactic:
SetLike.ext fun _ => eq_self_iff_true _

Premises used: SetLike.ext, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f g : M →* N
h : Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) (↑⊤ : Set M)
⊢ f = g

Tactic:
ext fun _ => h trivial

Premises used: trivial, MonoidHom.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
A : Type u_3
M₁ : Type u_4
inst : SetLike A M₁
inst_1 : One M₁
hA : OneMemClass A M₁
S' : A
⊢ Eq.{u_4 + 1} (α := M₁) (↑1 : M₁) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
A : Type u_3
M₁ : Type u_4
inst : SetLike A M₁
inst_1 : One M₁
hA : OneMemClass A M₁
S' : A
x : ↥S'
⊢ (↑x : M₁) = 1 ↔ x = 1

Tactic:
(Subtype.ext_iff.symm : (x : M₁) = (1 : S') ↔ x = 1)

Premises used: Subtype.ext_iff, Iff.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
A : Type u_3
M₁ : Type u_4
inst : SetLike A M₁
inst_1 : One M₁
hA : OneMemClass A M₁
S' : A
⊢ Eq (α := ↥S') 1 (Subtype.mk (p := fun (x : M₁) ↦ x ∈ S') 1 ⋯)

Tactic:
rfl

Premises used: rfl