awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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) (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
have 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)) sorry :
      M) =
  (ϕ i : (a : N i) → M) y
Tactic: rw [Pi.mulSingle_eq_same]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
      ((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
have 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
Tactic: rw [Finset.noncommProd_eq_pow_card]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 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
have m : M
Tactic: rw [Finset.noncommProd_eq_pow_card]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 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
have 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)
Tactic: rw [Finset.noncommProd_eq_pow_card]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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) ((ϕ i : (a : N i) → M) y : M) (HPow.hPow (α := M) 1 (Finset.erase Finset.univ i).card) =
    (ϕ i : (a : N i) → M) y
have rw : HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) y : M) (1 : M) = (ϕ i : (a : N i) → M) y
Tactic: rw [one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := M) ((ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j) : M) (1 : M)
have hj₁ : j ≠ i ∧ Membership.mem (γ := Finset ι) Finset.univ j
Tactic: simp only [Finset.mem_erase] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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) }
⊢ (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) ⋯)
        ϕ) =
    ϕ
have 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)) sorry :
                      { ϕ : (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) sorry)
                    ϕ)) :
              (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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 ι
⊢ Eq (α := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) (⨆ (i : ι), mrange (ϕ i))
have a : LE.le (α := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) (⨆ (i : ι), mrange (ϕ i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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))
⊢ Eq (α := Submonoid M) (mrange (noncommPiCoprod (N := N) ϕ hcomm)) (⨆ (i : ι), mrange (ϕ i))
have a₁ : LE.le (α := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
have 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)
Tactic: refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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) (⨆ (i : ι), mrange (ϕ i)) ((ϕ i : (a : N i) → M) (f i) : M)
have a : Membership.mem (γ := Set (Submonoid M)) (Set.range fun (i : ι) ↦ mrange (ϕ i))
  ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
Tactic: apply Submonoid.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) ((ϕ i : (a : N i) → M) (f i) : M)
have 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)
Tactic: apply Submonoid.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
⊢ Membership.mem.{u_1, u_1} (α := M) (γ := Submonoid M) (⨆ (i : ι), mrange (ϕ i)) ((ϕ i : (a : N i) → M) (f i) : M)
have a₂ : Submonoid M
Tactic: apply Submonoid.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
w : ι
⊢ Membership.mem (γ := Set (Submonoid M)) (Set.range fun (i : ι) ↦ mrange (ϕ i))
    ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
have h : Eq.{u_1 + 1} (α := Submonoid M) ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
  ((fun (i : ι) ↦ (mrange (ϕ i) : Submonoid M)) i)
Tactic: use i
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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))
have a : ∀ (i : ι), LE.le (α := Submonoid M) (mrange (ϕ i)) (mrange (noncommPiCoprod (N := N) ϕ hcomm))
Tactic: refine iSup_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ Commute m ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) h)
have dsimp : Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) sorry)
Tactic: dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
⊢ Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯)
have hom : ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
hom : ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)
⊢ Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯)
have unit : Commute m 1
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i : (a : N i) → M) x)
h : (i : ι) → N i
hom : ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)
unit : Commute m 1
⊢ Commute m (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (h i)) ⋯)
have base : ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → Commute m ((ϕ x : (a : N x) → M) (h x))
Tactic: apply Finset.noncommProd_induction
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
    (⨆ (i : ι), (ϕ i).range)
have a : LE.le.{u_1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i)) (⨆ (i : ι), (ϕ i).range)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
a :
  LE.le.{u_1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i)) (⨆ (i : ι), (ϕ i).range)
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
    (⨆ (i : ι), (ϕ i).range)
have a₁ : LE.le.{u_1} (α := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range)
    ((noncommPiCoprod (N := H) ϕ hcomm : (a : (i : ι) → H i) → G) f : G)
have a : ∀ (c : ι),
  Membership.mem (γ := Finset ι) Finset.univ c →
    Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ c : (a : H c) → G) (f c) : G)
Tactic: refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ i : (a : H i) → G) (f i) : G)
have a : Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)
Tactic: apply Subgroup.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
a : Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ i : (a : H i) → G) (f i) : G)
have a₁ : Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((ϕ i : (a : H i) → G) (f i) : G)
Tactic: apply Subgroup.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
a : Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)
a₁ :
  Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((ϕ i : (a : H i) → G) (f i) : G)
⊢ Membership.mem.{u_1, u_1} (α := G) (γ := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((ϕ i : (a : H i) → G) (f i) : G)
have a₂ : Subgroup G
Tactic: apply Subgroup.mem_sSup_of_mem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
w : ι
⊢ Membership.mem (γ := Set (Subgroup G)) (Set.range fun (i : ι) ↦ (ϕ i).range) ((fun (i : ι) ↦ (ϕ i).range) i)
have h : Eq.{u_1 + 1} (α := Subgroup G) ((fun (i : ι) ↦ (ϕ i).range) i) ((fun (i : ι) ↦ (ϕ i).range) i)
Tactic: use i
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
this : DecidableEq ι := Classical.decEq ι
⊢ LE.le.{u_1} (α := Subgroup G) (⨆ (i : ι), (ϕ i).range) ((noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i))
have a : ∀ (i : ι), (ϕ i).range ≤ (noncommPiCoprod (N := H) ϕ hcomm).range (G := (i : ι) → H i)
Tactic: refine iSup_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Type u_3
inst_1 : (i : ι) → Group (H i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (H i) G
inst_2 : Fintype ι
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : H i) (y : H j), Commute.{u_1} (S := G) ((ϕ i : (a : H i) → G) x : G) ((ϕ j : (a : H j) → G) y : G)
hind : iSupIndep.{u_2 + 1, u_1} (α := Subgroup G) fun (i : ι) ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective.{u_3 + 1, u_1 + 1} (α := H i) (β := G) (⇑(ϕ i) : (a : H i) → G)
⊢ Function.Injective (α := (i : ι) → H i) (β := G) (⇑(noncommPiCoprod (N := H) ϕ hcomm) : (a : (i : ι) → H i) → G)
have apply : Eq (α := Subgroup ((i : ι) → H i)) (noncommPiCoprod (N := H) ϕ hcomm).ker ⊥
Tactic: apply (MonoidHom.ker_eq_bot_iff _).mp