awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M × N →* M) (fst M N) u ≤ s
hK : map (F := M × N →* N) (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ s.prod t

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
mp : s.prod t ≤ u → map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
mpr : map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u → s.prod t ≤ u
⊢ s.prod t ≤ u ↔ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
mp : map (F := M →* M × N) (inl M N) s ≤ u
mp₁ : map (F := N →* M × N) (inr M N) t ≤ u
⊢ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : M
hx : x ∈ (↑s : Set M)
mp : Membership.mem (α := M × N) (s.prod t) ((inl M N : (a : M) → M × N) x : M × N)
⊢ Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x : M × N)

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : M
hx : x ∈ (↑s : Set M)
⊢ Membership.mem (α := M × N) (s.prod t) ((inl M N : (a : M) → M × N) x : M × N)

Tactic:
⟨hx, Submonoid.one_mem _⟩

Premises used: Set.Mem, setOf, Set.prod, Submonoid.one_mem, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : M
hx : x ∈ (↑s : Set M)
⊢ Membership.mem (α := M × N) (s.prod t) ((inl M N : (a : M) → M × N) x : M × N)

Tactic:
exact ⟨hx, Submonoid.one_mem _⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : N
hx : x ∈ (↑t : Set N)
mp : Membership.mem (α := M × N) (s.prod t) ((inr M N : (a : N) → M × N) x : M × N)
⊢ Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x : M × N)

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : N
hx : x ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) (s.prod t) ((inr M N : (a : N) → M × N) x : M × N)

Tactic:
⟨Submonoid.one_mem _, hx⟩

Premises used: Set.Mem, setOf, Set.prod, Submonoid.one_mem, And.intro
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : N
hx : x ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) (s.prod t) ((inr M N : (a : N) → M × N) x : M × N)

Tactic:
exact ⟨Submonoid.one_mem _, hx⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
a :
  Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := M →* M × N) (inl M N) s)
    ((inl M N : (a : M) → M × N) x1 : M × N)
⊢ Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)

Tactic:
apply hH
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := M →* M × N) (inl M N) s)
    ((inl M N : (a : M) → M × N) x1 : M × N)

Tactic:
simpa using h1
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)

Tactic:
have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
a :
  Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := N →* M × N) (inr M N) t)
    ((inr M N : (a : N) → M × N) x2 : M × N)
⊢ Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x2 : M × N)

Tactic:
apply hK
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
⊢ Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := N →* M × N) (inr M N) t)
    ((inr M N : (a : N) → M × N) x2 : M × N)

Tactic:
simpa using h2
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
⊢ Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x2 : M × N)

Tactic:
have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
h2' : Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x2 : M × N)
⊢ (x1, x2) ∈ u

Tactic:
simpa using Submonoid.mul_mem _ h1' h2'

Premises used: Submonoid.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Set M
t : Set N
hs : 1 ∈ s
ht : 1 ∈ t
⊢ Eq (α := Submonoid (M × N)) (closure (s ×ˢ t)) (prod (closure s) (closure t))

Tactic:
le_antisymm
    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
    (prod_le_iff.2 ⟨
      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)

Premises used: Iff.mpr, Set.prod_subset_prod_iff, Submonoid.map_le_of_le_comap, le_antisymm, And.intro, Or.inl, Submonoid.prod_le_iff, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Set M
⊢ LE.le (α := Submonoid (M × N)) (map (F := N →* M × N) (inr M N) ⊥) (closure (SProd.sprod (β := Set N) s {1}))

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
t : Set N
⊢ LE.le (α := Submonoid (M × N)) (map (F := M →* M × N) (inl M N) ⊥) (closure (SProd.sprod (α := Set M) {1} t))

Tactic:
simp
-- 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
⊢ (↑(mrange f) : Set N) = Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: setOf, Set.range, 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
y : N
⊢ Membership.mem (γ := Submonoid N) (mrange f) y ↔ ∃ (x : M), (f : (a : M) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
O : Type u_5
inst_2 : MulOneClass O
f : N →* O
g : M →* N
⊢ Eq (α := Submonoid O) (mrange (f.comp g)) (map f (mrange g))

Tactic:
SetLike.coe_injective <| Set.range_comp f _

Premises used: Set.range_comp, SetLike.coe_injective, 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
⊢ Eq (α := Submonoid N) (mrange f) (map f ⊤)

Tactic:
Submonoid.copy_eq _

Premises used: Submonoid.copy_eq, MonoidHom.mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq (α := Submonoid M) (mrange (F := M →* M) (id M)) ⊤

Tactic:
simp [mrange_eq_map]

Premises used: MonoidHom.mrange_eq_map
-- 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
g : N →* P
f : M →* N
⊢ Eq (α := Submonoid P) (map g (mrange f)) (mrange (g.comp f))

Tactic:
simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

Premises used: MonoidHom.mrange_eq_map, Submonoid.map_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
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
rw :
  Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
⊢ (↑(mrange f) : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ

Tactic:
rw [coe_mrange, coe_top]

Premises used: MonoidHom.coe_mrange, Submonoid.coe_top
-- 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 : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Eq (α := Submonoid N) (mrange f) ⊤

Tactic:
mrange_eq_top.2 hf

Premises used: Iff.mpr, MonoidHom.mrange_eq_top
-- 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 : Set N
⊢ LE.le (α := Submonoid M) (closure ((⇑f : (a : M) → N) ⁻¹' s)) (comap f (closure s))

Tactic:
closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, Submonoid.mem_comap, SetLike.mem_coe, Submonoid.subset_closure, Submonoid.closure_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
s : Set M
⊢ Eq (α := Submonoid N) (map f (closure s)) (closure ((⇑f : (a : M) → N) '' s))

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Submonoid.gi N).gc (Submonoid.gi M).gc
    fun _ ↦ rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Set.image_preimage, Submonoid.gc_map_comap, Submonoid.gi, rfl, GaloisInsertion.gc
-- 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
rw : Eq (α := Submonoid N) (closure (Set.image.{u_1, u_2} (α := M) (⇑f : (a : M) → N) Set.univ)) (mrange f)
rw₁ : Eq (α := Submonoid N) (map f (closure Set.univ)) (mrange f)
rw₂ : Eq (α := Submonoid N) (map f (closure Set.univ)) (map f ⊤)
rw₃ rw₄ : Eq (α := Submonoid N) (map f ⊤) (map f ⊤)
⊢ Eq (α := Submonoid N) (closure (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N))) (mrange f)

Tactic:
rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]

Premises used: Set.image_univ, MonoidHom.mrange_eq_map, Submonoid.closure_univ, MonoidHom.map_mclosure
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
N : Type u_5
S : Type u_6
inst_1 : MulOneClass N
inst_2 : SetLike S M
inst_3 : SubmonoidClass S M
f : M →* N
s : S
x : ↥s
⊢ Eq.{u_5 + 1} (α := N) ((f.restrict s : (a : ↥s) → N) x : N) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
N : Type u_5
S : Type u_6
inst_1 : MulOneClass N
f : M →* N
inst_2 : SetLike S M
inst_3 : SubmonoidClass S M
s : S
⊢ Eq (α := MonoidHom.{u_1, u_5} (↥s) N) (f.restrict s) 1 ↔
    ∀ x ∈ s, Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N)

Tactic:
simp [MonoidHom.ext_iff]

Premises used: MonoidHom.ext_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
f : M →* N
⊢ Eq (α := Submonoid N) (mrange (F := MonoidHom.{u_1, u_2} (↥S) N) (f.restrict S)) (map f S)

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- 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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
h : ∀ (x : ↥M'), Eq.{u_6 + 1} (α := A) ((restrict 1 M' : (a : ↥M') → A) x : A) ((1 : (a : ↥M') → A) x : A)
⊢ Eq (α := MonoidHom.{u_1, u_6} (↥M') A) (restrict 1 M') 1

Tactic:
ext
-- 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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
x : ↥M'
⊢ Eq.{u_6 + 1} (α := A) ((restrict 1 M' : (a : ↥M') → A) x : A) ((1 : (a : ↥M') → A) x : A)

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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
x x_1 : M →* A
h :
  ∀ (x_2 : ↥M'),
    Eq.{u_6 + 1} (α := A) (((x * x_1).restrict M' : (a : ↥M') → A) x_2 : A)
      ((HMul.hMul (α := MonoidHom.{u_1, u_6} (↥M') A) (x.restrict M') (x_1.restrict M') : (a : ↥M') → A) x_2 : A)
⊢ (x * x_1).restrict M' = HMul.hMul (α := MonoidHom.{u_1, u_6} (↥M') A) (x.restrict M') (x_1.restrict M')

Tactic:
ext
-- 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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
x x_1 : M →* A
x_2 : ↥M'
⊢ Eq.{u_6 + 1} (α := A) (((x * x_1).restrict M' : (a : ↥M') → A) x_2 : A)
    ((HMul.hMul (α := MonoidHom.{u_1, u_6} (↥M') A) (x.restrict M') (x_1.restrict M') : (a : ↥M') → A) x_2 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
S : Type u_5
inst_2 : SetLike S N
inst_3 : SubmonoidClass S N
f : M →* N
s : S
h : ∀ (x : M), Membership.mem.{u_2, u_5} (α := N) s ((f : (a : M) → N) x : N)
⊢ Injective.{u_1 + 1, u_2 + 1} (α := M) (β := ↥s) (⇑(f.codRestrict s h) : (a : M) → ↥s) ↔
    Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
⟨fun H _ _ hxy ↦ H <| Subtype.ext hxy, fun H _ _ hxy ↦ H (congr_arg Subtype.val hxy)⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
inst : MulOneClass M
N : Type u_5
inst_1 : MulOneClass N
f : M →* N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((↑((f.mrangeRestrict : (a : M) → ↥(mrange f)) x) : N) : N) ((f : (a : M) → N) x : 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
f : M →* N
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := ↥(mrange f)) (⇑f.mrangeRestrict : (a : M) → ↥(mrange f))

Tactic:
fun ⟨_, ⟨x, rfl⟩⟩ => ⟨x, rfl⟩

Premises used: Exists, Exists.intro, MonoidHom.mrangeRestrict, Eq, DFunLike.coe, Function.Surjective, _private.0.MonoidHom.mrangeRestrict_surjective.match_1, 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
x : M
⊢ Membership.mem (γ := Submonoid M) (mker f) x ↔ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- 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
⊢ (↑(mker f) : Set M) = Set.preimage (β := N) (⇑f : (a : M) → N) {1}

Tactic:
rfl

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

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, Submonoid.comap, Set.preimage, Set.singleton, 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
⊢ Eq (α := Submonoid M) (comap f ⊥) (mker f)

Tactic:
rfl

Premises used: MonoidHom.mker, 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
f : M →* N
⊢ Eq (α := Submonoid ↥S) (mker (F := MonoidHom.{u_1, u_2} (↥S) N) (f.restrict S)) (comap S.subtype (mker f))

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, Submonoid.comap, Set.preimage, Set.singleton, Submonoid.subtype, 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
h :
  ∀ (x : M), Membership.mem (γ := Submonoid M) (mker f.mrangeRestrict) x ↔ Membership.mem (γ := Submonoid M) (mker f) x
⊢ Eq (α := Submonoid M) (mker f.mrangeRestrict) (mker f)

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
f : M →* N
x : M
h :
  Eq.{u_2 + 1} (α := ↥(mrange f))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) ((f : (a : M) → N) x) ⋯ :
        ↥(mrange f))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) 1 ⋯ : ↥(mrange f)) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N)
⊢ Membership.mem (γ := Submonoid M) (mker f.mrangeRestrict) x ↔ Membership.mem (γ := Submonoid M) (mker f) x

Tactic:
change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1

Premises used: Subtype.mk, 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 : M →* N
x : M
⊢ Eq.{u_2 + 1} (α := ↥(mrange f))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) ((f : (a : M) → N) x) ⋯ :
        ↥(mrange f))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) 1 ⋯ : ↥(mrange f)) ↔
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
h : ∀ (x : M), Membership.mem (γ := Submonoid M) (mker (F := M →* N) 1) x ↔ Membership.mem (γ := Submonoid M) ⊤ x
⊢ Eq (α := Submonoid M) (mker (F := M →* N) 1) ⊤

Tactic:
ext
-- 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 →* N) 1) 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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
S : Submonoid N
S' : Submonoid N'
⊢ Eq (α := Submonoid (M × M')) (comap (f.prodMap g) (S.prod S')) (prod (comap f S) (comap g S'))

Tactic:
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Premises used: SetLike.coe_injective, Set.preimage_prod_map_prod, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Submonoid.Operations
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
rw₁ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (mker g))
rw₂ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (comap g ⊥))
rw₃ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (comap (f.prodMap g) (prod ⊥ ⊥))
rw₄ rw₅ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (comap (f.prodMap g) ⊥)
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))

Tactic:
rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]

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

Tactic:
ext x