awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
h : Eq.{u_1 + 1} (α := M) 1 (Finsupp.prod 0 fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)
⊢ ∃ (a : ι →₀ ℤ), Eq.{u_1 + 1} (α := M) 1 (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)

Tactic:
use 0
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ Eq.{u_1 + 1} (α := M) 1 (Finsupp.prod 0 fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
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
⊢ ∃ (a : ι →₀ ℤ), x * y = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 :
  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
⊢ ∃ (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:
use v + w
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
h₁ : ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂
⊢ 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:
rw [Finsupp.prod_add_index]

Premises used: Finsupp.prod_add_index
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 ∈ v.support ∪ w.support, HPow.hPow (β := ℤ) (f a) 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
simp [zpow_add]

Premises used: zpow_add
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
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)
⊢ ∃ (a : ι →₀ ℤ), x⁻¹ = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
obtain ⟨a, rfl⟩ := hx'

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 (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:
use -a
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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))
h₁ : ∀ (a : ι), HPow.hPow (β := ℤ) (f a) 0 = 1
⊢ Eq.{u_1 + 1} (α := M) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)⁻¹ ((-a).prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)

Tactic:
rw [Finsupp.prod_neg_index]

Premises used: Finsupp.prod_neg_index
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 (a : ι) (b : ℤ) ↦ f a ^ (-b))

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 : ι), HPow.hPow (β := ℤ) (f a) 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
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
⊢ ∃ (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

Premises used: zpow_add, Finsupp.prod_add_index, Subgroup.mul, Subgroup.one, Finsupp.prod_neg_index, Subgroup.inv, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
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
⊢ ∃ (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

Premises used: zpow_add, Finsupp.prod_add_index, Subgroup.mul, Subgroup.one, Finsupp.prod_neg_index, Subgroup.inv, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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
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)
⊢ ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i

Tactic:
obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx

Premises used: rfl, Subgroup.exists_finsupp_of_mem_closure_range
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
inst_1 : Fintype ι
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)
    (∏ i : ι, HPow.hPow (β := ℤ) (f i) ((a : (a : ι) → ℤ) i : ℤ))

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
inst_1 : Fintype ι
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:
exact ⟨a, by simp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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

Tactic:
⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Premises used: Iff.intro, Subgroup.exists_finsupp_of_mem_closure_range
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
refine :
  (∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2) →
    Membership.mem (γ := Subgroup M) (closure (Set.range f)) x
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) x ↔
    ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
a : ι →₀ ℤ
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)

Tactic:
Submonoid.prod_mem _ fun i hi ↦ zpow_mem (subset_closure (Set.mem_range_self i)) _

Premises used: Set.mem_range_self, Submonoid.prod_mem, Set.Mem, zpow_mem, Subgroup.subset_closure, DFunLike.coe, Finsupp.prod
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
a : ι →₀ ℤ
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) (a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2)

Tactic:
exact Submonoid.prod_mem _ fun i hi ↦ zpow_mem (subset_closure (Set.mem_range_self i)) _

Premises used: Submonoid.prod_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
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)
⊢ Membership.mem (γ := Subgroup M) (closure (Set.range f)) x ↔ ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Premises used: Equiv.exists_congr_left, Finsupp.equivFunOnFinite, Subgroup.mem_closure_range_iff, Equiv.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
⊢ (∃ (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:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
rw :
  Membership.mem (γ := Subgroup M)
    (closure (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x
| Membership.mem (γ := Subgroup M) (closure s) x

Tactic:
rw [← Subtype.range_coe (s := s)]

Premises used: Subtype.range_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
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
⊢ Membership.mem (γ := Subgroup M) (closure 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)]

Premises used: Subtype.range_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 (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:
mem_closure_range_iff_of_fintype

Premises used: Subgroup.mem_closure_range_iff_of_fintype
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
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 (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:
exact mem_closure_range_iff_of_fintype

Premises used: Subgroup.mem_closure_range_iff_of_fintype
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
f : G →* N
⊢ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(map f ⊤) : Set N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ (↑f.range : Set N) = Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
y : N
⊢ y ∈ f.range ↔ ∃ (x : G), (f : (a : G) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
h : ∀ (x : N), x ∈ f.range ↔ x ∈ map f ⊤
⊢ f.range = map f ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
x : N
⊢ x ∈ f.range ↔ x ∈ map f ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G_1 : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G_1
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N_1 : Type u_5
P : Type u_6
inst_4 : Group N_1
inst_5 : Group P
K : Subgroup G_1
G : Type u_7
inst_6 : Group G
inst_7 : IsMulCommutative G
N : Type u_8
inst_8 : Group N
f : G →* N
⊢ IsMulCommutative.{u_8} ↥f.range

Tactic:
range_eq_map f ▸ Subgroup.map_isMulCommutative ⊤ f

Premises used: MonoidHom.range_eq_map, Eq.rec, Top.top, Eq.symm, Subgroup.map_isMulCommutative
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
simp_rw₁ :
  ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
simp_rw₂ :
  ∀ (x : N),
    (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔
      ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₃ : ∀ (x : N), (∃ (x_1 : ↥K), (f : (a : G) → N) (↑x_1 : G) = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₄ : ∀ (x : N), (∃ (x_1 : G) (_ : x_1 ∈ K), (f : (a : G) → N) x_1 = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₅ : ∀ (x : N), True
⊢ range (f.restrict K) = map f K

Tactic:
simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]

Premises used: MonoidHom.restrict_apply, SetLike.ext_iff, exists_prop, MonoidHom.mem_range, Subgroup.mem_map, forall_const, SetLike.exists
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : G
⊢ Eq.{u_5 + 1} (α := N) ((↑((f.rangeRestrict : (a : G) → ↥f.range) g) : N) : N) ((f : (a : G) → N) g : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ Eq (α := G → N)
    (Function.comp (β := ↥f.range) (Subtype.val (p := fun (x : N) ↦ x ∈ f.range))
      (⇑f.rangeRestrict : (a : G) → ↥f.range))
    (⇑f : (a : G) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ f.range.subtype.comp f.rangeRestrict = f

Tactic:
ext <| f.coe_rangeRestrict

Premises used: MonoidHom.ext, MonoidHom.coe_rangeRestrict
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := ↥f.range) (⇑f.rangeRestrict : (a : G) → ↥f.range)

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

Premises used: MonoidHom.rangeRestrict, Exists, _private.0.MonoidHom.rangeRestrict_surjective.match_1, Exists.intro, Eq, DFunLike.coe, Function.Surjective, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ Injective (Set.codRestrict (⇑f : (a : G) → N) (↑f.range : Set N) ⋯) ↔
    Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)

Tactic:
Set.injective_codRestrict _

Premises used: Set.injective_codRestrict
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ Injective.{u_1 + 1, u_5 + 1} (α := G) (β := ↥f.range) (⇑f.rangeRestrict : (a : G) → ↥f.range) ↔
    Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)

Tactic:
convert! Set.injective_codRestrict _

Premises used: Set.injective_codRestrict
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
P : Type u_6
inst_1 : Group N
inst_2 : Group P
g : N →* P
f : G →* N
rw : map g (map f ⊤) = map (g.comp f) ⊤
⊢ map g f.range = (g.comp f).range

Tactic:
rw [range_eq_map, range_eq_map]

Premises used: MonoidHom.range_eq_map
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
P : Type u_6
inst_1 : Group N
inst_2 : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤

Tactic:
(⊤ : Subgroup G).map_map g f

Premises used: Top.top, Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
P : Type u_6
inst_1 : Group N
inst_2 : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤

Tactic:
exact (⊤ : Subgroup G).map_map g f

Premises used: Top.top, Subgroup.map_map
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
P : Type u_6
inst_1 : Group N
inst_2 : Group P
g : N →* P
f : G →* N
⊢ (g.comp f).range = map g f.range

Tactic:
(map_range ..).symm

Premises used: MonoidHom.map_range, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_7
inst_1 : Group N
f : G →* N
rw :
  Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑⊤ : Set N) ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
rw₁ rw₂ :
  Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
⊢ (↑f.range : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ

Tactic:
rw [coe_range, coe_top]

Premises used: Subgroup.coe_top, MonoidHom.coe_range
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_7
inst_1 : Group N
f : G →* N
hf : Surjective.{u_1 + 1, u_7 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ f.range = ⊤

Tactic:
range_eq_top.2 hf

Premises used: Iff.mpr, MonoidHom.range_eq_top
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
x : N
⊢ Membership.mem (γ := Subgroup N) (range.{u_1, u_5} (G := G) 1) x ↔ Membership.mem (γ := Subgroup N) ⊥ x

Tactic:
simpa using @comm _ (· = ·) _ 1 x

Premises used: comm
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.subtype.range = H

Tactic:
SetLike.coe_injective <| (coe_range _).trans <| Subtype.range_coe

Premises used: SetLike.coe_injective, Subtype.range_coe, MonoidHom.coe_range, Eq.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h_le : H ≤ K
⊢ (inclusion h_le).range = H.subgroupOf K

Tactic:
Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g

Premises used: Set.range_inclusion, Iff.mp, Set.ext_iff, Subgroup.ext