awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_5
inst : Monoid M
A : Type u_4
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : ↥S
n : ℕ
⊢ (↑(x ^ n) : M) = (↑x : M) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_5
inst : Monoid M
A : Type u_4
inst_1 : SetLike A M
inst_2 : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx ^ n = Subtype.mk (p := fun (x : M) ↦ x ∈ S) (x ^ n) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
inst : MulOneClass M
inst_1 : SetLike A M
hA : SubmonoidClass A M
S' : A
x x_1 : ↥S'
⊢ (↑(x * x_1) : M) = (↑x : M) * (↑x_1 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
A : Type u_3
inst : MulOneClass M
inst_1 : SetLike A M
hA : SubmonoidClass A M
S' : A
x : ↥S'
⊢ (subtype S' : (a : ↥S') → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
A : Type u_3
inst : MulOneClass M
inst_1 : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ Function.Injective (α := ↥S') (β := M) (⇑(subtype S') : (a : ↥S') → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_1
A : Type u_3
inst : MulOneClass M
inst_1 : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ Eq (α := (a : ↥S') → M) (⇑(subtype S') : (a : ↥S') → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S'))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
x y : ↥S
⊢ (↑(x * y) : M) = (↑x : M) * (↑y : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
⊢ Eq.{u_4 + 1} (α := M) (↑1 : M) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
a : M
ha : a ∈ S
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S) a ha = 1 ↔ a = 1

Tactic:
simp [← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
x y : M
hx : x ∈ S
hy : y ∈ S
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx * Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy =
    Subtype.mk (p := fun (x : M) ↦ x ∈ S) (x * y) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
x y : ↥S
⊢ x * y = Subtype.mk (p := fun (x : M) ↦ x ∈ S) ((↑x : M) * (↑y : M)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
⊢ 1 = Subtype.mk (p := fun (x : M) ↦ x ∈ S) 1 ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_5
inst : Monoid M
S : Submonoid M
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n ∈ S

Tactic:
pow_mem hx n

Premises used: pow_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : MulOneClass M_1
inst_1 : SetLike A M_1
hA : SubmonoidClass A M_1
S' : A
M : Type u_4
inst_2 : MulOneClass M
S : Submonoid M
x x_1 : ↥S
⊢ (↑(x * x_1) : M) = (↑x : M) * (↑x_1 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
s : Submonoid M
x : ↥s
⊢ (s.subtype : (a : ↥s) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
s : Submonoid M
⊢ Function.Injective (α := ↥s) (β := M) (⇑s.subtype : (a : ↥s) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Submonoid.Defs
Goal:
M : Type u_4
inst : MulOneClass M
S : Submonoid M
⊢ Eq (α := (a : ↥S) → M) (⇑S.subtype : (a : ↥S) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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 = 1

Tactic:
have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
this : x = 1
⊢ x ∈ H

Tactic:
this ▸ one_mem H

Premises used: Eq.rec, OneMemClass.one_mem, Eq.symm
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
this : x = 1
⊢ x ∈ H

Tactic:
exact this ▸ one_mem H
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
h : ∀ (j : η), x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j
⊢ x = Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)

Tactic:
ext j
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
neg : ∀ (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

Tactic:
by_cases heq : j = i
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
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
⊢ x j = (Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i)) j

Tactic:
subst heq
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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 : Finset η
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
j : η
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:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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

Tactic:
simp [heq]
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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)

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]
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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.insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ Insert.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)
insert : Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i) ∈ H
⊢ x ∈ H

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
⊢ Pi.mulSingle (M := f) i (x i) ∈ H

Tactic:
simp [h2]
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
apply₁ : ∀ i_1 ∈ I, Pi.mulSingle (M := f) i_1 (Function.update (β := f) x i 1 i_1) ∈ H
⊢ Function.update (β := f) x i 1 * Pi.mulSingle (M := f) i (x i) ∈ H

Tactic:
apply mul_mem (ih _ _ _) (by simp [h2])

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
neg : ∀ (heq : ¬j = i), Function.update (β := f) x i 1 j = 1
⊢ Function.update (β := f) x i 1 j = 1

Tactic:
by_cases heq : j = i
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
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
⊢ Function.update (β := f) x i 1 j = 1

Tactic:
subst heq
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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 : Finset η
x : (i : η) → f i
j : η
hj 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:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
⊢ j ∉ insert i I

Tactic:
simpa [heq] using hj
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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

Tactic:
simpa [heq] using h1 j (by simpa [heq] using hj)
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
⊢ j ≠ i

Tactic:
have : j ≠ i := fun h => h ▸ hnotMem <| hj
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
simp : Pi.mulSingle (M := f) j (x j) ∈ H
⊢ Pi.mulSingle (M := f) j (Function.update (β := f) x i 1 j) ∈ H

Tactic:
simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]

Premises used: ne_eq, not_false_eq_true, Function.update_of_ne
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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 (x j) ∈ H

Tactic:
h2 _ (Finset.mem_insert_of_mem hj)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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 (x j) ∈ H

Tactic:
exact h2 _ (Finset.mem_insert_of_mem hj)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
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.insert i I, x i_1 = 1)
    (h2 : ∀ i_1 ∈ Insert.insert i I, Pi.mulSingle (M := f) i_1 (x i_1) ∈ H), x ∈ 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)

Premises used: Insert.insert, ne_eq, not_false_eq_true, Function.update_of_ne
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
intro : ∀ (val : Fintype η), x ∈ H
⊢ x ∈ H

Tactic:
cases nonempty_fintype η

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
val : Fintype η
⊢ ∀ i ∉ Finset.univ, x i = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
val : Fintype η
⊢ x ∈ H

Tactic:
exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

Premises used: Finset.univ, Submonoid.pi_mem_of_mulSingle_mem_aux
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
Goal:
η : Type u_1
f : η → Type u_2
inst : (i : η) → MulOneClass (f i)
inst_1 : Finite η
inst_2 : DecidableEq η
H_1 : (i : η) → Submonoid (f i)
J : Submonoid ((i : η) → f i)
h : pi (M := f) univ H_1 ≤ J
i : η
x_1 : (i : η) → f i
h_1 :
  Membership.mem (γ := Submonoid ((i : η) → f i)) (map (F := f i →* (i : η) → f i) (MonoidHom.mulSingle f i) (H_1 i))
    x_1
x : f i
hx : x ∈ (↑(H_1 i) : Set (f i))
H : (MonoidHom.mulSingle f i : (a : f i) → (i : η) → f i) x = x_1
⊢ x_1 ∈ pi (M := f) univ H_1

Tactic:
simpa [← H]
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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)
neg : ∀ (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)

Tactic:
by_cases H : j = i
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
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)
⊢ Membership.mem (α := f j) (s j) ((MonoidHom.mulSingle f i : (a : f i) → (i : η) → f i) _x j : f j)

Tactic:
subst H
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
j : η
_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:
simpa
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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)

Tactic:
simpa [H] using hs _
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
⊢ LE.le (α := Submonoid ((i : η) → f i)) (pi (M := f) univ fun (i : η) ↦ closure (s i))
    (closure (Set.pi (α := f) univ fun (i : η) ↦ s i))

Tactic:
exact pi_le_iff.mpr fun i => map_le_of_le_comap _ <| closure_le.2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Premises used: Iff.mpr, Submonoid.map_le_of_le_comap, Submonoid.pi_le_iff, Submonoid.closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Finite
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
⊢ LE.le (α := Submonoid ((i : η) → f i)) (pi (M := f) univ fun (i : η) ↦ closure (s i))
    (closure (Set.pi (α := f) univ fun (i : η) ↦ s i))

Tactic:
classical
      exact pi_le_iff.mpr fun i => map_le_of_le_comap _ <| closure_le.2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Premises used: Iff.mpr, Submonoid.map_le_of_le_comap, Submonoid.pi_le_iff, Submonoid.closure, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x_1 x : M
h : x ∈ Set.range f
mem : ∀ (i : ι), ∃ (a : ι →₀ ℕ), f i = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℕ), x = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
obtain ⟨i, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = Finsupp.prod (Finsupp.single i 1) fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ (a : ι →₀ ℕ), f i = a.prod fun (x1 : ι) (x2 : ℕ) ↦ f x1 ^ x2

Tactic:
exact ⟨Finsupp.single i 1, by simp⟩
-- Module: Mathlib.Algebra.Group.Submonoid.Finsupp
Goal:
M : Type u_1
inst : CommMonoid 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