awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteIndexNormalSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A B : FiniteIndexNormalSubgroup G
h : A.toSubgroup = B.toSubgroup
x : G
⊢ x ∈ A.carrier ↔ x ∈ B.carrier
have carrier : x ∈ B.carrier ↔ x ∈ B.carrier
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteIndexNormalSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
N : Type u_3
inst_1 : Group H
inst_2 : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : MonoidHom.{u_1, u_2} G (H ⧸ K.toSubgroup) := MonoidHom.comp (QuotientGroup.mk' K.toSubgroup) f
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex
have hker : Subgroup.comap f K.toSubgroup = g.ker
Tactic: have hker : K.toSubgroup.comap f = g.ker := by
      simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
hN : N.IsNormalClosureFG
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ (map f N).IsNormalClosureFG
have obtain : ∀ (S : Set G) (hSfinite : S.Finite) (hSclosure : normalClosure S = N), (map f N).IsNormalClosureFG
Tactic: obtain ⟨S, hSfinite, hSclosure⟩ := hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ (map f N).IsNormalClosureFG
have refine : normalClosure ((⇑f : (a : G) → H) '' S) = map f N
Tactic: refine ⟨f '' S, hSfinite.image _, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ normalClosure ((⇑f : (a : G) → H) '' S) = map f N
have rw : normalClosure ((⇑f : (a : G) → H) '' S) = map f (normalClosure S)
Tactic: rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
rw : normalClosure ((⇑f : (a : G) → H) '' S) = map f (normalClosure S)
⊢ normalClosure ((⇑f : (a : G) → H) '' S) = map f N
have rw₁ : Eq.{u_2 + 1} (α := Subgroup H) (normalClosure ((⇑f : (a : G) → H) '' S)) (normalClosure ((⇑f : (a : G) → H) '' S))
Tactic: rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
h : IsFinitelyPresented G
⊢ IsFinitelyPresented H
have obtain : ∀ (n : ℕ) (φ : FreeGroup (Fin n) →* G)
  (hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G))
  (hNC : φ.ker.IsNormalClosureFG), IsFinitelyPresented H
Tactic: obtain ⟨n, φ, hφsurj, hNC⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective (α := FreeGroup (Fin n)) (β := G) (⇑φ : (a : FreeGroup (Fin n)) → G)
hNC : φ.ker.IsNormalClosureFG
⊢ IsFinitelyPresented H
have refine : (MonoidHom.ker (MonoidHom.comp (↑iso : G →* H) φ)).IsNormalClosureFG
Tactic: refine ⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
⊢ IsFinitelyPresented.{u_3} (FreeGroup α)
have have : ∀ (n : ℕ) (toFun : α → Fin n) (f : Fin n → α) (hf_surj : Function.LeftInverse f toFun)
  (hf_inj : Function.RightInverse f toFun), IsFinitelyPresented.{u_3} (FreeGroup α)
Tactic: have ⟨n, _, f, hf_surj, hf_inj⟩ := Finite.exists_equiv_fin α
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
⊢ IsFinitelyPresented.{u_3} (FreeGroup α)
have refine : (FreeGroup.map f).ker.IsNormalClosureFG
Tactic: refine ⟨n, FreeGroup.map f, FreeGroup.map_surjective hf_surj.surjective, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FinitelyPresentedGroup (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Finite α
n : ℕ
toFun : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun
hf_inj : Function.RightInverse f toFun
⊢ (FreeGroup.map f).ker.IsNormalClosureFG
have rw : Subgroup.IsNormalClosureFG (G := FreeGroup (Fin n)) ⊥
Tactic: rw [(FreeGroup.map f).ker_eq_bot_iff.mpr (FreeGroup.map_injective hf_inj.injective)]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG
have rcases : ∀ (s : Finset M), (closure (↑s : Set M) ⊔ Q).FG
Tactic: rcases hP with ⟨s, rfl⟩
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
Q : Submonoid M
hQ : Q.FG
s : Finset M
⊢ (closure (↑s : Set M) ⊔ Q).FG
have rcases : ∀ (t : Finset M), FG (closure (↑s : Set M) ⊔ closure (↑t : Set M))
Tactic: rcases hQ with ⟨t, rfl⟩
Cleared hypotheses: Q, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG
have rcases : ∀ (s : Finset M), (closure (↑s : Set M) ⊔ Q).FG
Tactic: classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
inst : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
rcases : ∀ (s : Finset M), (closure (↑s : Set M) ⊔ Q).FG
⊢ (P ⊔ Q).FG
have rcases₁ : ∀ (s t : Finset M), FG (closure (↑s : Set M) ⊔ closure (↑t : Set M))
Tactic: classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩
Cleared hypotheses: P, Q, hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (P.prod Q).FG (M := M × N)
have obtain : ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P), (P.prod Q).FG (M := M × N)
Tactic: obtain ⟨bM, hbM⟩ := hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
P : Submonoid M
Q : Submonoid N
hQ : Q.FG
bM : Finset M
hbM : closure (↑bM : Set M) = P
⊢ (P.prod Q).FG (M := M × N)
have obtain : ∀ (bN : Finset N) (hbN : closure (↑bN : Set N) = Q), (P.prod Q).FG (M := M × N)
Tactic: obtain ⟨bN, hbN⟩ := hQ
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (P.prod Q).FG (M := M × N)
have refine : closure (↑(SProd.sprod (β := Finset N) bM {1} ∪ SProd.sprod (α := Finset M) {1} bN) : Set (M × N)) = P.prod Q
Tactic: refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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 (β := Finset N) bM {1} ∪ SProd.sprod (α := Finset M) {1} bN) : Set (M × N)) = P.prod Q
have push_cast : closure (SProd.sprod (β := Set N) (↑bM : Set M) {1} ∪ SProd.sprod (α := Set M) {1} (↑bN : Set N)) = P.prod Q
Tactic: push_cast
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (P.prod Q).FG (M := M × N)
have obtain : ∀ (bM : Finset M) (hbM : closure (↑bM : Set M) = P), (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]
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)
⊢ (P.prod Q).FG (M := M × N)
have 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)
Tactic: classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)
⊢ (P.prod Q).FG (M := M × N)
have 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
Tactic: classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (P.prod Q).FG (M := M × N)
have 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
Tactic: classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
ι : Type u_3
inst : Finite ι
M : ι → Type u_4
inst_1 : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst_2 : DecidableEq ι
⊢ ⨆ (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
have 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
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have 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
Tactic: refine iSup_map_mulSingle_le.antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)) x
have 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)) sorry)
Tactic: rw [← Finset.noncommProd_mulSingle x]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have haveI : ∀ (this : Fintype ι), (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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 ι
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have 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)
Tactic: choose s hs using hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ (Submonoid.pi (M := M) Set.univ P).FG (M := (i : ι) → M i)
have 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
Tactic: refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]