[GOAL]
X : Type u_1
x : X
⊢ AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x) =
    ↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)
[PROOFSTEP]
ext
[GOAL]
case h1
X : Type u_1
x : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x)) 1 =
    ↑(↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)) 1
[PROOFSTEP]
simp only [AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, toFreeAbelianGroup,
  Finsupp.liftAddHom_apply_single]
[GOAL]
X : Type u_1
⊢ AddMonoidHom.comp toFinsupp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
[PROOFSTEP]
ext x y
[GOAL]
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.id (X →₀ ℤ)) (singleAddHom x)) 1) y
[PROOFSTEP]
simp only [AddMonoidHom.id_comp]
[GOAL]
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(singleAddHom x) 1) y
[PROOFSTEP]
rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]
[GOAL]
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp toFinsupp (↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x))) 1) y =
    ↑(↑(singleAddHom x) 1) y
[PROOFSTEP]
simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, lift.of,
  AddMonoidHom.flip_apply, smulAddHom_apply, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
⊢ AddMonoidHom.comp toFreeAbelianGroup toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
[PROOFSTEP]
ext
[GOAL]
case H
X : Type u_1
x✝ : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup toFinsupp) (of x✝) = ↑(AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
[PROOFSTEP]
rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift.of, liftAddHom_apply_single, AddMonoidHom.flip_apply,
  smulAddHom_apply, one_smul, AddMonoidHom.id_apply]
[GOAL]
X✝ : Type u_1
X : Type u_2
x : FreeAbelianGroup X
⊢ ↑toFreeAbelianGroup (↑toFinsupp x) = x
[PROOFSTEP]
rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
x : X
⊢ ↑toFinsupp (of x) = single x 1
[PROOFSTEP]
simp only [toFinsupp, lift.of]
[GOAL]
X : Type u_1
f : X →₀ ℤ
⊢ ↑toFinsupp (↑toFreeAbelianGroup f) = f
[PROOFSTEP]
rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ support a ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
rw [support, Finsupp.mem_support_iff]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x ≠ 0 ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ¬x ∈ support a ↔ ↑(coeff x) a = 0
[PROOFSTEP]
rw [support, Finsupp.not_mem_support_iff]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x = 0 ↔ ↑(coeff x) a = 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
X : Type u_1
⊢ support 0 = ∅
[PROOFSTEP]
simp only [support, Finsupp.support_zero, AddMonoidHom.map_zero]
[GOAL]
X : Type u_1
x : X
⊢ support (of x) = {x}
[PROOFSTEP]
rw [support, toFinsupp_of, Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
X : Type u_1
a : FreeAbelianGroup X
⊢ support (-a) = support a
[PROOFSTEP]
simp only [support, AddMonoidHom.map_neg, Finsupp.support_neg]
[GOAL]
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
[PROOFSTEP]
ext x
[GOAL]
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ support (k • a) ↔ x ∈ support a
[PROOFSTEP]
simp only [mem_support_iff, AddMonoidHom.map_zsmul]
[GOAL]
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • ↑(coeff x) a ≠ 0 ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
simp only [h, zsmul_int_int, false_or_iff, Ne.def, mul_eq_zero]
[GOAL]
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
[PROOFSTEP]
apply support_zsmul k _ a
[GOAL]
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
X : Type u_1
a b : FreeAbelianGroup X
⊢ support (a + b) ⊆ support a ∪ support b
[PROOFSTEP]
simp only [support, AddMonoidHom.map_add]
[GOAL]
X : Type u_1
a b : FreeAbelianGroup X
⊢ (↑toFinsupp a + ↑toFinsupp b).support ⊆ (↑toFinsupp a).support ∪ (↑toFinsupp b).support
[PROOFSTEP]
apply Finsupp.support_add


[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c : β
x : α ⊕ β
⊢ swap (a • x) = a • swap x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c : β
val✝ : α
⊢ swap (a • inl val✝) = a • swap (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c val✝ : β
⊢ swap (a • inr val✝) = a • swap (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : α
⊢ (a • b) • inl val✝ = a • b • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : β
⊢ (a • b) • inr val✝ = a • b • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
⊢ a • b • x = b • a • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : α
⊢ a • b • inl val✝ = b • a • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : β
⊢ a • b • inr val✝ = b • a • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x✝ : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
x : α ⊕ β
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
val✝ : α
⊢ MulOpposite.op a • inl val✝ = a • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
val✝ : β
⊢ MulOpposite.op a • inr val✝ = a • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
a : α
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
injection h (inl a)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a : M
b✝ : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
b : β
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (inr b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x : α ⊕ β
⊢ 1 • x = x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
val✝ : α
⊢ 1 • inl val✝ = inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
val✝ : β
⊢ 1 • inr val✝ = inr val✝
[PROOFSTEP]
exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
x : α ⊕ β
⊢ (a * b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
val✝ : α
⊢ (a * b) • inl val✝ = a • b • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
val✝ : β
⊢ (a * b) • inr val✝ = a • b • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)]


[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Commensurable H H
[PROOFSTEP]
simp [Commensurable]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ Setoid.r a b ↔ Setoid.r (↑(Subgroup.equivSMul g K).toEquiv a) (↑(Subgroup.equivSMul g K).toEquiv b)
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ Setoid.r a b ↔ Setoid.r (↑(Subgroup.equivSMul g K) a) (↑(Subgroup.equivSMul g K) b)
[PROOFSTEP]
rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq', QuotientGroup.eq', Subgroup.mem_subgroupOf,
  Subgroup.mem_subgroupOf, ← MulEquiv.map_inv, ← MulEquiv.map_mul, Subgroup.equivSMul_apply_coe]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ ↑(a⁻¹ * b) ∈ H ↔ g • ↑(a⁻¹ * b) ∈ g • H
[PROOFSTEP]
exact Subgroup.smul_mem_pointwise_smul_iff.symm
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : ConjAct G
⊢ Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)
[PROOFSTEP]
rw [commensurable_conj, inv_smul_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | Commensurable (g • H) H}
hb : b✝ ∈ {g | Commensurable (g • H) H}
⊢ a✝ * b✝ ∈ {g | Commensurable (g • H) H}
[PROOFSTEP]
rw [Set.mem_setOf_eq, mul_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | Commensurable (g • H) H}
hb : b✝ ∈ {g | Commensurable (g • H) H}
⊢ Commensurable (a✝ • b✝ • H) H
[PROOFSTEP]
exact trans ((commensurable_conj _).mp hb) ha
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 ∈
    { carrier := {g | Commensurable (g • H) H},
        mul_mem' :=
          (_ :
            ∀ {a b : ConjAct G},
              a ∈ {g | Commensurable (g • H) H} →
                b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, one_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝¹ : ConjAct G
x✝ :
  x✝¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | Commensurable (g • H) H},
              mul_mem' :=
                (_ :
                  ∀ {a b : ConjAct G},
                    a ∈ {g | Commensurable (g • H) H} →
                      b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := {g | Commensurable (g • H) H},
                    mul_mem' :=
                      (_ :
                        ∀ {a b : ConjAct G},
                          a ∈ {g | Commensurable (g • H) H} →
                            b ∈ {g | Commensurable (g • H) H} →
                              a * b ∈ {g | Commensurable (g • H) H}) }.carrier) }.toSubsemigroup.carrier
⊢ x✝¹⁻¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | Commensurable (g • H) H},
              mul_mem' :=
                (_ :
                  ∀ {a b : ConjAct G},
                    a ∈ {g | Commensurable (g • H) H} →
                      b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := {g | Commensurable (g • H) H},
                    mul_mem' :=
                      (_ :
                        ∀ {a b : ConjAct G},
                          a ∈ {g | Commensurable (g • H) H} →
                            b ∈ {g | Commensurable (g • H) H} →
                              a * b ∈ {g | Commensurable (g • H) H}) }.carrier) }.toSubsemigroup.carrier
[PROOFSTEP]
rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]


[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : Finset.noncommProd s f comm = 1
⊢ ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
classical
revert heq1
induction' s using Finset.induction_on with i s hnmem ih
· simp
· have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
  simp only [Finset.forall_mem_insert] at hmem
  have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i :=
    by
    refine' Subgroup.noncommProd_mem _ _ _
    intro x hx
    have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
    exact this (hmem.2 x hx)
  intro heq1
  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1
  have hnmem' : i ∉ (s : Set ι) := by simpa
  obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
    Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnmem') hmem.1 hmem_bsupr heq1
  intro i h
  simp only [Finset.mem_insert] at h
  rcases h with (rfl | h)
  · exact heq1i
  · refine' ih hcomm hmem.2 heq1S _ h
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : Finset.noncommProd s f comm = 1
⊢ ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
revert heq1
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
induction' s using Finset.induction_on with i s hnmem ih
[GOAL]
case empty
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s → f x ∈ K x
comm : Set.Pairwise ↑∅ fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ ∅ → f x ∈ K x
⊢ Finset.noncommProd ∅ f comm = 1 → ∀ (i : ι), i ∈ ∅ → f i = 1
[PROOFSTEP]
simp
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ insert i s → f x ∈ K x
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ insert i s → f x ∈ K x
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
simp only [Finset.forall_mem_insert] at hmem
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i :=
  by
  refine' Subgroup.noncommProd_mem _ _ _
  intro x hx
  have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
  exact this (hmem.2 x hx)
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
refine' Subgroup.noncommProd_mem _ _ _
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ ∀ (c : ι), c ∈ s → f c ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
intro x hx
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
x : ι
hx : x ∈ s
⊢ f x ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
x : ι
hx : x ∈ s
this : K x ≤ ⨆ (i : ι) (_ : i ∈ ↑s), K i
⊢ f x ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
exact this (hmem.2 x hx)
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
intro heq1
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : Finset.noncommProd (insert i s) f comm = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hnmem' : i ∉ (s : Set ι) := by simpa
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
⊢ ¬i ∈ ↑s
[PROOFSTEP]
simpa
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
  Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnmem') hmem.1 hmem_bsupr heq1
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
heq1i : f i = 1
heq1S : Finset.noncommProd s f hcomm = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
intro i h
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i ∈ insert i✝ s
⊢ f i = 1
[PROOFSTEP]
simp only [Finset.mem_insert] at h
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i = i✝ ∨ i ∈ s
⊢ f i = 1
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case insert.intro.inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
s : Finset ι
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
hnmem : ¬i ∈ s
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
heq1i : f i = 1
⊢ f i = 1
[PROOFSTEP]
exact heq1i
[GOAL]
case insert.intro.inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1
[PROOFSTEP]
refine' ih hcomm hmem.2 heq1S _ h
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ (fun f =>
        Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
          (_ :
            ∀ (i : ι), i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))))
      1 =
    1
[PROOFSTEP]
apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (x : ι), x ∈ Finset.univ → ↑(ϕ x) (OfNat.ofNat 1 x) = 1
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ OneHom.toFun
      {
        toFun := fun f =>
          Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
            (_ :
              ∀ (i : ι),
                i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
        map_one' :=
          (_ :
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                (_ :
                  ∀ (i : ι),
                    i ∈ ↑Finset.univ →
                      ∀ (j : ι),
                        j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
              1) }
      (f * g) =
    OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        f *
      OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        g
[PROOFSTEP]
classical
simp only
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 _ _
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ OneHom.toFun
      {
        toFun := fun f =>
          Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
            (_ :
              ∀ (i : ι),
                i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
        map_one' :=
          (_ :
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                (_ :
                  ∀ (i : ι),
                    i ∈ ↑Finset.univ →
                      ∀ (j : ι),
                        j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
              1) }
      (f * g) =
    OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        f *
      OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        g
[PROOFSTEP]
simp only
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) ((f * g) x))
      (_ :
        ∀ (x : ι),
          x ∈ ↑Finset.univ →
            ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) ((f * g) a)) (↑(ϕ b) ((f * g) b))) x y) =
    Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) (f x))
        (_ :
          ∀ (x : ι),
            x ∈ ↑Finset.univ →
              ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) (f a)) (↑(ϕ b) (f b))) x y) *
      Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) (g x))
        (_ :
          ∀ (x : ι),
            x ∈ ↑Finset.univ →
              ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) (g a)) (↑(ϕ b) (g b))) x y)
[PROOFSTEP]
convert @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
[GOAL]
case h.e'_2.h₂
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ↑(ϕ x✝) ((f * g) x✝) = ((fun i => ↑(ϕ i) (f i)) * fun i => ↑(ϕ i) (g i)) x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
case convert_4
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ Set.Pairwise ↑Finset.univ fun x y => Commute ((fun i => ↑(ϕ i) (g i)) x) ((fun i => ↑(ϕ i) (f i)) y)
[PROOFSTEP]
rintro i - j - h
[GOAL]
case convert_4
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
i j : ι
h : i ≠ j
⊢ Commute ((fun i => ↑(ϕ i) (g i)) i) ((fun i => ↑(ϕ i) (f i)) j)
[PROOFSTEP]
exact hcomm h _ _
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = ↑(ϕ i) y
[PROOFSTEP]
change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _) = ϕ i y
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ Finset.noncommProd Finset.univ (fun j => ↑(ϕ j) (Pi.mulSingle i y j))
      (_ :
        ∀ (x : ι),
          x ∈ ↑Finset.univ →
            ∀ (x_2 : ι),
              x_2 ∈ ↑Finset.univ → x ≠ x_2 → Commute (↑(ϕ x) (Pi.mulSingle i y x)) (↑(ϕ x_2) (Pi.mulSingle i y x_2))) =
    ↑(ϕ i) y
[PROOFSTEP]
simp (config := { singlePass := true }) only [← Finset.insert_erase (Finset.mem_univ i)]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ Finset.noncommProd (insert i (Finset.erase Finset.univ i)) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
      (_ :
        ∀ (x : ι),
          x ∈ ↑(insert i (Finset.erase Finset.univ i)) →
            ∀ (y_1 : ι),
              y_1 ∈ ↑(insert i (Finset.erase Finset.univ i)) →
                x ≠ y_1 → (fun a b => Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) x y_1) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ (Finset.not_mem_erase i _)]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) (Pi.mulSingle i y i) *
      Finset.noncommProd (Finset.erase Finset.univ i) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
        (_ :
          Set.Pairwise ↑(Finset.erase Finset.univ i) fun a b =>
            Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Pi.mulSingle_eq_same]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y *
      Finset.noncommProd (Finset.erase Finset.univ i) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
        (_ :
          Set.Pairwise ↑(Finset.erase Finset.univ i) fun a b =>
            Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Finset.noncommProd_eq_pow_card]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y * ?m ^ Finset.card (Finset.erase Finset.univ i) = ↑(ϕ i) y
[PROOFSTEP]
rw [one_pow]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y * 1 = ↑(ϕ i) y
[PROOFSTEP]
exact mul_one _
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ∀ (x : ι), x ∈ Finset.erase Finset.univ i → ↑(ϕ x) (Pi.mulSingle i y x) = 1
[PROOFSTEP]
intro j hj
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
j : ι
hj : j ∈ Finset.erase Finset.univ i
⊢ ↑(ϕ j) (Pi.mulSingle i y j) = 1
[PROOFSTEP]
simp only [Finset.mem_erase] at hj
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
j : ι
hj : j ≠ i ∧ j ∈ Finset.univ
⊢ ↑(ϕ j) (Pi.mulSingle i y j) = 1
[PROOFSTEP]
simp [hj]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ✝ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ✝ i) x) (↑(ϕ✝ j) y)
f g : (i : ι) → N i
ϕ : { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y) }
⊢ (fun f =>
        { val := fun i => comp f (single N i),
          property :=
            (_ : ∀ (i j : ι), i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
      ((fun ϕ => noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
        ϕ) =
    ϕ
[PROOFSTEP]
ext
[GOAL]
case a.h.h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ✝ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ✝ i) x) (↑(ϕ✝ j) y)
f g : (i : ι) → N i
ϕ : { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y) }
x✝¹ : ι
x✝ : N x✝¹
⊢ ↑(↑((fun f =>
                { val := fun i => comp f (single N i),
                  property :=
                    (_ :
                      ∀ (i j : ι),
                        i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
              ((fun ϕ =>
                  noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
                ϕ))
          x✝¹)
      x✝ =
    ↑(↑ϕ x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → N i
f : ((i : ι) → N i) →* M
i : ι
x : N i
⊢ ↑((fun ϕ => noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
          ((fun f =>
              { val := fun i => comp f (single N i),
                property :=
                  (_ :
                    ∀ (i j : ι),
                      i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
            f))
      (Pi.mulSingle i x) =
    ↑f (Pi.mulSingle i x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
classical
apply le_antisymm
· rintro x ⟨f, rfl⟩
  refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
  apply Submonoid.mem_sSup_of_mem
  · use i
  simp
· refine' iSup_le _
  rintro i x ⟨y, rfl⟩
  refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
rintro x ⟨f, rfl⟩
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
apply Submonoid.mem_sSup_of_mem
[GOAL]
case a.intro.hs
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => mrange (ϕ i)
[PROOFSTEP]
use i
[GOAL]
case a.intro.a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ (fun i => mrange (ϕ i)) i
[PROOFSTEP]
simp
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ⨆ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
rintro i x ⟨y, rfl⟩
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y ∈ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
classical
apply le_antisymm
· rintro x ⟨f, rfl⟩
  refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm _ _ h _ _) ?_
  intro i _hi
  apply Subgroup.mem_sSup_of_mem
  · use i
  simp
· refine' iSup_le _
  rintro i x ⟨y, rfl⟩
  refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
rintro x ⟨f, rfl⟩
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm _ _ h _ _) ?_
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
⊢ ∀ (c : ι), c ∈ Finset.univ → ↑(ϕ c) (f c) ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
intro i _hi
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
apply Subgroup.mem_sSup_of_mem
[GOAL]
case a.intro.hs
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => range (ϕ i)
[PROOFSTEP]
use i
[GOAL]
case a.intro.a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ (fun i => range (ϕ i)) i
[PROOFSTEP]
simp
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ ⨆ (i : ι), range (ϕ i) ≤ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ ∀ (i : ι), range (ϕ i) ≤ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
rintro i x ⟨y, rfl⟩
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
i : ι
y : H i
⊢ ↑(ϕ i) y ∈ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
classical
apply (MonoidHom.ker_eq_bot_iff _).mp
apply eq_bot_iff.mpr
intro f heq1
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
  Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _) _ hind (by simp) heq1
ext i
apply hinj
simp [this i (Finset.mem_univ i)]
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
apply (MonoidHom.ker_eq_bot_iff _).mp
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) = ⊥
[PROOFSTEP]
apply eq_bot_iff.mpr
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) ≤ ⊥
[PROOFSTEP]
intro f heq1
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ f ∈ ⊥
[PROOFSTEP]
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
  Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _) _ hind (by simp) heq1
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ ∀ (x : ι), x ∈ Finset.univ → ↑(ϕ x) (f x) ∈ range (ϕ x)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
⊢ f ∈ ⊥
[PROOFSTEP]
ext i
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ f i = OfNat.ofNat 1 i
[PROOFSTEP]
apply hinj
[GOAL]
case h.a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ ↑(ϕ i) (f i) = ↑(ϕ i) (OfNat.ofNat 1 i)
[PROOFSTEP]
simp [this i (Finset.mem_univ i)]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
classical
rintro i
rw [disjoint_iff_inf_le]
rintro f ⟨hxi, hxp⟩
dsimp at hxi hxp
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
rotate_left
· intro _ _ hj
  apply hcomm
  exact hj ∘ Subtype.ext
cases' hxp with g hgf
cases' hxi with g' hg'f
have hxi : orderOf f ∣ Fintype.card (H i) := by
  rw [← hg'f]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) :=
  by
  rw [← hgf, ← Fintype.card_pi]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
change f = 1
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  -- porting note: ouch, had to replace an ugly `convert`
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
use c
rw [← hc]
symm
rw [← Nat.coprime_iff_gcd_eq_one]
apply Nat.coprime_prod_left
intro j _
apply hcoprime
exact j.2
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
rintro i
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ Disjoint ((fun i => range (ϕ i)) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ (fun i => range (ϕ i)) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j ≤ ⊥
[PROOFSTEP]
rintro f ⟨hxi, hxp⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ ↑((fun i => range (ϕ i)) i).toSubmonoid
hxp : f ∈ ↑(⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j).toSubmonoid
⊢ f ∈ ⊥
[PROOFSTEP]
dsimp at hxi hxp
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (j : ι) (_ : ¬j = i), range (ϕ j))
⊢ f ∈ ⊥
[PROOFSTEP]
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp : f ∈ ↑(range (noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm))
⊢ f ∈ ⊥
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
[PROOFSTEP]
intro _ _ hj
[GOAL]
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute (↑(ϕ ↑i✝) x) (↑(ϕ ↑j✝) y)
[PROOFSTEP]
apply hcomm
[GOAL]
case intro.intro.hcomm.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝
[PROOFSTEP]
exact hj ∘ Subtype.ext
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp :
  f ∈
    ↑(range
        (noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y))))
⊢ f ∈ ⊥
[PROOFSTEP]
cases' hxp with g hgf
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
⊢ f ∈ ⊥
[PROOFSTEP]
cases' hxi with g' hg'f
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ f ∈ ⊥
[PROOFSTEP]
have hxi : orderOf f ∣ Fintype.card (H i) := by
  rw [← hg'f]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf f ∣ Fintype.card (H i)
[PROOFSTEP]
rw [← hg'f]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf (↑(ϕ i) g') ∣ Fintype.card (H i)
[PROOFSTEP]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ f ∈ ⊥
[PROOFSTEP]
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) :=
  by
  rw [← hgf, ← Fintype.card_pi]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
[PROOFSTEP]
rw [← hgf, ← Fintype.card_pi]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf
      (↑(noncommPiCoprod (fun x => ϕ ↑x)
            (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
        g) ∣
    Fintype.card ((a : { j // j ≠ i }) → H ↑a)
[PROOFSTEP]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ f ∈ ⊥
[PROOFSTEP]
change f = 1
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ f = 1
[PROOFSTEP]
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  -- porting note: ouch, had to replace an ugly `convert`
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1
[PROOFSTEP]
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ orderOf f ∣ 1
[PROOFSTEP]
use c
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c
[PROOFSTEP]
rw [← hc]
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
symm
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = 1
[PROOFSTEP]
rw [← Nat.coprime_iff_gcd_eq_one]
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.coprime (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
apply Nat.coprime_prod_left
[GOAL]
case h.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (i_1 : { j // j ≠ i }), i_1 ∈ Finset.univ → Nat.coprime (Fintype.card (H ↑i_1)) (Fintype.card (H i))
[PROOFSTEP]
intro j _
[GOAL]
case h.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ Nat.coprime (Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
apply hcoprime
[GOAL]
case h.a.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ ↑j ≠ i
[PROOFSTEP]
exact j.2
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
⊢ ∀ (x : { x // x ∈ H i }) (y : { x // x ∈ H j }), Commute (↑(Subgroup.subtype (H i)) x) (↑(Subgroup.subtype (H j)) y)
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩
[GOAL]
case mk.mk
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (↑(Subgroup.subtype (H i)) { val := x, property := hx })
    (↑(Subgroup.subtype (H j)) { val := y, property := hy })
[PROOFSTEP]
exact hcomm i j hne x y hx hy
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i : ι
y : { x // x ∈ H i }
⊢ ↑(noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
[PROOFSTEP]
apply MonoidHom.noncommPiCoprod_mulSingle
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
⊢ MonoidHom.range (noncommPiCoprod hcomm) = ⨆ (i : ι), H i
[PROOFSTEP]
simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ Function.Injective ↑(noncommPiCoprod hcomm)
[PROOFSTEP]
apply MonoidHom.injective_noncommPiCoprod_of_independent
[GOAL]
case hind
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ CompleteLattice.Independent fun i => MonoidHom.range (Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
simpa using hind
[GOAL]
case hinj
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ ∀ (i : ι), Function.Injective ↑(Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
intro i
[GOAL]
case hinj
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
i : ι
⊢ Function.Injective ↑(Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
exact Subtype.coe_injective
[GOAL]
G : Type u_1
inst✝² : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype { x // x ∈ H i }
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card { x // x ∈ H i }) (Fintype.card { x // x ∈ H j })
⊢ CompleteLattice.Independent H
[PROOFSTEP]
simpa using
  MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype) (commute_subtype_of_commute hcomm) hcoprime


[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
fst✝ : ι
snd✝ : α fst✝
⊢ (a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, smul_assoc]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ a • b • x = b • a • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
fst✝ : ι
snd✝ : α fst✝
⊢ a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x✝ : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
x : (i : ι) × α i
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
fst✝ : ι
snd✝ : α fst✝
⊢ MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, op_smul_eq_smul]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
x : (i : ι) × α i
⊢ 1 • x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
fst✝ : ι
snd✝ : α fst✝
⊢ 1 • { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, one_smul]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
x : (i : ι) × α i
⊢ (a * b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
fst✝ : ι
snd✝ : α fst✝
⊢ (a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, mul_smul]