awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : Membership.mem (γ := Subsemigroup M) (closure s) y
z : M
hz : z ∈ s
mem₁ : ∀ (x : M) (h : x ∈ s), p z x ⋯ ⋯
mem₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (h₁ : p z x ⋯ hx) (h₂ : p z y ⋯ hy), p z (x * y) ⋯ ⋯
⊢ p z y ⋯ hy

Tactic:
induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : Membership.mem (γ := Subsemigroup M) (closure s) y
x_1 y_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure s) x_1
hy_1 : Membership.mem (γ := Subsemigroup M) (closure s) y_1
h₁ : p x_1 y hx hy
h₂ : p y_1 y hy_1 hy
⊢ p (x_1 * y_1) y ⋯ hy

Tactic:
mul_left _ _ _ _ _ hy h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : Membership.mem (γ := Subsemigroup M) (closure s) y
x_1 y_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure s) x_1
hy_1 : Membership.mem (γ := Subsemigroup M) (closure s) y_1
h₁ : p x_1 y hx hy
h₂ : p y_1 y hy_1 hy
⊢ p (x_1 * y_1) y ⋯ hy

Tactic:
exact mul_left _ _ _ _ _ hy h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x_1 : M
h : x_1 ∈ s
⊢ p x_1

Tactic:
mem _ h
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x_1 : M
h : x_1 ∈ s
⊢ p x_1

Tactic:
exact mem _ h
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x_1 y : M
hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x_1
hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) y
h₁ : p x_1
h₂ : p y
⊢ p (x_1 * y)

Tactic:
mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x_1 y : M
hx : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x_1
hy : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) y
h₁ : p x_1
h₂ : p y
⊢ p (x_1 * y)

Tactic:
exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤

Tactic:
closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤

Tactic:
exact closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
mem x hx
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
exact mem x hx
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x y : M
h₁ : p x
h₂ : p y
⊢ p (x * y)

Tactic:
mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x y : M
h₁ : p x
h₂ : p y
⊢ p (x * y)

Tactic:
exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s_1 : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
closure₁ : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem₁ : ∀ (x : M) (hx : x ∈ s), p x
mul₁ : ∀ (x y : M) (h₁ : p x) (h₂ : p y), p (x * y)
⊢ p x

Tactic:
induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup M
⊢ closure (↑S : Set M) = S

Tactic:
(Subsemigroup.gi M).l_u_eq S

Premises used: Subsemigroup.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := Subsemigroup M) (closure ∅) ⊥

Tactic:
(Subsemigroup.gi M).gc.l_bot

Premises used: Subsemigroup.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := Subsemigroup M) (closure univ) ⊤

Tactic:
@coe_top M _ ▸ closure_eq ⊤

Premises used: Eq.rec, Subsemigroup.closure_eq, Subsemigroup.coe_top, Top.top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
s t : Set M
⊢ Eq (α := Subsemigroup M) (closure (s ∪ t)) (closure s ⊔ closure t)

Tactic:
(Subsemigroup.gi M).gc.l_sup

Premises used: Subsemigroup.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
s : ι → Set M
⊢ Eq.{u_1 + 1} (α := Subsemigroup M) (closure (⋃ (i : ι), s i)) (⨆ (i : ι), closure (s i))

Tactic:
(Subsemigroup.gi M).gc.l_iSup

Premises used: Subsemigroup.gi, GaloisConnection.l_iSup, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
m : M
p : Subsemigroup M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
rw₂ rw₃ : m ∈ p ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, Subsemigroup.closure_le, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
rw :
  (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), p i) m ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Premises used: Subsemigroup.closure_singleton_le_iff_mem, le_iSup_iff
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

Premises used: Subsemigroup.closure_singleton_le_iff_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
simp_rw : Eq.{u_1 + 1} (α := Subsemigroup M) (⨆ (i : ι), p i) (⨆ (i : ι), closure (↑(p i) : Set M))
⊢ Eq.{u_1 + 1} (α := Subsemigroup M) (⨆ (i : ι), p i) (closure (⋃ (i : ι), (↑(p i) : Set M)))

Tactic:
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

Premises used: Subsemigroup.closure_iUnion, Subsemigroup.closure_eq
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f g : M →ₙ* N
s : Set M
h : Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) (↑(closure s) : Set M)

Tactic:
show closure s ≤ f.eqLocus g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Subsemigroup.closure_le, Set.EqOn
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
s : Set M
hs : Eq (α := Subsemigroup M) (closure s) ⊤
f g : M →ₙ* N
h : Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ f = g

Tactic:
eq_of_eqOn_top <| hs ▸ eqOn_closure h

Premises used: Eq.rec, MulHom.eqOn_closure, MulHom.eq_of_eqOn_top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M_1 : Type u_1
N_1 : Type u_2
M : Type u_3
N : Type u_4
inst : Semigroup M
inst_1 : Semigroup N
s : Set M
f : M → N
hs : Eq (α := Subsemigroup M) (closure s) ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x_1 y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
simp only [← mul_assoc, h₁, h₂]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subsemigroup.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Semigroup M
inst_1 : Semigroup N
s : Set M
f : M → N
hs : Eq (α := Subsemigroup M) (closure s) ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
⊢ (⇑(ofDense (s := s) f hs hmul) : (a : M) → N) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
p q : Subsemigroup M
h : p.carrier = q.carrier
mk :
  ∀ (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
    (h : { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier = q.carrier),
    { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
q : Subsemigroup M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
h : { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier = q.carrier
mk :
  ∀ (carrier_1 : Set M) (mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1)
    (h :
      { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier =
        { carrier := carrier_1, mul_mem' := @mul_mem'_1 : Subsemigroup M }.carrier),
    { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = { carrier := carrier_1, mul_mem' := @mul_mem'_1 }
⊢ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
carrier_1 : Set M
mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1
h :
  { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier =
    { carrier := carrier_1, mul_mem' := @mul_mem'_1 : Subsemigroup M }.carrier
⊢ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = { carrier := carrier_1, mul_mem' := @mul_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
s : Subsemigroup M
x : M
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
s : Set M
x : M
h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
⊢ x ∈ { carrier := s, mul_mem' := @h_mul : Subsemigroup M } ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
s : Set M
h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
⊢ (↑{ carrier := s, mul_mem' := @h_mul : Subsemigroup M } : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
s t : Set M
h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t
⊢ { carrier := s, mul_mem' := @h_mul : Subsemigroup M } ≤ { carrier := t, mul_mem' := @h_mul' } ↔ s ⊆ t

Tactic:
Iff.rfl

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

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup 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.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup 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.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup M
x y : M
⊢ x ∈ S → y ∈ S → x * y ∈ S

Tactic:
Subsemigroup.mul_mem' S

Premises used: Set.Mem, Subsemigroup.mul_mem'
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
x : M
⊢ ¬Membership.mem (γ := Subsemigroup M) ⊥ x

Tactic:
Set.notMem_empty x

Premises used: Set.Mem, Set.notMem_empty
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
x : M
⊢ Membership.mem (γ := Subsemigroup M) ⊤ x

Tactic:
Set.mem_univ x

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

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
⊢ (↑⊥ : Set M) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = ⊤ ↔ carrier = Set.univ

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = ⊥ ↔ carrier = ∅

Tactic:
simp [← SetLike.coe_set_eq]

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

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
p p' : Subsemigroup 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.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
allEq : ∀ (a b : M), a = b
⊢ Subsingleton M

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
x y : M
⊢ ∀ (a : M), Membership.mem (γ := Subsemigroup M) ⊥ a

Tactic:
simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]

Premises used: Bot.bot, Subsingleton.elim, Top.top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
x y : M
⊢ ∀ (a : M), Membership.mem (γ := Subsemigroup M) ⊥ a

Tactic:
have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
x y : M
this : ∀ (a : M), Membership.mem (γ := Subsemigroup M) ⊥ a
⊢ x = y

Tactic:
absurd (this x) notMem_bot

Premises used: Subsemigroup.notMem_bot, absurd
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
x y : M
this : ∀ (a : M), Membership.mem (γ := Subsemigroup M) ⊥ a
⊢ x = y

Tactic:
exact absurd (this x) notMem_bot

Premises used: Subsemigroup.notMem_bot, absurd
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : Eq.{u_1 + 1} (α := Subsemigroup M) ⊥ ⊤
obtain : ∀ (x : M), False
⊢ False

Tactic:
obtain ⟨x⟩ := id hn

Premises used: id
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : Eq.{u_1 + 1} (α := Subsemigroup M) ⊥ ⊤
x : M
⊢ False

Tactic:
absurd (?_ : x ∈ ⊥) notMem_bot

Premises used: Subsemigroup.notMem_bot, absurd
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : Eq.{u_1 + 1} (α := Subsemigroup M) ⊥ ⊤
x : M
⊢ Membership.mem (γ := Subsemigroup M) ⊥ x

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
inst_1 : Mul 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.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f g : M →ₙ* N
x : M
⊢ x ∈ f.eqLocus 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.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul 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, MulHom.ext
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
x y : ↥S'
⊢ (↑(x * y) : M) = (↑x : M) * (↑y : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
x y : M
hx : x ∈ S'
hy : y ∈ S'
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S') x hx * Subtype.mk (p := fun (x : M) ↦ x ∈ S') y hy =
    Subtype.mk (p := fun (x : M) ↦ x ∈ S') (x * y) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
x y : ↥S'
⊢ x * y = Subtype.mk (p := fun (x : M) ↦ x ∈ S') ((↑x : M) * (↑y : M)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
inst_2 : IsLeftCancelMul M
S : A
⊢ IsLeftCancelMul.{u_1} ↥S

Tactic:
Subtype.coe_injective.isLeftCancelMul Subtype.val fun _ _ => rfl

Premises used: Subtype.coe_injective, Subtype.val, Function.Injective.isLeftCancelMul, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
inst_2 : IsRightCancelMul M
S : A
⊢ IsRightCancelMul.{u_1} ↥S

Tactic:
Subtype.coe_injective.isRightCancelMul Subtype.val fun _ _ => rfl

Premises used: Function.Injective.isRightCancelMul, Subtype.coe_injective, Subtype.val, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
x : ↥S'
⊢ (subtype S' : (a : ↥S') → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
⊢ Function.Injective (α := ↥S') (β := M) (⇑(subtype S') : (a : ↥S') → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
M : Type u_1
A : Type u_3
inst : Mul M
inst_1 : SetLike A M
hA : MulMemClass A M
S' : A
⊢ Eq (α := (a : ↥S') → M) (⇑(subtype S') : (a : ↥S') → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S'))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
S : Type u_3
M : Type u_4
inst : SetLike S M
inst_1 : Mul M
inst_2 : MulMemClass S M
s : S
⊢ IsMulCommutative.{u_4} ↥s ↔ ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a

Tactic:
simp [isMulCommutative_iff]

Premises used: isMulCommutative_iff
-- Module: Mathlib.Algebra.Group.Subsemigroup.Defs
Goal:
S : Type u_3
M : Type u_4
inst : SetLike S M
inst_1 : Mul M
inst_2 : MulMemClass S M
s : S
inst_3 : IsMulCommutative.{u_4} ↥s
a b : M
ha : a ∈ s
hb : b ∈ s
⊢ a * b = b * a

Tactic:
isMulCommutative_iff_of_setLike.mp ‹_› a ha b hb

Premises used: Iff.mp, isMulCommutative_iff_of_setLike