awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
this : x = Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)
⊢ x ∈ H
have insert : Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i) ∈ H
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
⊢ Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i) ∈ H
have apply : ∀ i_1 ∉ I, Function.update (β := f) x i 1 i_1 = 1
Tactic: apply mul_mem (ih _ _ _) (by simp [h2])
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
apply : ∀ i_1 ∉ I, Function.update (β := f) x i 1 i_1 = 1
⊢ Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i) ∈ H
have apply₁ : ∀ i_1 ∈ I, Pi.mulSingle (M := f) i_1 (Function.update (β := f) x i 1 i_1) ∈ H
Tactic: apply mul_mem (ih _ _ _) (by simp [h2])
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
⊢ Function.update (β := f) x i 1 j = 1
have pos : ∀ (heq : j = i), Function.update (β := f) x i 1 j = 1
Tactic: by_cases heq : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
pos : ∀ (heq : j = i), Function.update (β := f) x i 1 j = 1
⊢ Function.update (β := f) x i 1 j = 1
have neg : ∀ (heq : ¬j = i), Function.update (β := f) x i 1 j = 1
Tactic: by_cases heq : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : j = i
⊢ Function.update (β := f) x i 1 j = 1
have pos : ∀ (hnotMem : j ∉ I) (h1 : ∀ i ∉ insert j I, x i = 1) (h2 : ∀ i ∈ insert j I, Pi.mulSingle (M := f) i (x i) ∈ H),
  Function.update (β := f) x j 1 j = 1
Tactic: subst heq
Cleared hypotheses: i, hnotMem, h1, h2, heq
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (hypothesis)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ Pi.mulSingle (M := f) j (Function.update (β := f) x i 1 j) ∈ H
have this : j ≠ i
Tactic: have : j ≠ i := fun h => h ▸ hnotMem <| hj
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle (M := f) j (Function.update (β := f) x i 1 j) ∈ H
have simp : Pi.mulSingle (M := f) j (x j) ∈ H
Tactic: simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
I : Finset η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ I, x i = 1
h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H
⊢ x ∈ H
have empty : ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ ∅, x i = 1)
  (h2 : ∀ (i : η), Membership.mem (γ := Finset η) ∅ i → Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H
Tactic: induction I using Finset.induction_on generalizing x with
  | empty =>
    have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
    exact this ▸ one_mem H
  | insert i I hnotMem ih =>
    have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by
      ext j
      by_cases heq : j = i
      · subst heq
        simp
      · simp [heq]
    rw [this]
    clear this
    apply mul_mem (ih _ _ _) (by simp [h2]) <;> clear ih <;> intro j hj
    · by_cases heq : j = i
      · subst heq
        simp
      · simpa [heq] using h1 j (by simpa [heq] using hj)
    · have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)
Cleared hypotheses: I, x, h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : DecidableEq η
I : Finset η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ I, x i = 1
h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H
empty :
  ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ ∅, x i = 1)
    (h2 : ∀ (i : η), Membership.mem (γ := Finset η) ∅ i → Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H
⊢ x ∈ H
have insert : ∀ (i : η) (I : Finset η) (hnotMem : i ∉ I)
  (ih : ∀ (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle (M := f) i (x i) ∈ H), x ∈ H)
  (x : (i : η) → f i) (h1 : ∀ i_1 ∉ insert i I, x i_1 = 1)
  (h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H), x ∈ H
Tactic: induction I using Finset.induction_on generalizing x with
  | empty =>
    have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
    exact this ▸ one_mem H
  | insert i I hnotMem ih =>
    have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by
      ext j
      by_cases heq : j = i
      · subst heq
        simp
      · simp [heq]
    rw [this]
    clear this
    apply mul_mem (ih _ _ _) (by simp [h2]) <;> clear ih <;> intro j hj
    · by_cases heq : j = i
      · subst heq
        simp
      · simpa [heq] using h1 j (by simpa [heq] using hj)
    · have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)
Cleared hypotheses: I, x, h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
S : Type u_3
inst_1 : SetLike S ((i : η) → f i)
inst_2 : SubmonoidClass S ((i : η) → f i)
inst_3 : Finite η
inst_4 : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle (M := f) i (x i) ∈ H
⊢ x ∈ H
have intro : ∀ (val : Fintype η), x ∈ H
Tactic: cases nonempty_fintype η
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (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 : (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 : (a : f i) → (i : η) → f i) _x j : f j)
Tactic: by_cases H : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (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 : (a : f i) → (i : η) → f i) _x j : f j)
⊢ Membership.mem (α := f j) (s j) ((MonoidHom.mulSingle 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 : (a : f i) → (i : η) → f i) _x j : f j)
Tactic: by_cases H : j = i
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finite (goal)
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (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 : (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 : (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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x_1 x y : M
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
hy : Membership.mem (γ := Submonoid 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 (γ := Submonoid 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 (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid 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 (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid 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 (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : Membership.mem (γ := Submonoid 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 (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 (γ := Submonoid M) (closure (Set.range f)) x)
  (hy : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : Membership.mem (γ := Submonoid 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 (γ := Submonoid M) (closure (Set.range f)) x)
  (hy : Membership.mem (γ := Submonoid 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 [pow_add]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
hx : Membership.mem (γ := Submonoid M) (closure (Set.range f)) x
⊢ ∃ (a : ι → ℕ), x = ∏ i : ι, f i ^ a i
have obtain : ∀ (a : ι →₀ ℕ)
  (hx : Membership.mem (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ Membership.mem (γ := Submonoid 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 (γ := Submonoid M) (closure (Set.range f)) x
Tactic: refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst_1 : Fintype ι
⊢ Membership.mem (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
| Membership.mem (γ := Submonoid M) (closure s) x
have rw : Membership.mem (γ := Submonoid 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.Submonoid.Finsupp (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
inst_1 : Fintype (↑s : Type u_1)
⊢ Membership.mem (γ := Submonoid M) (closure s) x ↔
    ∃ (a : (↑s : Type u_1) → ℕ), x = ∏ i : (↑s : Type u_1), (↑i : M) ^ a i
have conv_lhs : Membership.mem (γ := Submonoid 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.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : MulOneClass M
ι : Sort u_4
inst_1 : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun (x1 x2 : Submonoid M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Submonoid M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
have suffices : Membership.mem (γ := Submonoid M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
Tactic: suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this