awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (ϕ x : (a : N x) → M) ((f * g) x) =
    HMul.hMul (α := ι → M) (β := ι → M) (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i))
      (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) x

Tactic:
exact map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
i j : ι
h : i ≠ j
⊢ Commute.{u_1} (S := M) ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (g i) : M)) i)
    ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (f i) : M)) j)

Tactic:
hcomm h _ _
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
i j : ι
h : i ≠ j
⊢ Commute.{u_1} (S := M) ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (g i) : M)) i)
    ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (f i) : M)) j)

Tactic:
exact hcomm h _ _
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
h :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      (ϕ x : (a : N x) → M) ((f * g) x) =
        HMul.hMul (α := ι → M) (β := ι → M) (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i))
          (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) x
convert_4 convert_4₁ :
  (↑Finset.univ : Set ι).Pairwise fun (x y : ι) ↦
    Commute.{u_1} (S := M) ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (g i) : M)) x)
      ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (f i) : M)) y)
⊢ Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) ((f * g) i)) ⋯ =
    HMul.hMul (α := M) (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i)) ⋯)
      (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) ⋯)

Tactic:
classical
    convert! @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
    · exact map_mul _ _ _
    · rintro i - j - h
      exact hcomm h _ _

Premises used: Finset.noncommProd_mul_distrib, map_mul, DFunLike.coe
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
change :
  Eq.{u_1 + 1} (α := M)
    (Finset.noncommProd Finset.univ (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ : M)
    ((ϕ i : (a : N i) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M) ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) (Pi.mulSingle (M := N) i y) : M)
    ((ϕ i : (a : N i) → M) y : M)

Tactic:
change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _)
    = ϕ i y

Premises used: Finset.univ, Finset.noncommProd, DFunLike.coe, Pi.mulSingle
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
rw :
  Eq.{u_1 + 1} (α := M)
    ((insert i (Finset.erase Finset.univ i)).noncommProd
        (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
      M)
    ((ϕ i : (a : N i) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M)
    (Finset.noncommProd Finset.univ (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ : M)
    ((ϕ i : (a : N i) → M) y : M)

Tactic:
rw [← Finset.insert_erase (Finset.mem_univ i)]

Premises used: Finset.mem_univ, Finset.insert_erase
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
rw :
  HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) (Pi.mulSingle (M := N) i y i) : M)
      ((Finset.erase Finset.univ i).noncommProd (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
        M) =
    (ϕ i : (a : N i) → M) y
⊢ Eq.{u_1 + 1} (α := M)
    ((insert i (Finset.erase Finset.univ i)).noncommProd
        (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
      M)
    ((ϕ i : (a : N i) → M) y : M)

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ (Finset.notMem_erase i _)]

Premises used: Finset.notMem_erase, Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
rw :
  HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M)
      ((Finset.erase Finset.univ i).noncommProd (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
        M) =
    (ϕ i : (a : N i) → M) y
⊢ HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) (Pi.mulSingle (M := N) i y i) : M)
      ((Finset.erase Finset.univ i).noncommProd (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
        M) =
    (ϕ i : (a : N i) → M) y

Tactic:
rw [Pi.mulSingle_eq_same]

Premises used: Pi.mulSingle_eq_same
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
rw :
  HMul.hMul (α := M) ((ϕ i : (a : N i) → M) y : M) (HPow.hPow (α := M) 1 (Finset.erase Finset.univ i).card) =
    (ϕ i : (a : N i) → M) y
m : M
h :
  ∀ x ∈ Finset.erase Finset.univ i,
    Eq.{u_1 + 1} (α := M) ((ϕ x : (a : N x) → M) (Pi.mulSingle (M := N) i y x) : M) (1 : M)
⊢ HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M)
      ((Finset.erase Finset.univ i).noncommProd (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
        M) =
    (ϕ i : (a : N i) → M) y

Tactic:
rw [Finset.noncommProd_eq_pow_card]

Premises used: Finset.noncommProd_eq_pow_card
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
rw : HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M) (1 : M) = (ϕ i : (a : N i) → M) y
⊢ HMul.hMul (α := M) ((ϕ i : (a : N i) → M) y : M) (HPow.hPow (α := M) 1 (Finset.erase Finset.univ i).card) =
    (ϕ i : (a : N i) → M) y

Tactic:
rw [one_pow]

Premises used: one_pow
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
⊢ HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M) (1 : M) = (ϕ i : (a : N i) → M) y

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
⊢ HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M) (1 : M) = (ϕ i : (a : N i) → M) y

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
j : ι
hj : j ∈ Finset.erase Finset.univ i
⊢ j ≠ i ∧ Membership.mem (γ := Finset ι) Finset.univ j

Tactic:
simp only [Finset.mem_erase] at hj

Premises used: Finset.mem_erase
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
i : ι
y : N i
j : ι
hj : j ≠ i ∧ Membership.mem (γ := Finset ι) Finset.univ j
⊢ Eq.{u_1 + 1} (α := M) ((ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j) : M) (1 : M)

Tactic:
simp [hj]
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ_1 : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ_1 i : (a : N i) → M) x : M) ((ϕ_1 j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
ϕ :
  { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
    Pairwise fun (i j : ι) ↦
      ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }
a :
  ∀ (x : ι) (x_1 : N x),
    Eq.{u_1 + 1} (α := M)
      (((↑((fun (f : ((i : ι) → N i) →* M) ↦
                      (Subtype.mk (p := fun (ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M) ↦
                          Pairwise fun (i j : ι) ↦
                            ∀ (x : N i) (y : N j),
                              Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M))
                          (fun (i : ι) ↦ f.comp (mulSingle N i)) ⋯ :
                        { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                          Pairwise fun (i j : ι) ↦
                            ∀ (x : N i) (y : N j),
                              Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }))
                    ((fun
                          (ϕ :
                            { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                              Pairwise fun (i j : ι) ↦
                                ∀ (x : N i) (y : N j),
                                  Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M)
                                    ((ϕ j : (a : N j) → M) y : M) }) ↦
                        noncommPiCoprod (N := N) (↑ϕ : (i : ι) → N i →* M) ⋯)
                      ϕ)) :
                (i : ι) → N i →* M)
              x :
            (a : N x) → M)
          x_1 :
        M)
      (((↑ϕ : (i : ι) → N i →* M) x : (a : N x) → M) x_1 : M)
⊢ (fun (f : ((i : ι) → N i) →* M) ↦
        (Subtype.mk (p := fun (ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M) ↦
            Pairwise fun (i j : ι) ↦
              ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M))
            (fun (i : ι) ↦ f.comp (mulSingle N i)) ⋯ :
          { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
            Pairwise fun (i j : ι) ↦
              ∀ (x : N i) (y : N j),
                Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }))
      ((fun
            (ϕ :
              { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                Pairwise fun (i j : ι) ↦
                  ∀ (x : N i) (y : N j),
                    Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }) ↦
          noncommPiCoprod (N := N) (↑ϕ : (i : ι) → N i →* M) ⋯)
        ϕ) =
    ϕ

Tactic:
ext
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ_1 : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ_1 i : (a : N i) → M) x : M) ((ϕ_1 j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
ϕ :
  { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
    Pairwise fun (i j : ι) ↦
      ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }
x : ι
x_1 : N x
⊢ Eq.{u_1 + 1} (α := M)
    (((↑((fun (f : ((i : ι) → N i) →* M) ↦
                    (Subtype.mk (p := fun (ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M) ↦
                        Pairwise fun (i j : ι) ↦
                          ∀ (x : N i) (y : N j),
                            Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M))
                        (fun (i : ι) ↦ f.comp (mulSingle N i)) ⋯ :
                      { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                        Pairwise fun (i j : ι) ↦
                          ∀ (x : N i) (y : N j),
                            Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }))
                  ((fun
                        (ϕ :
                          { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                            Pairwise fun (i j : ι) ↦
                              ∀ (x : N i) (y : N j),
                                Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }) ↦
                      noncommPiCoprod (N := N) (↑ϕ : (i : ι) → N i →* M) ⋯)
                    ϕ)) :
              (i : ι) → N i →* M)
            x :
          (a : N x) → M)
        x_1 :
      M)
    (((↑ϕ : (i : ι) → N i →* M) x : (a : N x) → M) x_1 : M)

Tactic:
simp only [coe_comp, Function.comp_apply, mulSingle_apply, noncommPiCoprod_mulSingle]

Premises used: MonoidHom.coe_comp, MonoidHom.noncommPiCoprod_mulSingle, MonoidHom.mulSingle_apply, Function.comp_apply
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
inst_3 : DecidableEq ι
f : ((i : ι) → N i) →* M
i : ι
x : N i
⊢ Eq.{u_1 + 1} (α := M)
    (((fun
                (ϕ :
                  { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                    Pairwise fun (i j : ι) ↦
                      ∀ (x : N i) (y : N j),
                        Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }) ↦
              noncommPiCoprod (N := N) (↑ϕ : (i : ι) → N i →* M) ⋯)
            ((fun (f : ((i : ι) → N i) →* M) ↦
                (Subtype.mk (p := fun (ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M) ↦
                    Pairwise fun (i j : ι) ↦
                      ∀ (x : N i) (y : N j),
                        Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M))
                    (fun (i : ι) ↦ f.comp (mulSingle N i)) ⋯ :
                  { ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M //
                    Pairwise fun (i j : ι) ↦
                      ∀ (x : N i) (y : N j),
                        Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M) }))
              f) :
          (a : (i : ι) → N i) → M)
        (Pi.mulSingle (M := N) i x) :
      M)
    ((f : (a : (i : ι) → N i) → M) (Pi.mulSingle (M := N) i x) : M)

Tactic:
simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, mulSingle_apply]

Premises used: MonoidHom.coe_comp, MonoidHom.noncommPiCoprod_mulSingle, MonoidHom.mulSingle_apply, Function.comp_apply
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
a : LE.le (α := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) (⨆ (i : ι), mrange (ϕ i))
a₁ : LE.le (α := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))
⊢ Eq (α := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) (⨆ (i : ι), mrange (ϕ i))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i))
    ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) f : M)

Tactic:
Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)

Premises used: Multiset.foldr, Multiset.map, Set.Mem, Multiset.noncommFoldr, Multiset.noncommFold, Finset.noncommProd, Submonoid.noncommProd_mem, Multiset.noncommProd
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
a :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) ((ϕ i : (a : N i) → M) (f i) : M)
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i))
    ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) f : M)

Tactic:
refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)

Premises used: Submonoid.noncommProd_mem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
a :
  Membership.mem (γ := Set (Submonoid M)) (Set.range fun (i : ι) ↦ mrange (ϕ i))
    ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
a₁ :
  Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
    ((ϕ i : (a : N i) → M) (f i) : M)
a₂ : Submonoid M
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) ((ϕ i : (a : N i) → M) (f i) : M)

Tactic:
apply Submonoid.mem_sSup_of_mem

Premises used: Submonoid.mem_sSup_of_mem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
w : ι
h :
  Eq.{u_1 + 1} (α := Submonoid M) ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
    ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
⊢ Membership.mem (γ := Set (Submonoid M)) (Set.range fun (i : ι) ↦ mrange (ϕ i))
    ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)

Tactic:
use i
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
    ((ϕ i : (a : N i) → M) (f i) : M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
⊢ LE.le (α := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))

Tactic:
iSup_le ?_

Premises used: Set.Mem, iSup_le
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
a : ∀ (i : ι), LE.le (α := Submonoid M) (mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))
⊢ LE.le (α := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))

Tactic:
refine iSup_le ?_

Premises used: iSup_le
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : N i
⊢ Membership.mem (α := M) (γ := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) ((ϕ i : (a : N i) → M) y : M)

Tactic:
⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Premises used: Set.Mem, setOf, MonoidHom.noncommPiCoprod_mulSingle, Exists.intro, Set.range, Pi.mulSingle