awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
s : Set Mᵐᵒᵖ
rw : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
⊢ Eq (α := Submonoid M) (Submonoid.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))

Tactic:
rw [← op_inj, op_unop, op_closure]

Premises used: Submonoid.op_inj, Submonoid.op_unop, Submonoid.op_closure
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
s : Set Mᵐᵒᵖ
simp_rw : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
simp_rw₁ : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ x) ⁻¹' s))
⊢ Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Premises used: Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id'
-- 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 x : Submonoid M
mk :
  ∀ (toSubsemigroup : Subsemigroup M) (one_mem' : 1 ∈ toSubsemigroup.carrier),
    (fun (S : AddSubmonoid (Additive M)) ↦
          ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid M))
        ((fun (S : Submonoid M) ↦
            ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
              AddSubmonoid (Additive M)))
          { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
      { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid M }
⊢ (fun (S : AddSubmonoid (Additive M)) ↦
        ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid M))
      ((fun (S : Submonoid M) ↦
          ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid (Additive M)))
        x) =
    x

Tactic:
cases x
-- 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 : Submonoid M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ (fun (S : AddSubmonoid (Additive M)) ↦
        ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid M))
      ((fun (S : Submonoid M) ↦
          ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid (Additive M)))
        { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
    { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid M }

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 : Submonoid M
x : AddSubmonoid (Additive M)
mk :
  ∀ (toAddSubsemigroup : AddSubsemigroup (Additive M)) (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
    (fun (S : Submonoid M) ↦
          ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid (Additive M)))
        ((fun (S : AddSubmonoid (Additive M)) ↦
            ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
                one_mem' := ⋯ } :
              Submonoid M))
          { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
      { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid (Additive M) }
⊢ (fun (S : Submonoid M) ↦
        ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid (Additive M)))
      ((fun (S : AddSubmonoid (Additive M)) ↦
          ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid M))
        x) =
    x

Tactic:
cases x
-- 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 : Submonoid M
toAddSubsemigroup : AddSubsemigroup (Additive M)
zero_mem' : 0 ∈ toAddSubsemigroup.carrier
⊢ (fun (S : Submonoid M) ↦
        ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid (Additive M)))
      ((fun (S : AddSubmonoid (Additive M)) ↦
          ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid M))
        { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
    { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid (Additive M) }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Set M
⊢ Eq (α := AddSubmonoid (Additive M))
    ((toAddSubmonoid : (a : Submonoid M) → AddSubmonoid (Additive M)) (closure S) : AddSubmonoid (Additive M))
    (AddSubmonoid.closure ((⇑Additive.toMul : (a : Additive M) → M) ⁻¹' S) : AddSubmonoid (Additive M))

Tactic:
le_antisymm
    (Submonoid.toAddSubmonoid.le_symm_apply.1 <|
      Submonoid.closure_le.2 (AddSubmonoid.subset_closure (M := Additive M)))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := M))

Premises used: Iff.mpr, AddSubmonoid.subset_closure, le_antisymm, AddSubmonoid.closure_le, Submonoid.toAddSubmonoid, OrderIso.le_symm_apply, Iff.mp, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
S : Set (Additive M)
⊢ Eq (α := Submonoid M) ((toSubmonoid' : (a : AddSubmonoid (Additive M)) → Submonoid M) (closure S) : Submonoid M)
    (Submonoid.closure ((⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' S) : Submonoid M)

Tactic:
le_antisymm
    (AddSubmonoid.toSubmonoid'.le_symm_apply.1 <|
      AddSubmonoid.closure_le.2 (Submonoid.subset_closure (M := M)))
    (Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := Additive M))

Premises used: Iff.mpr, AddSubmonoid.toSubmonoid', AddSubmonoid.subset_closure, le_antisymm, AddSubmonoid.closure_le, OrderIso.le_symm_apply, Iff.mp, Submonoid.subset_closure, Submonoid.closure_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 : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
x : AddSubmonoid A
mk :
  ∀ (toAddSubsemigroup : AddSubsemigroup A) (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
    (fun (S : Submonoid (Multiplicative A)) ↦
          ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
              add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid A))
        ((fun (S : AddSubmonoid A) ↦
            ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
                one_mem' := ⋯ } :
              Submonoid (Multiplicative A)))
          { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
      { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid A }
⊢ (fun (S : Submonoid (Multiplicative A)) ↦
        ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
            add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid A))
      ((fun (S : AddSubmonoid A) ↦
          ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid (Multiplicative A)))
        x) =
    x

Tactic:
cases x
-- 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 : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
toAddSubsemigroup : AddSubsemigroup A
zero_mem' : 0 ∈ toAddSubsemigroup.carrier
⊢ (fun (S : Submonoid (Multiplicative A)) ↦
        ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
            add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid A))
      ((fun (S : AddSubmonoid A) ↦
          ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid (Multiplicative A)))
        { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
    { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid A }

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 : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
x : Submonoid (Multiplicative A)
mk :
  ∀ (toSubsemigroup : Subsemigroup (Multiplicative A)) (one_mem' : 1 ∈ toSubsemigroup.carrier),
    (fun (S : AddSubmonoid A) ↦
          ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid (Multiplicative A)))
        ((fun (S : Submonoid (Multiplicative A)) ↦
            ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
                add_mem' := ⋯, zero_mem' := ⋯ } :
              AddSubmonoid A))
          { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
      { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid (Multiplicative A) }
⊢ (fun (S : AddSubmonoid A) ↦
        ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid (Multiplicative A)))
      ((fun (S : Submonoid (Multiplicative A)) ↦
          ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
              add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid A))
        x) =
    x

Tactic:
cases x
-- 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 : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
toSubsemigroup : Subsemigroup (Multiplicative A)
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ (fun (S : AddSubmonoid A) ↦
        ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid (Multiplicative A)))
      ((fun (S : Submonoid (Multiplicative A)) ↦
          ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
              add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid A))
        { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
    { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid (Multiplicative A) }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
A : Type u_4
inst : AddZeroClass A
S : Set A
⊢ Eq (α := Submonoid (Multiplicative A))
    ((toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) (closure S) : Submonoid (Multiplicative A))
    (Submonoid.closure ((⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' S) : Submonoid (Multiplicative A))

Tactic:
le_antisymm
    (AddSubmonoid.toSubmonoid.to_galoisConnection.l_le <|
      AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := Multiplicative A))
    (Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := A))

Premises used: Iff.mpr, OrderIso.to_galoisConnection, AddSubmonoid.subset_closure, GaloisConnection.l_le, le_antisymm, AddSubmonoid.toSubmonoid, AddSubmonoid.closure_le, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
A : Type u_4
inst : AddZeroClass A
S : Set (Multiplicative A)
⊢ Eq (α := AddSubmonoid A)
    ((toAddSubmonoid' : (a : Submonoid (Multiplicative A)) → AddSubmonoid A) (closure S) : AddSubmonoid A)
    (AddSubmonoid.closure ((⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' S) : AddSubmonoid A)

Tactic:
le_antisymm
    (Submonoid.toAddSubmonoid'.to_galoisConnection.l_le <|
      Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := A))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := Multiplicative A))

Premises used: Iff.mpr, Submonoid.toAddSubmonoid', OrderIso.to_galoisConnection, AddSubmonoid.subset_closure, GaloisConnection.l_le, le_antisymm, AddSubmonoid.closure_le, Submonoid.subset_closure, Submonoid.closure_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_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S
⊢ Membership.mem (α := N) S ((f : (a : M) → N) (a * b) : N)

Tactic:
rw [map_mul]

Premises used: map_mul
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S

Tactic:
S.mul_mem ha hb

Premises used: Submonoid.mul_mem
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S

Tactic:
exact S.mul_mem ha hb

Premises used: Submonoid.mul_mem
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
rw : 1 ∈ S
⊢ Membership.mem (α := N) S ((f : (a : M) → N) 1 : N)

Tactic:
rw [map_one]

Premises used: map_one
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S

Tactic:
S.one_mem

Premises used: Submonoid.one_mem
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S

Tactic:
exact S.one_mem

Premises used: Submonoid.one_mem
-- 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
S : Submonoid N
f : F
⊢ (↑(comap f S) : Set M) = (⇑f : (a : M) → N) ⁻¹' (↑S : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, 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
S : Submonoid N
f : F
x : M
⊢ Membership.mem (γ := Submonoid M) (comap f S) x ↔ Membership.mem (α := N) S ((f : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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 : Submonoid P
g : N →* P
f : M →* N
⊢ Eq (α := Submonoid M) (comap f (comap g S)) (comap (g.comp f) S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Submonoid.comap, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
P : Type u_3
inst : MulOneClass P
S : Submonoid P
⊢ ∀ (x : P), Membership.mem (γ := Submonoid P) (comap (F := P →* P) (MonoidHom.id P) S) x ↔ x ∈ S

Tactic:
simp
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
rw rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
rw [map_mul]

Premises used: map_mul
-- 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
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
⊢ Membership.mem (γ := Set N) ((⇑f : (a : M) → N) '' (↑S : Set M))
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))

Tactic:
exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩
-- 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 M
⊢ (↑(map f S) : Set N) = (⇑f : (a : M) → N) '' (↑S : Set M)

Tactic:
rfl

Premises used: setOf, Set.image, 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 M
⊢ Eq (α := Submonoid N) (map (F := M →* N) (↑f : M →* N) S) (map f S)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, Submonoid.map, 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_5
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
S : Submonoid M
⊢ Eq (α := Submonoid N) (map (F := M ≃* N) (↑f : M ≃* N) S) (map f S)

Tactic:
rfl

Premises used: Submonoid.map, MulEquivClass.toMulEquiv, 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 M
y : N
⊢ Membership.mem (γ := Submonoid N) (map f S) y ↔ ∃ x ∈ S, (f : (a : M) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- 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 M
x : M
hx : x ∈ S
⊢ Membership.mem (α := N) (γ := Submonoid N) (map f S) ((f : (a : M) → N) x : N)

Tactic:
mem_image_of_mem f hx

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- 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 M
x : ↥S
⊢ Membership.mem (α := N) (γ := Submonoid N) (map f S) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
mem_map_of_mem f x.2

Premises used: Submonoid.mem_map_of_mem, Subtype.property
-- 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 : Submonoid M
g : N →* P
f : M →* N
⊢ Eq (α := Submonoid P) (map g (map f S)) (map (g.comp f) S)

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- 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
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submonoid M
x : M
⊢ Membership.mem (α := N) (γ := Submonoid N) (map f S) ((f : (a : M) → N) x : N) ↔ x ∈ S

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- 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 M
T : Submonoid N
⊢ map f S ≤ T ↔ S ≤ comap f T

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- 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
⊢ GaloisConnection (α := Submonoid M) (β := Submonoid N) (map f) (comap f)

Tactic:
fun _ _ => map_le_iff_le_comap

Premises used: Submonoid.map_le_iff_le_comap, GaloisConnection
-- 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
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
T : Submonoid N
f : F
⊢ S ≤ comap f T → map f S ≤ T

Tactic:
(gc_map_comap f).l_le

Premises used: GaloisConnection.l_le, Submonoid.gc_map_comap
-- 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
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
T : Submonoid N
f : F
⊢ map f S ≤ T → S ≤ comap f T

Tactic:
(gc_map_comap f).le_u

Premises used: GaloisConnection.le_u, Submonoid.gc_map_comap
-- 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
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ S ≤ comap f (map f S)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: GaloisConnection.le_u_l, Submonoid.gc_map_comap
-- 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
S : Submonoid N
f : F
⊢ map f (comap f S) ≤ S

Tactic:
(gc_map_comap f).l_u_le _

Premises used: Submonoid.gc_map_comap, GaloisConnection.l_u_le
-- 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
⊢ Monotone (α := Submonoid M) (β := Submonoid N) (map f)

Tactic:
(gc_map_comap f).monotone_l

Premises used: Submonoid.gc_map_comap, GaloisConnection.monotone_l
-- 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
⊢ Monotone (α := Submonoid N) (β := Submonoid M) (comap f)

Tactic:
(gc_map_comap f).monotone_u

Premises used: GaloisConnection.monotone_u, Submonoid.gc_map_comap