awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
y : M
hy_1 : Membership.mem (γ := Submonoid M) (closure s) y
hy : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
⊢ ∃ (f_1 : M → ℕ) (t_1 : Finset M),
    (↑t_1 : Set M) ⊆ s ∧ Function.support f_1 ⊆ (↑t_1 : Set M) ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y
have mul : ∀ (g : M → ℕ) (u : Finset M) (hus : (↑u : Set M) ⊆ s) (hg : Function.support g ⊆ (↑u : Set M)),
  Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a) →
    ∃ (f_1 : M → ℕ) (t_1 : Finset M),
      (↑t_1 : Set M) ⊆ s ∧
        Function.support f_1 ⊆ (↑t_1 : Set M) ∧
          ∏ a ∈ t_1, a ^ f_1 a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
Tactic: obtain ⟨g, u, hus, hg, rfl⟩ := hy
Cleared hypotheses: y, hy_1, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ ∃ (f_1 : M → ℕ) (t_1 : Finset M),
    (↑t_1 : Set M) ⊆ s ∧
      Function.support f_1 ⊆ (↑t_1 : Set M) ∧
        ∏ a ∈ t_1, a ^ f_1 a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
have mul : ∏ a ∈ t ∪ u, a ^ (f + g) a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
Tactic: refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ ∏ a ∈ t ∪ u, a ^ (f + g) a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
have mul : HMul.hMul (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t ∪ u, x ^ g x) =
  HMul.hMul (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ u, x ^ g x)
Tactic: simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ HMul.hMul (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t ∪ u, x ^ g x) =
    HMul.hMul (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ u, x ^ g x)
have mul : Eq (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t, x ^ f x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : Eq (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t, x ^ f x)
⊢ HMul.hMul (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t ∪ u, x ^ g x) =
    HMul.hMul (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ u, x ^ g x)
have mul₁ : Eq (α := M) (∏ x ∈ t ∪ u, x ^ g x) (∏ x ∈ u, x ^ g x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ t ∪ u, x ^ f x) (∏ x ∈ t, x ^ f x)
have mul : Eq (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ t ∪ u, x ^ f x)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ t ∪ u, x ^ g x) (∏ x ∈ u, x ^ g x)
have mul : Eq (α := M) (∏ x ∈ u, x ^ g x) (∏ x ∈ t ∪ u, x ^ g x)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ t, x ^ f x) (∏ x ∈ t ∪ u, x ^ f x)
have mul : ∀ x ∈ t ∪ u, x ∉ t → x ^ f x = 1
Tactic: refine Finset.prod_subset Finset.subset_union_left ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ Eq (α := M) (∏ x ∈ u, x ^ g x) (∏ x ∈ t ∪ u, x ^ g x)
have mul : ∀ x ∈ t ∪ u, x ∉ u → x ^ g x = 1
Tactic: refine Finset.prod_subset Finset.subset_union_right ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have one : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
Tactic: induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have mem : ∀ (x : M) (hx : x ∈ s),
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
Tactic: induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
mem :
  ∀ (x : M) (hx : x ∈ s),
    ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have mul : ∀ (x y : M),
  Membership.mem (γ := Submonoid M) (closure s) x →
    Membership.mem (γ := Submonoid M) (closure s) y →
      ∀ (hx : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x)
        (hy :
          ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y),
        ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y
Tactic: induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have one : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
Tactic: classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have mem : ∀ (x : M) (hx : x ∈ s),
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
Tactic: classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
hx : Membership.mem (γ := Submonoid M) (closure s) x
one :
  ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1
mem :
  ∀ (x : M) (hx : x ∈ s),
    ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
have mul : ∀ (x y : M),
  Membership.mem (γ := Submonoid M) (closure s) x →
    Membership.mem (γ := Submonoid M) (closure s) y →
      ∀ (hx : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x)
        (hy :
          ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y),
        ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y
Tactic: classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Finset M
⊢ Membership.mem (γ := Submonoid M) (closure (↑s : Set M)) x →
    ∃ (f : M → ℕ), Function.support f ⊆ (↑s : Set M) ∧ ∏ a ∈ s, a ^ f a = x
have rw : (∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ (↑s : Set M) ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x) →
  ∃ (f : M → ℕ), Function.support f ⊆ (↑s : Set M) ∧ ∏ a ∈ s, a ^ f a = x
Tactic: rw [mem_closure_iff_exists_finset_subset]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.BigOperators (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
⊢ ∃ (f_1 : M → ℕ), Function.support f_1 ⊆ (↑s : Set M) ∧ Eq (α := M) (∏ a ∈ s, a ^ f_1 a) (∏ a ∈ t, a ^ f a)
have refine : ∀ x ∈ s, x ∉ t → x ^ f x = 1
Tactic: refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ HPow.hPow (β := ℕ) x 0 ∈ S
have rw : 1 ∈ S
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S
have rw : x ^ n * x ∈ S
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
ha : Membership.mem (γ := Set M) {1} a
hb : Membership.mem (γ := Set M) {1} b
⊢ Membership.mem (γ := Set M) {1} (a * b)
have hb₁ : b = 1
Tactic: push _ ∈ _ at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
ha : Membership.mem (γ := Set M) {1} a
hb : Membership.mem (γ := Set M) {1} b
hb₁ : b = 1
⊢ Membership.mem (γ := Set M) {1} (a * b)
have ha₁ : a = 1
Tactic: push _ ∈ _ at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
hb : b = 1
ha : a = 1
⊢ a * b = 1
have rw : 1 * b = 1
Tactic: rw [ha, hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
hb : b = 1
ha : a = 1
rw : 1 * b = 1
⊢ a * b = 1
have rw₁ : HMul.hMul (α := M) 1 1 = 1
Tactic: rw [ha, hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
S : Submonoid M
a b : M
hb : b = 1
ha : a = 1
rw : 1 * b = 1
rw₁ : HMul.hMul (α := M) 1 1 = 1
⊢ a * b = 1
have rw₂ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [ha, hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
inst_1 : MulOneClass N
f g : M →* N
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)} 1
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N)
Tactic: rw [Set.mem_setOf_eq, f.map_one, g.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
inst_1 : MulOneClass N
f g : M →* N
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N)
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)} 1
have rw₁ : Eq.{u_2 + 1} (α := N) (1 : N) ((g : (a : M) → N) 1 : N)
Tactic: rw [Set.mem_setOf_eq, f.map_one, g.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
s : Set M
inst_1 : MulOneClass N
f g : M →* N
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) ((g : (a : M) → N) 1 : N)
rw₁ : Eq.{u_2 + 1} (α := N) (1 : N) ((g : (a : M) → N) 1 : N)
⊢ Membership.mem (γ := Set M) {x : M | Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)} 1
have rw₂ : Eq.{u_2 + 1} (α := N) 1 1
Tactic: rw [Set.mem_setOf_eq, f.map_one, g.map_one]
-- 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
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
have this : x = 1
Tactic: have : x = 1 := funext fun i => h1 i (Finset.notMem_empty 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
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 = Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)
have h : ∀ (j : η), x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
Tactic: ext j
-- 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
j : η
⊢ x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
have pos : ∀ (heq : j = i), x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
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
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
j : η
pos : ∀ (heq : j = i), x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
⊢ x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
have neg : ∀ (heq : ¬j = i), x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
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
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
j : η
heq : j = i
⊢ x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
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),
  x j = (Function.update (β := f) x j 1 * Pi.mulSingle (M := f) j (x j)) j
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
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
have this : x = Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)
Tactic: 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]