[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ Linear k (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ AddCommGroup (CoeSort.coe V)
[PROOFSTEP]
change AddCommGroup ((forget₂ (Rep k G) (ModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ AddCommGroup ↑((forget₂ (Rep k G) (ModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Module k (CoeSort.coe V)
[PROOFSTEP]
change Module k ((forget₂ (Rep k G) (ModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Module k ↑((forget₂ (Rep k G) (ModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : CoeSort.coe A
⊢ ↑(↑(ρ A) g⁻¹ * ↑(ρ A) g) x = x
[PROOFSTEP]
rw [← map_mul, inv_mul_self, map_one, LinearMap.one_apply]
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : CoeSort.coe A
⊢ ↑(↑(ρ A) g * ↑(ρ A) g⁻¹) x = x
[PROOFSTEP]
rw [← map_mul, mul_inv_self, map_one, LinearMap.one_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) (MonCat.of G)
g : G
x : X.V
⊢ ↑(↑(ρ ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) (Finsupp.single x 1) =
    Finsupp.single (↑X.ρ g x) 1
[PROOFSTEP]
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) (MonCat.of G)
g : G
x : X.V
r : k
⊢ ↑(↑(ρ ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) (Finsupp.single x r) =
    Finsupp.single (↑X.ρ g x) r
[PROOFSTEP]
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ (inv (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y)).hom =
    ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V))
[PROOFSTEP]
rw [← Action.forget_map, Functor.map_inv]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ inv
      ((Action.forget (ModuleCat k) (MonCat.of G)).map
        (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y)) =
    ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V))
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ (Action.forget (ModuleCat k) (MonCat.of G)).map (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y) ≫
      ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) =
    𝟙
      ((Action.forget (ModuleCat k) (MonCat.of G)).obj
        (MonoidalCategory.tensorObj ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)
          ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj Y)))
[PROOFSTEP]
exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply (finsuppTensorFinsupp' k X.V Y.V) x
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
⊢ (↑(ofMulAction k G G).ρ g ≫ ↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) =
    (↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) ≫ ↑A.ρ g
[PROOFSTEP]
refine'
  Finsupp.lhom_ext' fun y =>
    LinearMap.ext_ring
      _
        /- Porting note: rest of broken proof was
            simpa only [LinearMap.comp_apply, ModuleCat.comp_def, Finsupp.lsingle_apply, Finsupp.lift_apply,
              Action_ρ_eq_ρ, of_ρ_apply, Representation.ofMulAction_single, Finsupp.sum_single_index,
              zero_smul, one_smul, smul_eq_mul, A.ρ.map_mul] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(LinearMap.comp (↑(ofMulAction k G G).ρ g ≫ ↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x)
          (Finsupp.lsingle y))
      1 =
    ↑(LinearMap.comp ((↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) ≫ ↑A.ρ g)
          (Finsupp.lsingle y))
      1
[PROOFSTEP]
simp only [LinearMap.comp_apply, ModuleCat.comp_def, Finsupp.lsingle_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) x) (↑(↑(ofMulAction k G G).ρ g) (Finsupp.single y 1)) =
    ↑(↑A.ρ g) (↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) x) (Finsupp.single y 1))
[PROOFSTEP]
erw [Finsupp.lift_apply, Finsupp.lift_apply, Representation.ofMulAction_single (G := G)]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ (Finsupp.sum (Finsupp.single (g • y) 1) fun x_1 r => r • ↑(↑(ρ A) x_1) x) =
    ↑(↑A.ρ g) (Finsupp.sum (Finsupp.single y 1) fun x_1 r => r • ↑(↑(ρ A) x_1) x)
[PROOFSTEP]
simp only [Finsupp.sum_single_index, zero_smul, one_smul, smul_eq_mul, A.ρ.map_mul, of_ρ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(↑(ρ A) g * ↑(ρ A) y) x = ↑(↑A.ρ g) (↑(↑(ρ A) y) x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
⊢ ↑(leftRegularHom A x).hom (Finsupp.single 1 1) = x
[PROOFSTEP]
rw [leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, A.ρ.map_one, LinearMap.one_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
⊢ 0 • ↑(↑(ρ A) 1) x = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
⊢ (fun x => leftRegularHom A x)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                map_add' :=
                  (_ :
                    ∀ (x y : ofMulAction k G G ⟶ A),
                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                  AddHom.toFun
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                      (r • x) =
                    AddHom.toFun
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                      (r • x)) }.toAddHom
        f) =
    f
[PROOFSTEP]
refine' Action.Hom.ext _ _ (Finsupp.lhom_ext' fun x : G => LinearMap.ext_ring _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
⊢ ↑(LinearMap.comp
          ((fun x => leftRegularHom A x)
              (AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                          AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x) =
                            AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x)) }.toAddHom
                f)).hom
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp f.hom (Finsupp.lsingle x)) 1
[PROOFSTEP]
have :
  f.hom ((ofMulAction k G G).ρ x (Finsupp.single (1 : G) (1 : k))) = A.ρ x (f.hom (Finsupp.single (1 : G) (1 : k))) :=
  LinearMap.ext_iff.1 (f.comm x)
    (Finsupp.single 1 1)
      /- Porting note: rest of broken proof was
          simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, left_regular_hom_hom,
            Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, ← this, zero_smul, of_ρ_apply,
            Representation.ofMulAction_single x (1 : G) (1 : k), smul_eq_mul, mul_one] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ ↑(LinearMap.comp
          ((fun x => leftRegularHom A x)
              (AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                          AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x) =
                            AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x)) }.toAddHom
                f)).hom
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp f.hom (Finsupp.lsingle x)) 1
[PROOFSTEP]
simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, leftRegularHom_hom]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ ↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) (↑f.hom (Finsupp.single 1 1))) (Finsupp.single x 1) =
    ↑f.hom (Finsupp.single x 1)
[PROOFSTEP]
erw [Finsupp.lift_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ (Finsupp.sum (Finsupp.single x 1) fun x r => r • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))) =
    ↑f.hom (Finsupp.single x 1)
[PROOFSTEP]
rw [Finsupp.sum_single_index, ← this, of_ρ_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 1 • ↑f.hom (↑(↑(Representation.ofMulAction k G G) x) (Finsupp.single 1 1)) = ↑f.hom (Finsupp.single x 1)
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
erw [Representation.ofMulAction_single x (1 : G) (1 : k)]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 1 • ↑f.hom (Finsupp.single (x • 1) 1) = ↑f.hom (Finsupp.single x 1)
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
simp only [one_smul, smul_eq_mul, mul_one]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : G
⊢ ↑(↑(LinearEquiv.symm (leftRegularHomEquiv A)) x).hom (Finsupp.single g 1) = ↑(↑(ρ A) g) x
[PROOFSTEP]
rw [leftRegularHomEquiv_symm_apply, leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : G
⊢ 0 • ↑(↑(ρ A) g) x = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑(↑(↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).ρ g ≫
              ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom))
          x)
      y =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) Y).ρ g)
          x)
      y
[PROOFSTEP]
show f.hom (X.ρ g _) = _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑f.hom (↑(↑(ρ X) g) (↑(LinearMap.comp x (↑(ρ A) g⁻¹)) y)) =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) Y).ρ g)
          x)
      y
[PROOFSTEP]
simp only [hom_comm_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑(↑(ρ Y) g) (↑f.hom (↑(LinearMap.comp x (↑(ρ A) g⁻¹)) y)) =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑(of (Representation.linHom (ρ A) (ρ Y))).ρ g)
          x)
      y
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A x✝ : Rep k G
⊢ { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
          map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        x✝)
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A x✝¹ : Rep k G
x✝ :
  ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        x✝¹).V
⊢ ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                map := fun {X Y} f =>
                  Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
            (𝟙 x✝¹)).hom
      x✝ =
    ↑(𝟙
            ({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
              x✝¹)).hom
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
          map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
        x✝¹ ≫
      { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X✝ Y✝ Z✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ :
  ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        X✝).V
⊢ ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                map := fun {X Y} f =>
                  Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
            (x✝² ≫ x✝¹)).hom
      x✝ =
    ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
              x✝² ≫
            { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
              x✝¹).hom
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
⊢ ↑B.ρ g ≫ LinearMap.flip (TensorProduct.curry f.hom) =
    LinearMap.flip (TensorProduct.curry f.hom) ≫ ↑((Rep.ihom A).obj C).ρ g
[PROOFSTEP]
refine' LinearMap.ext fun x => LinearMap.ext fun y => _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑(↑(↑B.ρ g ≫ LinearMap.flip (TensorProduct.curry f.hom)) x) y =
    ↑(↑(LinearMap.flip (TensorProduct.curry f.hom) ≫ ↑((Rep.ihom A).obj C).ρ g) x) y
[PROOFSTEP]
change f.hom (_ ⊗ₜ[k] _) = C.ρ g (f.hom (_ ⊗ₜ[k] _))
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) = ↑(↑(ρ C) g) (↑f.hom (↑(↑(ρ A) g⁻¹) y ⊗ₜ[k] x))
[PROOFSTEP]
rw [← hom_comm_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) = ↑f.hom (↑(↑(ρ (A ⊗ B)) g) (↑(↑(ρ A) g⁻¹) y ⊗ₜ[k] x))
[PROOFSTEP]
change _ = f.hom ((A.ρ g * A.ρ g⁻¹) y ⊗ₜ[k] _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) =
    ↑f.hom
      (↑(↑(ρ A) g * ↑(ρ A) g⁻¹) y ⊗ₜ[k]
        ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).map
              g)
          (↑(↑(ρ A) g⁻¹) y, x).snd)
[PROOFSTEP]
simp only [← map_mul, mul_inv_self, map_one]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) =
    ↑f.hom
      (↑1 y ⊗ₜ[k]
        ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).map
              g)
          x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(A ⊗ B).ρ g ≫ ↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))
      (x ⊗ₜ[k] y) =
    ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom) ≫ ↑C.ρ g) (x ⊗ₜ[k] y)
[PROOFSTEP]
change
  TensorProduct.uncurry k _ _ _ f.hom.flip (A.ρ g x ⊗ₜ[k] B.ρ g y) =
    C.ρ g (TensorProduct.uncurry k _ _ _ f.hom.flip (x ⊗ₜ[k] y))
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))
      (↑(↑(ρ A) g) x ⊗ₜ[k] ↑(↑(ρ B) g) y) =
    ↑(↑(ρ C) g)
      (↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)) (x ⊗ₜ[k] y))
[PROOFSTEP]
rw [TensorProduct.uncurry_apply, LinearMap.flip_apply, hom_comm_apply, Rep.ihom_obj_ρ_apply, LinearMap.comp_apply,
  LinearMap.comp_apply, ρ_inv_self_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(ρ C) g) (↑(↑f.hom y) x) =
    ↑(↑(ρ C) g)
      (↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)) (x ⊗ₜ[k] y))
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
⊢ (fun f => Hom.mk (LinearMap.flip (TensorProduct.curry f.hom)))
      ((fun f => Hom.mk (↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
x✝ : ↑B.V
⊢ ↑((fun f => Hom.mk (LinearMap.flip (TensorProduct.curry f.hom)))
            ((fun f =>
                Hom.mk (↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)))
              f)).hom
      x✝ =
    ↑f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C A B : Rep k G
⊢ (NatTrans.app (ihom.ev A) B).hom =
    ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B))
      (LinearMap.flip LinearMap.id)
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B).V
⊢ ↑(NatTrans.app (ihom.ev A) B).hom x✝ =
    ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B))
          (LinearMap.flip LinearMap.id))
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ SymmetricCategory (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ MonoidalPreadditive (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ MonoidalLinear k (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (↑f x)
[PROOFSTEP]
apply MonoidAlgebra.induction_on r
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (g : G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (↑(MonoidAlgebra.of k G) g)) x) =
      ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (↑(MonoidAlgebra.of k G) g)) (↑f x)
[PROOFSTEP]
intro g
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g : G
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (↑(MonoidAlgebra.of k G) g)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (↑(MonoidAlgebra.of k G) g)) (↑f x)
[PROOFSTEP]
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g : G
⊢ ↑f (↑(↑ρ g) x) = ↑(↑σ g) (↑f x)
[PROOFSTEP]
exact LinearMap.congr_fun (w g) x
[GOAL]
case hadd
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (f_1 g : MonoidAlgebra k G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (↑f x) →
      ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x) →
        ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (f_1 + g)) x) =
          ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (f_1 + g)) (↑f x)
[PROOFSTEP]
intro g h gw hw
[GOAL]
case hadd
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g h : MonoidAlgebra k G
gw : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x)
hw : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) h) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) h) (↑f x)
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (g + h)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (g + h)) (↑f x)
[PROOFSTEP]
simp only [map_add, add_left_inj, LinearMap.add_apply, hw, gw]
[GOAL]
case hsmul
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (r : k) (f_1 : MonoidAlgebra k G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (↑f x) →
      ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • f_1)) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • f_1)) (↑f x)
[PROOFSTEP]
intro r g w
[GOAL]
case hsmul
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w✝ : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r✝ : MonoidAlgebra k G
x : V
r : k
g : MonoidAlgebra k G
w : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x)
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • g)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • g)) (↑f x)
[PROOFSTEP]
simp only [AlgHom.map_smul, w, RingHom.id_apply, LinearMap.smul_apply, LinearMap.map_smulₛₗ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat (MonoidAlgebra k G)
f : X✝ ⟶ Y✝
g : ↑(MonCat.of G)
⊢ ↑((fun M => of (Representation.ofModule ↑M)) X✝).ρ g ≫
      { toAddHom := f.toAddHom,
        map_smul' :=
          (_ :
            ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
              ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } =
    { toAddHom := f.toAddHom,
        map_smul' :=
          (_ :
            ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
              ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } ≫
      ↑((fun M => of (Representation.ofModule ↑M)) Y✝).ρ g
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat (MonoidAlgebra k G)
f : X✝ ⟶ Y✝
g : ↑(MonCat.of G)
x✝ : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V
⊢ ↑(↑((fun M => of (Representation.ofModule ↑M)) X✝).ρ g ≫
          { toAddHom := f.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
                  ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) })
      x✝ =
    ↑({ toAddHom := f.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
                  ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } ≫
          ↑((fun M => of (Representation.ofModule ↑M)) Y✝).ρ g)
      x✝
[PROOFSTEP]
apply f.map_smul
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
⊢ ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M
[PROOFSTEP]
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
⊢ ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (Representation.ofModule ↑M))) ≃+ ↑M
[PROOFSTEP]
refine' (Representation.ofModule M).asModuleEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V)
[PROOFSTEP]
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ CoeSort.coe V ≃+
    RestrictScalars k (MonoidAlgebra k G) ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))
[PROOFSTEP]
refine' V.ρ.asModuleEquiv.symm.trans _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Representation.asModule (ρ V) ≃+
    RestrictScalars k (MonoidAlgebra k G) ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))
[PROOFSTEP]
exact (RestrictScalars.addEquiv _ _ _).symm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id (MonoidAlgebra k G)) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp [counitIsoAddEquiv]
  /- Porting note: rest of broken proof was `simp`. -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
      (r • x) =
    r •
      ↑↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
              (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
rw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M)
      (↑(Representation.asModuleEquiv (Representation.ofModule ↑M)) (r • x)) =
    r •
      ↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
erw [Representation.ofModule_asAlgebraHom_apply_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => ↑M) x)))
      (r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M) x) =
    r •
      ↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
exact AddEquiv.symm_apply_apply _ _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑unitIsoAddEquiv (AddHom.toFun (↑(ρ V) g).toAddHom x) =
    AddHom.toFun (↑(ρ (ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V))) g).toAddHom (↑unitIsoAddEquiv x)
[PROOFSTEP]
dsimp [unitIsoAddEquiv, ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
  /- Porting note: rest of broken proof was
    simp only [AddEquiv.apply_eq_iff_eq, AddEquiv.apply_symm_apply,
      Representation.asModuleEquiv_symm_map_rho, Representation.ofModule_asModule_act] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
          (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
      (↑(↑(ρ V) g) x) =
    AddHom.toFun
      (↑(Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))) g).toAddHom
      (↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x)
[PROOFSTEP]
erw [Representation.asModuleEquiv_symm_map_rho]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑(MonoidAlgebra.of k G) g • ↑(AddEquiv.symm (Representation.asModuleEquiv (ρ V))) x =
    AddHom.toFun
      (↑(Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))) g).toAddHom
      (↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : CoeSort.coe V),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : CoeSort.coe V),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp [unitIsoAddEquiv]
  /- Porting note: rest of broken proof was
            simp only [Representation.asModuleEquiv_symm_map_smul,
              RestrictScalars.addEquiv_symm_map_algebraMap_smul] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ ↑↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
      (r • x) =
    r •
      ↑↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
              (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x
[PROOFSTEP]
rw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply, Representation.asModuleEquiv_symm_map_smul,
  RestrictScalars.addEquiv_symm_map_algebraMap_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ r •
      ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V))))
        (↑(AddEquiv.symm (Representation.asModuleEquiv (ρ V))) x) =
    r •
      ↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : ↑(MonCat.of G)
⊢ ↑V.ρ g ≫
      (LinearEquiv.toModuleIso'
          (let src := unitIsoAddEquiv;
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : CoeSort.coe V),
                          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (r : k) (x : ↑V.V),
                      AddHom.toFun
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : CoeSort.coe V),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                          (r • x) =
                        ↑(RingHom.id k) r •
                          AddHom.toFun
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : CoeSort.coe V),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                            x) },
            invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
            right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom =
    (LinearEquiv.toModuleIso'
          (let src := unitIsoAddEquiv;
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : CoeSort.coe V),
                          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (r : k) (x : ↑V.V),
                      AddHom.toFun
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : CoeSort.coe V),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                          (r • x) =
                        ↑(RingHom.id k) r •
                          AddHom.toFun
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : CoeSort.coe V),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                            x) },
            invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
            right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom ≫
      ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V).ρ g
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : ↑(MonCat.of G)
x✝ : ↑V.V
⊢ ↑(↑V.ρ g ≫
          (LinearEquiv.toModuleIso'
              (let src := unitIsoAddEquiv;
              {
                toLinearMap :=
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : CoeSort.coe V),
                              Equiv.toFun src.toEquiv (x + y) =
                                Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ↑V.V),
                          AddHom.toFun
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : CoeSort.coe V),
                                      Equiv.toFun src.toEquiv (x + y) =
                                        Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                              (r • x) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : CoeSort.coe V),
                                        Equiv.toFun src.toEquiv (x + y) =
                                          Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                                x) },
                invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
                right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom)
      x✝ =
    ↑((LinearEquiv.toModuleIso'
              (let src := unitIsoAddEquiv;
              {
                toLinearMap :=
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : CoeSort.coe V),
                              Equiv.toFun src.toEquiv (x + y) =
                                Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ↑V.V),
                          AddHom.toFun
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : CoeSort.coe V),
                                      Equiv.toFun src.toEquiv (x + y) =
                                        Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                              (r • x) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : CoeSort.coe V),
                                        Equiv.toFun src.toEquiv (x + y) =
                                          Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                                x) },
                invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
                right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom ≫
          ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V).ρ g)
      x✝
[PROOFSTEP]
apply unit_iso_comm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ∀ {X Y : Rep k G} (f : X ⟶ Y),
    (𝟭 (Rep k G)).map f ≫ ((fun V => unitIso V) Y).hom =
      ((fun V => unitIso V) X).hom ≫ (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).map f
[PROOFSTEP]
aesop_cat
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ∀ {X Y : ModuleCat (MonoidAlgebra k G)} (f : X ⟶ Y),
    (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).map f ≫ ((fun M => counitIso M) Y).hom =
      ((fun M => counitIso M) X).hom ≫ (𝟭 (ModuleCat (MonoidAlgebra k G))).map f
[PROOFSTEP]
aesop_cat


[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let a := I.smithCoeffs b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let b' := I.ringBasis b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let ab := I.selfBasis b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have ab_eq := I.selfBasis_def b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have mem_I_iff : ∀ x, x ∈ I ↔ ∀ i, a i ∣ b'.repr x i := by
  intro x
  rw [ab.mem_ideal_iff']
  simp_rw [ab_eq]
  have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i :=
    by
    intro c i
    simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
  constructor
  · rintro ⟨c, rfl⟩ i
    exact ⟨c i, this c i⟩
  · rintro ha
    choose c hc using ha
    exact
      ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
        -- Now we map everything through the linear equiv `S ≃ₗ (ι → R)`,
          -- which maps `I` to `I' := Π i, a i ℤ`.
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
⊢ ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
rw [ab.mem_ideal_iff']
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ (∃ c, x = ∑ i : ι, c i • ↑(↑ab i)) ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
simp_rw [ab_eq]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i :=
  by
  intro c i
  simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
[PROOFSTEP]
intro c i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
c : ι → R
i : ι
⊢ ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
[PROOFSTEP]
simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) →
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
rintro ⟨c, rfl⟩ i
[GOAL]
case mp.intro
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
c : ι → R
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr (∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x)) i
[PROOFSTEP]
exact ⟨c i, this c i⟩
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i) →
    ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
rintro ha
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
ha : ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
⊢ ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
choose c hc using ha
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
c : ι → R
hc : ∀ (i : ι), ↑(↑(ringBasis b I hI).repr x) i = smithCoeffs b I hI i * c i
⊢ ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
exact
  ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
    -- Now we map everything through the linear equiv `S ≃ₗ (ι → R)`,
      -- which maps `I` to `I' := Π i, a i ℤ`.
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span ({a i} : Set R)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have : Submodule.map (b'.equivFun : S →ₗ[R] ι → R) (I.restrictScalars R) = I' :=
  by
  ext x
  simp only [Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ, Submodule.restrictScalars_mem,
    mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe, Basis.equivFun_apply]
  constructor
  · rintro ⟨y, hy, rfl⟩ i
    exact hy i
  · rintro hdvd
    refine' ⟨∑ i, x i • b' i, fun i => _, _⟩ <;> rw [b'.repr_sum_self]
    · exact hdvd i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
⊢ Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ x ∈ Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) ↔ x ∈ I'
[PROOFSTEP]
simp only [Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ, Submodule.restrictScalars_mem,
  mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe, Basis.equivFun_apply]
[GOAL]
case h
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x) →
    ∀ (i : ι), smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩ i
[GOAL]
case h.mp.intro.intro
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
y : S
hy : ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i
[PROOFSTEP]
exact hy i
[GOAL]
case h.mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∀ (i : ι), smithCoeffs b I hI i ∣ x i) →
    ∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x
[PROOFSTEP]
rintro hdvd
[GOAL]
case h.mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
⊢ ∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x
[PROOFSTEP]
refine' ⟨∑ i, x i • b' i, fun i => _, _⟩
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr (∑ i : ι, x i • ↑b' i)) i
[PROOFSTEP]
rw [b'.repr_sum_self]
[GOAL]
case h.mpr.refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
⊢ ↑(↑(ringBasis b I hI).repr (∑ i : ι, x i • ↑b' i)) = x
[PROOFSTEP]
rw [b'.repr_sum_self]
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
i : ι
⊢ smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
exact hdvd i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
refine'
  ((Submodule.Quotient.restrictScalarsEquiv R I).restrictScalars R).symm.trans (σ₁₂ := RingHom.id R) (σ₃₂ :=
    RingHom.id R) _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ (S ⧸ Submodule.restrictScalars R I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
refine'
  (Submodule.Quotient.equiv (I.restrictScalars R) I' b'.equivFun this).trans (σ₁₂ := RingHom.id R) (σ₃₂ := RingHom.id R)
    _
[GOAL]
case refine'_3.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3.refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
classical
let this := Submodule.quotientPi (show ∀ _, Submodule R R from fun i => span ({a i} : Set R))
exact this
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let this := Submodule.quotientPi (show ∀ _, Submodule R R from fun i => span ({a i} : Set R))
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝¹ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this✝ : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
this : ((ι → R) ⧸
    Submodule.pi Set.univ
      (let_fun this := fun i => span {a i};
      this)) ≃ₗ[R]
  (i : ι) → R ⧸ (fun this => this) (fun i => span {a i}) i :=
  Submodule.quotientPi
    (let_fun this := fun i => span {a i};
    this)
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
exact this
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let a := I.smithCoeffs b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let e := I.quotientEquivPiZMod b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
haveI : ∀ i, NeZero (a i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr (smithCoeffs_ne_zero b I hI i)⟩
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (Int.natAbs (a i))
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
classical exact Fintype.ofEquiv (∀ i, ZMod (a i).natAbs) e.symm
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (Int.natAbs (a i))
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
exact Fintype.ofEquiv (∀ i, ZMod (a i).natAbs) e.symm
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : IsDomain S
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F R S
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ (S ⧸ I) ≃ₗ[F] ⨁ (i : ι), R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : IsDomain S
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F R S
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
this : Fintype ι
⊢ (S ⧸ I) ≃ₗ[F] ⨁ (i : ι), R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
exact ((I.quotientEquivPiSpan b _).restrictScalars F).trans (DirectSum.linearEquivFunOnFintype _ _ _).symm
[GOAL]
ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsPrincipalIdealRing R
inst✝⁹ : IsDomain S
inst✝⁸ : Finite ι✝
F : Type u_4
inst✝⁷ : CommRing F
inst✝⁶ : Algebra F R
inst✝⁵ : Algebra F S
inst✝⁴ : IsScalarTower F R S
b✝ : Basis ι✝ R S
I : Ideal S
hI : I ≠ ⊥
ι : Type u_5
inst✝³ : Fintype ι
b : Basis ι R S
inst✝² : Nontrivial F
inst✝¹ : ∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})
⊢ FiniteDimensional.finrank F (S ⧸ I) = ∑ i : ι, FiniteDimensional.finrank F (R ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, FiniteDimensional.finrank_directSum]


[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Subsingleton R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
apply Module.Free.of_subsingleton'
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
classical exact Module.Free.of_equiv (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
exact Module.Free.of_equiv (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Subsingleton R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
infer_instance
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
classical
have f := (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
exact Module.Finite.of_surjective f.toLinearMap (LinearEquiv.surjective f)
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
have f := (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
f : Matrix (Free.ChooseBasisIndex R N) (Free.ChooseBasisIndex R M) R ≃ₗ[R] M →ₗ[R] N
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
exact Module.Finite.of_surjective f.toLinearMap (LinearEquiv.surjective f)
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
classical
letI := nontrivial_of_invariantBasisNumber R
have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix, FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber R
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
h : (M →ₗ[R] N) ≃ₗ[R] Matrix (Module.Free.ChooseBasisIndex R N) (Module.Free.ChooseBasisIndex R M) R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix, FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (↑toLin' (vecMulVec w v)) ≤ 1
[PROOFSTEP]
rw [Matrix.vecMulVec_eq, Matrix.toLin'_mul]
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (LinearMap.comp (↑toLin' (col w)) (↑toLin' (row v))) ≤ 1
[PROOFSTEP]
refine' le_trans (LinearMap.rank_comp_le_left _ _) _
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (↑toLin' (col w)) ≤ 1
[PROOFSTEP]
refine' (LinearMap.rank_le_domain _).trans_eq _
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ Module.rank K (Unit → K) = 1
[PROOFSTEP]
rw [rank_fun', Fintype.card_unit, Nat.cast_one]


[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ StrongRankCondition R
[PROOFSTEP]
suffices ∀ n, ∀ f : (Fin (n + 1) → R) →ₗ[R] Fin n → R, ¬Injective f by rwa [strongRankCondition_iff_succ R]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
this : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
⊢ StrongRankCondition R
[PROOFSTEP]
rwa [strongRankCondition_iff_succ R]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
[PROOFSTEP]
intro n f
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
⊢ ¬Injective ↑f
[PROOFSTEP]
by_contra hf
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
⊢ False
[PROOFSTEP]
let g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := (ExtendByZero.linearMap R castSucc).comp f
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
⊢ False
[PROOFSTEP]
have hg : Injective g := (extend_injective Fin.strictMono_castSucc.injective _).comp hf
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
⊢ False
[PROOFSTEP]
have hnex : ¬∃ i : Fin n, castSucc i = last n := fun ⟨i, hi⟩ => ne_of_lt (castSucc_lt_last i) hi
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
⊢ False
[PROOFSTEP]
let a₀ := (minpoly R g).coeff 0
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
⊢ False
[PROOFSTEP]
have : a₀ ≠ 0 := minpoly_coeff_zero_of_injective hg
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
⊢ False
[PROOFSTEP]
have : a₀ = 0 := by
  -- Evaluate `(minpoly R g) g` at the vector `(0,...,0,1)`
  have heval := LinearMap.congr_fun (minpoly.aeval R g) (Pi.single (Fin.last n) 1)
  obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0)
  rw [← monomial_add_erase (minpoly R g) 0, hP] at heval
  replace heval :=
    congr_fun heval
      (Fin.last n)
        -- Porting note: ...it's just that this line gives a timeout without slightly raising heartbeats
  simpa [hnex] using heval
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
⊢ a₀ = 0
[PROOFSTEP]
have heval := LinearMap.congr_fun (minpoly.aeval R g) (Pi.single (Fin.last n) 1)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
heval : ↑(↑(aeval g) (minpoly R g)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
⊢ a₀ = 0
[PROOFSTEP]
obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0)
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
heval : ↑(↑(aeval g) (minpoly R g)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
P : R[X]
hP : erase 0 (minpoly R g) = X * P
⊢ a₀ = 0
[PROOFSTEP]
rw [← monomial_add_erase (minpoly R g) 0, hP] at heval
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
P : R[X]
heval : ↑(↑(aeval g) (↑(monomial 0) (coeff (minpoly R g) 0) + X * P)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
hP : erase 0 (minpoly R g) = X * P
⊢ a₀ = 0
[PROOFSTEP]
replace heval :=
  congr_fun heval
    (Fin.last n)
      -- Porting note: ...it's just that this line gives a timeout without slightly raising heartbeats
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
P : R[X]
hP : erase 0 (minpoly R g) = X * P
heval :
  ↑(↑(aeval g) (↑(monomial 0) (coeff (minpoly R g) 0) + X * P)) (Pi.single (last n) 1) (last n) =
    ↑0 (Pi.single (last n) 1) (last n)
⊢ a₀ = 0
[PROOFSTEP]
simpa [hnex] using heval
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this✝ : a₀ ≠ 0
this : a₀ = 0
⊢ False
[PROOFSTEP]
contradiction