awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
bM : Finset M
hbM : closure (↑bM : Set M) = P
bN : Finset N
hbN : closure (↑bN : Set N) = Q
⊢ closure (SProd.sprod (β := Set N) (↑bM : Set M) {1} ∪ SProd.sprod (α := Set M) {1} (↑bN : Set N)) = P.prod Q

Tactic:
simp [closure_union, hbM, hbN]

Premises used: Submonoid.closure_union
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
obtain : ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P), (P.prod Q).FG (M := M × N)
obtain₁ :
  ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P) (bN : Finset N) (hbN : closure (↑bN : Set N) = Q),
    (P.prod Q).FG (M := M × N)
obtain₂ :
  ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P) (bN : Finset N) (hbN : closure (↑bN : Set N) = Q),
    closure (↑(SProd.sprod (β := Finset N) bM {1} ∪ SProd.sprod (α := Finset M) {1} bN) : Set (M × N)) = P.prod Q
obtain₃ :
  ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P) (bN : Finset N) (hbN : closure (↑bN : Set N) = Q),
    closure (SProd.sprod (β := Set N) (↑bM : Set M) {1} ∪ SProd.sprod (α := Set M) {1} (↑bN : Set N)) = P.prod Q
⊢ (P.prod Q).FG (M := M × N)

Tactic:
classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]

Premises used: Submonoid.closure_union
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
haveI :
  ∀ (this : Fintype ι),
    ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
      pi (M := M) Set.univ P
⊢ ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
    pi (M := M) Set.univ P

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
this : Fintype ι
⊢ ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
    pi (M := M) Set.univ P

Tactic:
iSup_map_mulSingle_le.antisymm fun x hx => ?_

Premises used: Submonoid.iSup_map_mulSingle_le, LE.le.antisymm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
this : Fintype ι
refine :
  ∀ (x : (i : ι) → M i) (hx : x ∈ pi (M := M) Set.univ P),
    Membership.mem (γ := Submonoid ((i : ι) → M i))
      (⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i)) x
⊢ ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
    pi (M := M) Set.univ P

Tactic:
refine iSup_map_mulSingle_le.antisymm fun x hx => ?_

Premises used: Submonoid.iSup_map_mulSingle_le, LE.le.antisymm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi (M := M) Set.univ P
rw :
  Membership.mem (γ := Submonoid ((i : ι) → M i))
    (⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i))
    (Finset.noncommProd Finset.univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯)
⊢ Membership.mem (γ := Submonoid ((i : ι) → M i))
    (⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i)) x

Tactic:
rw [← Finset.noncommProd_mulSingle x]

Premises used: Finset.noncommProd_mulSingle
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi (M := M) Set.univ P
⊢ Membership.mem (γ := Submonoid ((i : ι) → M i))
    (⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i))
    (Finset.noncommProd Finset.univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯)

Tactic:
noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

Premises used: trivial, Set.Mem, MonoidHom.mulSingle, Submonoid.noncommProd_mem, Submonoid.mem_iSup_of_mem, Submonoid.mem_map_of_mem
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi (M := M) Set.univ P
⊢ Membership.mem (γ := Submonoid ((i : ι) → M i))
    (⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i))
    (Finset.noncommProd Finset.univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯)

Tactic:
exact noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

Premises used: Submonoid.noncommProd_mem, Submonoid.mem_iSup_of_mem, Submonoid.mem_map_of_mem
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
haveI : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
this : Fintype ι
choose :
  ∀ (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
    (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)

Tactic:
choose s hs using hP
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i
⊢ (pi (M := M) Set.univ P).FG (M := (i : ι) → M i)

Tactic:
⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩

Premises used: Finset.univ, MonoidHom.mulSingle, Finset.biUnion, Exists.intro, Submonoid.FG, DFunLike.coe, Finset.image
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i
refine :
  closure
      (↑(Finset.biUnion Finset.univ fun (i : ι) ↦
            Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
        Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)

Tactic:
refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i
simp_rw :
  closure
      (⋃ x ∈ (↑Finset.univ : Set ι),
        (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
          Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₁ :
  closure
      (⋃ (x : ι),
        ⋃ (_ : Membership.mem (γ := Set ι) Set.univ x),
          (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
            Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₂ :
  closure
      (⋃ (x : ι),
        (↑(Finset.image (⇑(MonoidHom.mulSingle M x : M x →* (i : ι) → M i) : (a : M x) → (i : ι) → M i) (s x)) :
          Set ((i : ι) → M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₃ :
  ⨆ (i : ι),
      closure
        (↑(Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
          Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₄ :
  ⨆ (i : ι),
      closure
        ((⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) '' (↑(s i) : Set (M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₅ :
  ⨆ (i : ι),
      map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (closure (↑(s i) : Set (M i))) =
    Submonoid.pi (M := M) Set.univ P
simp_rw₆ :
  ⨆ (i : ι), map (F := M i →* (i : ι) → M i) (MonoidHom.mulSingle M i : M i →* (i : ι) → M i) (P i) =
    Submonoid.pi (M := M) Set.univ P
⊢ closure
      (↑(Finset.biUnion Finset.univ fun (i : ι) ↦
            Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
        Set ((i : ι) → M i)) =
    Submonoid.pi (M := M) Set.univ P

Tactic:
simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]

Premises used: Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, Finset.coe_image, Submonoid.iSup_map_mulSingle, MonoidHom.map_mclosure, Submonoid.closure_iUnion
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
haveI₃ :
  ∀ (this : Fintype ι) (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
    (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
haveI₄ :
  ∀ (this : Fintype ι) (s : (i : ι) → Finset (M i)) (hs : ∀ (i : ι), closure (↑(s i) : Set (M i)) = P i),
    closure
        (↑(Finset.biUnion Finset.univ fun (i : ι) ↦
              Finset.image (⇑(MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (s i)) :
          Set ((i : ι) → M i)) =
      Submonoid.pi (M := M) Set.univ P
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)

Tactic:
classical
  haveI := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]

Premises used: Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, Finset.coe_image, Submonoid.iSup_map_mulSingle, MonoidHom.map_mclosure, Submonoid.closure_iUnion
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M ↔ Submonoid.FG.{u_1} (M := M) ⊤

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Monoid.FG.mk, Monoid.FG.fg_top, Iff.intro
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M ↔ ∃ (S : Set M), Eq (α := Submonoid M) (Submonoid.closure S) ⊤ ∧ S.Finite

Tactic:
⟨fun _ => (Submonoid.fg_iff ⊤).1 FG.fg_top, fun h => ⟨(Submonoid.fg_iff ⊤).2 h⟩⟩

Premises used: Iff.mpr, Monoid.FG.mk, Monoid.FG.fg_top, Submonoid.fg_iff, Iff.intro, Iff.mp, Top.top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Monoid.FG M
⊢ ∃ (S : Finset M), Minimal (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) S

Tactic:
Monoid.FG.fg_top.exists_minimal_closure_eq

Premises used: Monoid.FG.fg_top, Submonoid.FG.exists_minimal_closure_eq
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid.FG M
⊢ FG.{u_1} (Additive M)

Tactic:
Monoid.fg_iff_add_fg.1 ‹_›

Premises used: Monoid.fg_iff_add_fg, Iff.mp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M_1 : Type u_1
N : Type u_2
inst : Monoid M_1
M : Type u_3
inst_1 : AddMonoid M
inst_2 : AddMonoid.FG M
⊢ FG.{u_3} (Multiplicative M)

Tactic:
AddMonoid.fg_iff_mul_fg.1 ‹_›

Premises used: Iff.mp, AddMonoid.fg_iff_mul_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
intro : ∀ (val : Fintype M), FG M
⊢ FG M

Tactic:
cases nonempty_fintype M

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
val : Fintype M
rw : Eq.{u_1 + 1} (α := Submonoid M) (Submonoid.closure Set.univ) ⊤
⊢ Eq (α := Submonoid M) (Submonoid.closure (↑Finset.univ : Set M)) ⊤

Tactic:
rw [Finset.coe_univ]

Premises used: Finset.coe_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
val : Fintype M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (Submonoid.closure Set.univ) ⊤

Tactic:
Submonoid.closure_univ

Premises used: Submonoid.closure_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
val : Fintype M
⊢ Eq.{u_1 + 1} (α := Submonoid M) (Submonoid.closure Set.univ) ⊤

Tactic:
exact Submonoid.closure_univ

Premises used: Submonoid.closure_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
val : Fintype M
⊢ FG M

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
obtain : ∀ (s : Finset M), FG (Submonoid.map e (closure (↑s : Set M)))
⊢ FG (Submonoid.map e P)

Tactic:
obtain ⟨s, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
e : M →* M'
s : Finset M
rw : Eq (α := Submonoid M') (closure ((⇑e : (a : M) → M') '' (↑s : Set M))) (Submonoid.map e (closure (↑s : Set M)))
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := Submonoid M') (closure ((⇑e : (a : M) → M') '' (↑s : Set M)))
    (closure ((⇑e : (a : M) → M') '' (↑s : Set M)))
⊢ Eq (α := Submonoid M') (closure (↑(Finset.image (⇑e : (a : M) → M') s) : Set M'))
    (Submonoid.map e (closure (↑s : Set M)))

Tactic:
rw [Finset.coe_image, MonoidHom.map_mclosure]

Premises used: Finset.coe_image, MonoidHom.map_mclosure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
e : M →* M'
s : Finset M
⊢ FG (Submonoid.map e (closure (↑s : Set M)))

Tactic:
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
obtain : ∀ (s : Finset M), FG (Submonoid.map e (closure (↑s : Set M)))
⊢ FG (Submonoid.map e P)

Tactic:
classical
    obtain ⟨s, rfl⟩ := h
    exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
h : FG (Submonoid.map e P)
obtain : ∀ (s : Finset M') (hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)), P.FG
⊢ P.FG

Tactic:
obtain ⟨s, hs⟩ := h
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
h : closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M) = P
⊢ P.FG

Tactic:
use s.preimage e he.injOn

Premises used: Function.Injective.injOn, Finset.preimage, DFunLike.coe
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
h : Eq (α := Submonoid M') (Submonoid.map e (closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M))) (Submonoid.map e P)
⊢ closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M) = P

Tactic:
apply Submonoid.map_injective_of_injective he

Premises used: Submonoid.map_injective_of_injective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
h :
  Eq (α := Submonoid M')
    (closure (Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M'))))
    (closure (↑s : Set M'))
⊢ Eq (α := Submonoid M') (Submonoid.map e (closure (↑(s.preimage (⇑e : (a : M) → M') ⋯) : Set M))) (Submonoid.map e P)

Tactic:
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]

Premises used: Finset.coe_preimage, MonoidHom.map_mclosure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
h : Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M')) = (↑s : Set M')
⊢ Eq (α := Submonoid M')
    (closure (Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M'))))
    (closure (↑s : Set M'))

Tactic:
congr
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
h : LE.le (α := Submonoid M') (Submonoid.map e P) (Submonoid.map e ⊤)
⊢ Set.image.{u_1, u_3} (α := M) (⇑e : (a : M) → M') ((⇑e : (a : M) → M') ⁻¹' (↑s : Set M')) = (↑s : Set M')

Tactic:
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]

Premises used: MonoidHom.coe_mrange, MonoidHom.mrange_eq_map, Set.image_preimage_eq_iff, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ LE.le (α := Submonoid M') (Submonoid.map e P) (Submonoid.map e ⊤)

Tactic:
Submonoid.monotone_map le_top

Premises used: le_top, Submonoid.monotone_map
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑e : (a : M) → M')
s : Finset M'
hs : Eq (α := Submonoid M') (closure (↑s : Set M')) (Submonoid.map e P)
⊢ LE.le (α := Submonoid M') (Submonoid.map e P) (Submonoid.map e ⊤)

Tactic:
exact Submonoid.monotone_map le_top

Premises used: le_top, Submonoid.monotone_map
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
rw : Submonoid.FG (Submonoid.map N.subtype ⊤)
| N.FG

Tactic:
rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]

Premises used: MonoidHom.mrange_eq_map, Submonoid.mrange_subtype
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
conv_rhs : FG.{u_1} ↥N ↔ Submonoid.FG (Submonoid.map N.subtype ⊤)
⊢ FG.{u_1} ↥N ↔ N.FG

Tactic:
conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]

Premises used: MonoidHom.mrange_eq_map, Submonoid.mrange_subtype
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
⊢ FG.{u_1} ↥N ↔ Submonoid.FG (Submonoid.map N.subtype ⊤)

Tactic:
⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

Premises used: Monoid.FG.mk, Monoid.FG.fg_top, Subtype.coe_injective, Iff.intro, Submonoid.FG.map, Submonoid.subtype, Submonoid.FG.map_injective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
N : Submonoid M
⊢ FG.{u_1} ↥N ↔ Submonoid.FG (Submonoid.map N.subtype ⊤)

Tactic:
exact ⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
obtain : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤), FG M'
⊢ FG M'

Tactic:
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›

Premises used: Iff.mp, Monoid.fg_def
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
h : Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
⊢ FG M'

Tactic:
use s.image f

Premises used: DFunLike.coe, Finset.image
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
s : Finset M
hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤
h : Eq.{u_3 + 1} (α := Submonoid M') (Submonoid.closure ((⇑f : (a : M) → M') '' (↑s : Set M))) ⊤
h₁ : Eq (α := Submonoid M') (Submonoid.map f (Submonoid.closure (↑s : Set M))) ⊤
h₂ : Eq (α := Submonoid M') (Submonoid.map f ⊤) ⊤
h₃ : Eq (α := Submonoid M') (MonoidHom.mrange f) ⊤
h₄ h₅ h₆ h₇ : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤

Tactic:
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

Premises used: MonoidHom.mrange_eq_map, MonoidHom.mrange_eq_top, Finset.coe_image, MonoidHom.map_mclosure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
obtain : ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤), FG M'
h :
  ∀ (s : Finset M) (hs : Eq (α := Submonoid M) (Submonoid.closure (↑s : Set M)) ⊤),
    Eq (α := Submonoid M') (Submonoid.closure (↑(Finset.image (⇑f : (a : M) → M') s) : Set M')) ⊤
⊢ FG M'

Tactic:
classical
    obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

Premises used: MonoidHom.mrange_eq_map, MonoidHom.mrange_eq_top, Finset.coe_image, Iff.mp, MonoidHom.map_mclosure, Monoid.fg_def
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
M' : Type u_3
inst_1 : Monoid M'
inst_2 : FG M
f : M →* M'
⊢ FG.{u_3} ↥(MonoidHom.mrange f)

Tactic:
Monoid.fg_of_surjective f.mrangeRestrict f.mrangeRestrict_surjective

Premises used: MonoidHom.mrangeRestrict_surjective, MonoidHom.mrangeRestrict, Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
α : Type u_3
inst_1 : Finite α
⊢ Monoid.FG.{u_3} (FreeMonoid α)

Tactic:
Monoid.fg_iff.mpr ⟨Set.range of, closure_range_of, Set.finite_range of⟩

Premises used: Iff.mpr, FreeMonoid.closure_range_of, Set.finite_range, Monoid.fg_iff, FreeMonoid.of, And.intro, Exists.intro, Set.range