awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : M
⊢ Membership.mem (γ := Submonoid M) (mker (F := M →* M × N) (inl M N)) x ↔ Membership.mem (γ := Submonoid M) ⊥ x

Tactic:
simp [mem_mker]

Premises used: MonoidHom.mem_mker
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
h :
  ∀ (x : N),
    Membership.mem (γ := Submonoid N) (mker (F := N →* M × N) (inr M N)) x ↔ Membership.mem (γ := Submonoid N) ⊥ x
⊢ Eq (α := Submonoid N) (mker (F := N →* M × N) (inr M N)) ⊥

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : N
⊢ Membership.mem (γ := Submonoid N) (mker (F := N →* M × N) (inr M N)) x ↔ Membership.mem (γ := Submonoid N) ⊥ x

Tactic:
simp [mem_mker]

Premises used: MonoidHom.mem_mker
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mker (F := M × N →* M) (fst M N)) (prod ⊥ ⊤)

Tactic:
SetLike.ext fun _ => (iff_of_eq (and_true _)).symm

Premises used: MonoidHom.mker, and_true, Membership.mem, SetLike.ext, MonoidHom.fst, Iff.symm, iff_of_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mker (F := M × N →* N) (snd M N)) (prod ⊤ ⊥)

Tactic:
SetLike.ext fun _ => (iff_of_eq (true_and _)).symm

Premises used: MonoidHom.mker, Membership.mem, SetLike.ext, Iff.symm, true_and, MonoidHom.snd, iff_of_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
obtain :
  ∀ (x : M) (hx : (f : (a : M) → N) x = (↑y : N)),
    ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y
⊢ ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y

Tactic:
obtain ⟨x, hx⟩ := hf y

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
x : M
hx : (f : (a : M) → N) x = (↑y : N)
h :
  (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x ⋯) =
    y
⊢ ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y

Tactic:
use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
x : M
hx : (f : (a : M) → N) x = (↑y : N)
h :
  (↑((f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x ⋯)) :
      N) =
    (↑y : N)
⊢ (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x ⋯) =
    y

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
x : M
hx : (f : (a : M) → N) x = (↑y : N)
⊢ (↑((f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x ⋯)) :
      N) =
    (↑y : N)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ (a : ↥M'),
    Eq.{u_2 + 1} (α := ↥(map f M')) ((f.submonoidMap M' : (a : ↥M') → ↥(map f M')) a : ↥(map f M'))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (map f M') x) ((f : (a : M) → N) x) ⋯ :
        ↥(map f M'))

Tactic:
⟨⟨x, hx⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ (a : ↥M'),
    Eq.{u_2 + 1} (α := ↥(map f M')) ((f.submonoidMap M' : (a : ↥M') → ↥(map f M')) a : ↥(map f M'))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (map f M') x) ((f : (a : M) → N) x) ⋯ :
        ↥(map f M'))

Tactic:
exact ⟨⟨x, hx⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
M' : Submonoid M
⊢ Injective.{u_1 + 1, u_2 + 1} (α := ↥M') (β := ↥(map f M')) (⇑(f.submonoidMap M') : (a : ↥M') → ↥(map f M'))

Tactic:
grind [Injective, submonoidMap_apply_coe]

Premises used: MonoidHom.submonoidMap_apply_coe, Function.Injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
H : Submonoid M
K : Submonoid N
⊢ Set.SurjOn (⇑f : (a : M) → N) (↑H : Set M) (↑K : Set N) ↔ K ≤ map f H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.SurjOn, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mrange (F := M →* M × N) (inl M N)) (prod ⊤ ⊥)

Tactic:
simpa only [mrange_eq_map] using map_inl ⊤

Premises used: MonoidHom.mrange_eq_map, Submonoid.map_inl, Top.top
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mrange (F := N →* M × N) (inr M N)) (prod ⊥ ⊤)

Tactic:
simpa only [mrange_eq_map] using map_inr ⊤

Premises used: Submonoid.map_inr, MonoidHom.mrange_eq_map, Top.top
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mrange (F := M →* M × N) (inl M N)) (comap (F := M × N →* N) (snd M N) ⊥)

Tactic:
mrange_inl.trans (top_prod _)

Premises used: Submonoid.top_prod, Submonoid.mrange_inl, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mrange (F := N →* M × N) (inr M N)) (comap (F := M × N →* M) (fst M N) ⊥)

Tactic:
mrange_inr.trans (prod_top _)

Premises used: Submonoid.prod_top, Submonoid.mrange_inr, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid M) (mrange (F := M × N →* M) (fst M N)) ⊤

Tactic:
mrange_eq_top_of_surjective (fst M N) <| @Prod.fst_surjective _ _ ⟨1⟩

Premises used: Prod.fst_surjective, MonoidHom.fst, MonoidHom.mrange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid N) (mrange (F := M × N →* N) (snd M N)) ⊤

Tactic:
mrange_eq_top_of_surjective (snd M N) <| @Prod.snd_surjective _ _ ⟨1⟩

Premises used: MonoidHom.mrange_eq_top_of_surjective, Prod.snd_surjective, MonoidHom.snd
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

Tactic:
simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot', mker_inl, mker_inr]

Premises used: GaloisConnection.le_iff_le, MonoidHom.mker_inl, MonoidHom.comap_bot', MonoidHom.mker_inr, Submonoid.gc_map_comap, Submonoid.prod_le_iff, eq_bot_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, ← mrange_eq_map, mrange_fst, mrange_snd]

Premises used: eq_top_iff, MonoidHom.mrange_eq_map, Submonoid.le_prod_iff, Submonoid.mrange_snd, Submonoid.mrange_fst
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M × N)) (mrange (F := M →* M × N) (inl M N) ⊔ mrange (F := N →* M × N) (inr M N)) ⊤

Tactic:
simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

Premises used: Submonoid.prod_bot_sup_bot_prod, Submonoid.mrange_inr, Submonoid.top_prod_top, Submonoid.mrange_inl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
h : S ≤ T
a : ↥S
⊢ (↑((inclusion h : (a : ↥S) → ↥T) a) : M) = (↑a : M)

Tactic:
Set.coe_inclusion h a

Premises used: Set.coe_inclusion
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
h : S ≤ T
⊢ Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

Tactic:
Set.inclusion_injective h

Premises used: Set.inclusion_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
h : S ≤ T
x y : ↥S
⊢ Eq (α := ↥T) ((inclusion h : (a : ↥S) → ↥T) x : ↥T) ((inclusion h : (a : ↥S) → ↥T) y : ↥T) ↔ x = y

Tactic:
(inclusion_injective h).eq_iff

Premises used: Function.Injective.eq_iff, Submonoid.inclusion_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S T : Submonoid M
h : S ≤ T
⊢ T.subtype.comp (inclusion h) = S.subtype

Tactic:
rfl

Premises used: Set.Mem, Submonoid.subtype, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
s : Submonoid M
⊢ mrange s.subtype = s

Tactic:
SetLike.coe_injective <| (coe_mrange _).trans <| Subtype.range_coe

Premises used: MonoidHom.coe_mrange, SetLike.coe_injective, Subtype.range_coe, Eq.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ S = ⊤ ↔ ∀ (x : M), x ∈ S

Tactic:
eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Premises used: Submonoid.mem_top, eq_top_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ (∀ (x : M), x ∈ S ↔ Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ x ∈ S, x = 1

Tactic:
simp +contextual [iff_def, S.one_mem]

Premises used: iff_def, Submonoid.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
inst_1 : Subsingleton.{u_1 + 1} ↥S
rw : ∀ x ∈ S, x = 1
⊢ S = ⊥

Tactic:
rw [eq_bot_iff_forall]

Premises used: Submonoid.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
inst_1 : Subsingleton.{u_1 + 1} ↥S
y : M
hy : y ∈ S
⊢ y = 1

Tactic:
simpa using congr_arg ((↑) : S → M) <| Subsingleton.elim (⟨y, hy⟩ : S) 1

Premises used: Subtype.mk, congr_arg, Subsingleton.elim, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ (∃ (x : M) (hx : x ∈ S), Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ≠ Subtype.mk (p := fun (x : M) ↦ x ∈ S) 1 ⋯) ↔
    ∃ x ∈ S, x ≠ 1

Tactic:
simp [Ne]

Premises used: Ne
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ S = ⊥ ∨ Nontrivial.{u_1} ↥S

Tactic:
simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← Classical.not_imp,
    Classical.em]

Premises used: Submonoid.eq_bot_iff_forall, Submonoid.nontrivial_iff_exists_ne_one, Classical.not_imp, Classical.em, Classical.not_forall
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
⊢ S = ⊥ ∨ ∃ x ∈ S, x ≠ 1

Tactic:
S.bot_or_nontrivial.imp_right S.nontrivial_iff_exists_ne_one.mp

Premises used: Submonoid.nontrivial_iff_exists_ne_one, Iff.mp, Or.imp_right, Submonoid.bot_or_nontrivial
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint H K
rw : Eq (α := Submonoid N) (map f H ⊔ map f K) ⊤
rw₁ : Eq (α := Submonoid N) (map f (H ⊔ K)) ⊤
rw₂ : Eq (α := Submonoid N) (map f ⊤) ⊤
rw₃ : Eq (α := Submonoid N) (mrange f) ⊤
rw₄ rw₅ : Eq.{u_2 + 1} (α := Submonoid N) ⊤ ⊤
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)

Tactic:
rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]

Premises used: MonoidHom.mrange_eq_map, codisjoint_iff, Submonoid.map_sup, Iff.mp, MonoidHom.mrange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
I : Set ι
S : (i : ι) → Submonoid (M i)
⊢ (↑(pi (M := M) I S) : Set ((i : ι) → M i)) = I.pi (α := M) fun (i : ι) ↦ (↑(S i) : Set (M i))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.pi, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
I : Set ι
S : (i : ι) → Submonoid (M i)
p : (i : ι) → M i
⊢ p ∈ pi (M := M) I S ↔ ∀ i ∈ I, p i ∈ S i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
I : Set ι
x : (i : ι) → M i
⊢ Membership.mem (γ := Submonoid ((i : ι) → M i)) (pi (M := M) I fun (i : ι) ↦ ⊤) x ↔
    Membership.mem (γ := Submonoid ((i : ι) → M i)) ⊤ x

Tactic:
simp [mem_pi]

Premises used: Submonoid.mem_pi
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
H : (i : ι) → Submonoid (M i)
x : (i : ι) → M i
⊢ x ∈ pi (M := M) ∅ H ↔ Membership.mem (γ := Submonoid ((i : ι) → M i)) ⊤ x

Tactic:
simp [mem_pi]

Premises used: Submonoid.mem_pi
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
x : (i : ι) → M i
⊢ Membership.mem (γ := Submonoid ((i : ι) → M i)) (pi (M := M) Set.univ fun (i : ι) ↦ ⊥) x ↔
    Membership.mem (γ := Submonoid ((i : ι) → M i)) ⊥ x

Tactic:
simp [mem_pi, funext_iff]

Premises used: Submonoid.mem_pi, funext_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
I : Set ι
S : (i : ι) → Submonoid (M i)
J : Submonoid ((i : ι) → M i)
⊢ J ≤ pi (M := M) I S ↔ ∀ i ∈ I, J ≤ comap (F := ((i : ι) → M i) →* M i) (Pi.evalMonoidHom M i) (S i)

Tactic:
Set.subset_pi_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.pi, Set.subset_pi_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
inst_1 : DecidableEq ι
I : Set ι
S : (i : ι) → Submonoid (M i)
i : ι
x : M i
⊢ Pi.mulSingle (M := M) i x ∈ pi (M := M) I S ↔ i ∈ I → x ∈ S i

Tactic:
Set.update_mem_pi_iff_of_mem (one_mem (pi I _))

Premises used: Set.Mem, setOf, Set.update_mem_pi_iff_of_mem, Submonoid.pi, Set.pi, OneMemClass.one_mem, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
simp_rw :
  (↑(pi (M := M) Set.univ S) : Set ((i : ι) → M i)) = (↑⊥ : Set ((i : ι) → M i)) ↔
    ∀ (i : ι), (↑(S i) : Set (M i)) = (↑⊥ : Set (M i))
⊢ pi (M := M) Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ (↑(pi (M := M) Set.univ S) : Set ((i : ι) → M i)) = (↑⊥ : Set ((i : ι) → M i)) ↔
    ∀ (i : ι), (↑(S i) : Set (M i)) = (↑⊥ : Set (M i))

Tactic:
Set.univ_pi_eq_singleton_iff

Premises used: setOf, Set.singleton, Set.univ_pi_eq_singleton_iff, Set.pi
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ (↑(pi (M := M) Set.univ S) : Set ((i : ι) → M i)) = (↑⊥ : Set ((i : ι) → M i)) ↔
    ∀ (i : ι), (↑(S i) : Set (M i)) = (↑⊥ : Set (M i))

Tactic:
exact Set.univ_pi_eq_singleton_iff

Premises used: Set.univ_pi_eq_singleton_iff
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
inst_1 : DecidableEq ι
S : (i : ι) → Submonoid (M i)
I : Set ι
i : ι
x : M i
hx : x ∈ S i
⊢ Membership.mem (γ := Submonoid (M i)) (comap (F := M i →* (i : ι) → M i) (mulSingle M i) (pi (M := M) I S)) x

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
inst_1 : DecidableEq ι
I : Set ι
S : (i : ι) → Submonoid (M i)
⊢ ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (mulSingle M i) (S i) ≤ pi (M := M) I S

Tactic:
iSup_le fun _ => map_le_iff_le_comap.mpr (le_comap_mulSingle_pi _)

Premises used: Iff.mpr, Submonoid.map_le_iff_le_comap, Submonoid.le_comap_mulSingle_pi, iSup_le
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S T : Submonoid M
f : M →* N
g : N → M
h : LeftInverse g (⇑f : (a : M) → N)
x : ↥(MonoidHom.mrange f)
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x' : N) ((f : (a : M) → N) x' : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
S : Submonoid M
g : ↥S
⊢ Eq.{u_2 + 1} (α := N) ((↑((e.submonoidMap S : (a : ↥S) → ↥(Submonoid.map e S)) g) : N) : N)
    ((e : (a : M) → N) (↑g : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
S : Submonoid M
g : ↥(Submonoid.map (F := M →* N) (↑e : M →* N) S)
⊢ Eq.{u_1 + 1} (α := ↥S) (((e.submonoidMap S).symm : (a : ↥(Submonoid.map e S)) → ↥S) g : ↥S)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((e.symm : (a : N) → M) (↑g : N)) ⋯ : ↥S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
S : Submonoid M
e : M ≃* N
h :
  ∀ (x : ↥S),
    Eq.{u_2 + 1} (α := N)
      (↑(((S.equivMapOfInjective (↑e : M →* N) ⋯ : MulEquiv.{u_1, u_2} ↥S ↥(map (F := M →* N) (↑e : M →* N) S)) :
              (a : ↥S) → ↥(map (↑e : M →* N) S))
            x) :
        N)
      (↑((e.submonoidMap S : (a : ↥S) → ↥(map (↑e : M →* N) S)) x) : N)
⊢ S.equivMapOfInjective (↑e : M →* N) ⋯ = e.submonoidMap S

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
S : Submonoid M
e : M ≃* N
x : ↥S
⊢ Eq.{u_2 + 1} (α := N)
    (↑(((S.equivMapOfInjective (↑e : M →* N) ⋯ : MulEquiv.{u_1, u_2} ↥S ↥(map (F := M →* N) (↑e : M →* N) S)) :
            (a : ↥S) → ↥(map (↑e : M →* N) S))
          x) :
      N)
    (↑((e.submonoidMap S : (a : ↥S) → ↥(map (↑e : M →* N) S)) x) : N)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
M' : Type u_4
α : Type u_5
inst_3 : MulOneClass M'
inst_4 : SMul M' α
S : Submonoid M'
inst_5 : FaithfulSMul M' α
⊢ FaithfulSMul.{u_4, u_5} (↥S) α

Tactic:
⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩

Premises used: FaithfulSMul.eq_of_smul_eq_smul, FaithfulSMul.mk, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M_1 : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M_1
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M_1
M : Type u_4
inst_3 : Monoid M
x : ↥(IsUnit.submonoid M)
simp_rw simp_rw₁ :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑(IsUnit.unit ⋯) : M) ⋯ = x
⊢ (fun (x : Mˣ) ↦ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) ⋯)
      ((fun (x : ↥(IsUnit.submonoid M)) ↦ IsUnit.unit ⋯) x) =
    x

Tactic:
simp_rw [IsUnit.unit_spec]

Premises used: IsUnit.unit_spec
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M_1 : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M_1
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M_1
M : Type u_4
inst_3 : Monoid M
x y : Mˣ
simp_rw :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) ((↑x : M) * (↑y : M)) ⋯ =
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) ⋯ *
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑y : M) ⋯
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑(x * y) : M) ⋯ =
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) ⋯ *
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑y : M) ⋯

Tactic:
simp_rw [Units.val_mul]

Premises used: Units.val_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M_1 : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M_1
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M_1
M : Type u_4
inst_3 : Monoid M
x y : Mˣ
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) ((↑x : M) * (↑y : M)) ⋯ =
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) ⋯ *
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑y : M) ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ map f (comap f S) = S ⊓ MonoidHom.mrange f

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Premises used: Submonoid.map_comap_eq, inf_of_le_left
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
h : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid N
⊢ map f (comap f S) = S

Tactic:
map_comap_eq_self (MonoidHom.mrange_eq_top_of_surjective _ h ▸ le_top)

Premises used: Eq.rec, le_top, MonoidHom.mrange_eq_top_of_surjective, Submonoid.map_comap_eq_self, Eq.symm
-- 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 : S
⊢ (↑H : Set M) * (↑H : Set M) = (↑H : Set M)

Tactic:
aesop (add simp mem_mul)

Premises used: Set.mem_mul