awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
refine_1 : x ∈ s
⊢ x = y
have refine_2 : y ∈ s
Tactic: refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Defs (goal)
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
refine_1 : x ∈ s
refine_2 : y ∈ s
⊢ x = y
have refine_3 : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
Tactic: refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : Nat.card.{u_1} ↥H = Nat.card G
⊢ H = ⊤
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero (h ▸ Nat.card_pos.ne')
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
have pos : ∀ (H : j = i),
  Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
Tactic: by_cases H : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
pos :
  ∀ (H : j = i),
    Membership.mem (α := f j) (s j)
      (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
have neg : ∀ (H : ¬j = i),
  Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
Tactic: by_cases H : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
have pos : ∀ (_x : f j) (hx : _x ∈ s j),
  Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f j : f j →* (i : η) → f i) : (a : f j) → (i : η) → f i) _x j : f j)
Tactic: subst H
Cleared hypotheses: i, _x, hx, H
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
⊢ Membership.mem (γ := Subgroup G) (normalizer S) x
have haveI : ∀ (this : (a : Prop) → Decidable a), Membership.mem (γ := Subgroup G) (normalizer S) x
Tactic: haveI := Classical.propDecidable
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ Membership.mem (γ := Subgroup G) (normalizer S) x
have intro : ∀ (val : Fintype (↑S : Type u_1)), Membership.mem (γ := Subgroup G) (normalizer S) x
Tactic: cases nonempty_fintype S
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finite (goal)
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val : Fintype (↑S : Type u_1)
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card.{u_1} (↑S : Type u_1) ≤ Fintype.card.{u_1} (↑((fun (n : G) ↦ x * n * x⁻¹) '' S) : Type u_1)
have rw : Fintype.card.{u_1} (↑S : Type u_1) ≤ Fintype.card.{u_1} (↑S : Type u_1)
Tactic: rw [Set.card_image_of_injective S conj_injective]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x_1 x : M
h : x ∈ Set.range f
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mem : ∀ (i : ι), ∃ (a : ι →₀ ℤ), f i = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: obtain ⟨i, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
have h : Eq.{u_1 + 1} (α := M) 1 (Finsupp.prod 0 fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x_1 x y : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) y
hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
hy' : ∃ (a : ι →₀ ℤ), y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mul : ∀ (v : ι →₀ ℤ)
  (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2))
  (hx' :
    ∃ (a : ι →₀ ℤ),
      Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2))
  (w : ι →₀ ℤ)
  (hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2))
  (hy' :
    ∃ (a : ι →₀ ℤ),
      Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)),
  ∃ (a : ι →₀ ℤ),
    HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) =
      a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
Cleared hypotheses: x, y, hx, hy, hx', hy'
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
w : ι →₀ ℤ
hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ ∃ (a : ι →₀ ℤ),
    HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) =
      a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have h : HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) =
  (v + w).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: use v + w
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
w : ι →₀ ℤ
hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) =
    (v + w).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have h : ∀ a ∈ v.support ∪ w.support, HPow.hPow (β := ℤ) (f a) 0 = 1
Tactic: rw [Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hx' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
w : ι →₀ ℤ
hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
hy' :
  ∃ (a : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
h : ∀ a ∈ v.support ∪ w.support, HPow.hPow (β := ℤ) (f a) 0 = 1
⊢ HMul.hMul (α := M) (v.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (w.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) =
    (v + w).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have h₁ : ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂
Tactic: rw [Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x_1 x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x⁻¹ = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have inv : ∀ (a : ι →₀ ℤ)
  (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)),
  ∃ (a_1 : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ (a_1.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
Tactic: obtain ⟨a, rfl⟩ := hx'
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ ∃ (a_1 : ι →₀ ℤ),
    Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ (a_1.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
have h : Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ ((-a).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
Tactic: use -a
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ ((-a).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
have h : Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ (a.prod fun (a : ι) (b : ℤ) ↦ f a ^ (-b))
Tactic: rw [Finsupp.prod_neg_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
h : Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ (a.prod fun (a : ι) (b : ℤ) ↦ f a ^ (-b))
⊢ Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ ((-a).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
have h₁ : ∀ (a : ι), HPow.hPow (β := ℤ) (f a) 0 = 1
Tactic: rw [Finsupp.prod_neg_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
Tactic: induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mul : ∀ (x y : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
  (hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) y)
  (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
  (hy' : ∃ (a : ι →₀ ℤ), y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
  ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
    (hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) y)
    (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
    (hy' : ∃ (a : ι →₀ ℤ), y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
    ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have inv : ∀ (x : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
  (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
  ∃ (a : ι →₀ ℤ), x⁻¹ = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
Tactic: classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have mul : ∀ (x y : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
  (hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) y)
  (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
  (hy' : ∃ (a : ι →₀ ℤ), y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
  ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
mem : ∀ (x : M) (h : x ∈ Set.range f), ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
one : ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
    (hy : Membership.mem (γ := Subgroup M) (closure (Set.range f)) y)
    (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
    (hy' : ∃ (a : ι →₀ ℤ), y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
    ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have inv : ∀ (x : M) (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x)
  (hx' : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2),
  ∃ (a : ι →₀ ℤ), x⁻¹ = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
Tactic: classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
⊢ ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i
have obtain : ∀ (a : ι →₀ ℤ)
  (hx : Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)),
  ∃ (a_1 : ι → ℤ), Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) (∏ i : ι, f i ^ a_1 i)
Tactic: obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) x ↔
    ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
have refine : (∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) →
  Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
Tactic: refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) x ↔ ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i
have rw : (∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) ↔
  ∃ (b : ι →₀ ℤ),
    x =
      ∏ i : ι, HPow.hPow (β := ℤ) (f i) ((Equiv.symm (Equiv.symm Finsupp.equivFunOnFinite) : (a : ι →₀ ℤ) → ι → ℤ) b i)
Tactic: rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
| Membership.mem (γ := Subgroup M) (closure s) x
have rw : Membership.mem (γ := Subgroup M)
  (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x
Tactic: rw [← Subtype.range_coe (s := s)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Finsupp (goal)
Goal:
M : Type u_1
inst : CommGroup M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
⊢ Membership.mem (γ := Subgroup M) (closure s) x ↔
    ∃ (a : (↑s : Type u_1) → ℤ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i
have conv_lhs : Membership.mem (γ := Subgroup M)
    (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
  ∃ (a : (↑s : Type u_1) → ℤ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i
Tactic: conv_lhs => rw [← Subtype.range_coe (s := s)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ f.range = map f ⊤
have h : ∀ (x : N), x ∈ f.range ↔ x ∈ map f ⊤
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
⊢ range (f.restrict K) = map f K
have simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]