[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : G ≃+ H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : G ≃+ H
x✝ : G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                    invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_mul' :=
                  (_ :
                    ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : Multiplicative G ≃* Multiplicative H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : AddZeroClass H
x : Multiplicative G ≃* Multiplicative H
x✝ : Multiplicative G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_add' :=
                  (_ :
                    ∀ (x y : Multiplicative G),
                      Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : G ≃* H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : G ≃* H
x✝ : G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                    invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_add' :=
                  (_ :
                    ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : Additive G ≃+ Additive H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
              invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : MulOneClass H
x : Additive G ≃+ Additive H
x✝ : Additive G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑MonoidHom.toAdditive (toMonoidHom f)),
                  invFun := ↑(↑MonoidHom.toAdditive (toMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(AddEquiv.toAddMonoidHom f), invFun := ↑(AddEquiv.toAddMonoidHom (AddEquiv.symm f)),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_mul' :=
                  (_ :
                    ∀ (x y : Additive G),
                      Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : Additive G ≃+ H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ :
                ∀ (x y : Additive G),
                  Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : Additive G ≃+ H
x✝ : Additive G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                    invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_mul' :=
                  (_ :
                    ∀ (x y : Additive G),
                      Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : G ≃* Multiplicative H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ :
              ∀ (x y : Additive G),
                Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : MulOneClass G
inst✝ : AddZeroClass H
x : G ≃* Multiplicative H
x✝ : G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ :
                  ∀ (x y : Additive G),
                    Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_add' :=
                  (_ :
                    ∀ (x y : G), Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : G ≃+ Additive H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_add' :=
            (_ :
              ∀ (x y : Multiplicative G),
                Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_mul' :=
              (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : G ≃+ Additive H
x✝ : G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_add' :=
                (_ :
                  ∀ (x y : Multiplicative G),
                    Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                    invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_mul' :=
                  (_ :
                    ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : Multiplicative G ≃* H
⊢ (fun f =>
        {
          toEquiv :=
            { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
              invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
              left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
              right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
          map_mul' :=
            (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
      ((fun f =>
          {
            toEquiv :=
              { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
            map_add' :=
              (_ :
                ∀ (x y : Multiplicative G),
                  Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝¹ : AddZeroClass G
inst✝ : MulOneClass H
x : Multiplicative G ≃* H
x✝ : Multiplicative G
⊢ ↑((fun f =>
            {
              toEquiv :=
                { toFun := ↑(↑AddMonoidHom.toMultiplicative'' (toAddMonoidHom f)),
                  invFun := ↑(↑AddMonoidHom.toMultiplicative' (toAddMonoidHom (symm f))),
                  left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                  right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
              map_mul' :=
                (_ : ∀ (x y : G), Equiv.toFun f.toEquiv (x + y) = Equiv.toFun f.toEquiv x + Equiv.toFun f.toEquiv y) })
          ((fun f =>
              {
                toEquiv :=
                  { toFun := ↑(MulEquiv.toMonoidHom f), invFun := ↑(MulEquiv.toMonoidHom (MulEquiv.symm f)),
                    left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
                    right_inv := (_ : Function.RightInverse f.invFun f.toFun) },
                map_add' :=
                  (_ :
                    ∀ (x y : Multiplicative G),
                      Equiv.toFun f.toEquiv (x * y) = Equiv.toFun f.toEquiv x * Equiv.toFun f.toEquiv y) })
            x))
      x✝ =
    ↑x x✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ ↑f ↑u * ↑f u.inv = 1
[PROOFSTEP]
rw [← f.map_mul, u.val_inv, f.map_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ ↑f u.inv * ↑f ↑u = 1
[PROOFSTEP]
rw [← f.map_mul, u.inv_val, f.map_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : Mˣ
⊢ ↑(↑(map (MonoidHom.id M)) x✝) = ↑(↑(MonoidHom.id Mˣ) x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / ↑u
[PROOFSTEP]
rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ g 1 = 1
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑(g 1) = ↑1
[PROOFSTEP]
dsimp only
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑(g 1) = ↑1
[PROOFSTEP]
rw [h 1]
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑f 1 = ↑1
[PROOFSTEP]
exact f.map_one
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x y : M
⊢ ↑(OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } (x * y)) =
    ↑(OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } x *
        OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } y)
[PROOFSTEP]
simp only [h, val_mul, f.map_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x : M
⊢ ↑f x * ↑(↑(liftRight f g h) x)⁻¹ = 1
[PROOFSTEP]
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x : M
⊢ ↑(↑(liftRight f g h) x)⁻¹ * ↑f x = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit (↑f x)
[PROOFSTEP]
rcases h with ⟨y, rfl⟩
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (↑f ↑y)
[PROOFSTEP]
exact (Units.map (f : M →* N) y).isUnit
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MonoidHomClass F M N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ↑g ↑f
h : IsUnit (↑f x)
⊢ IsUnit x
[PROOFSTEP]
simpa only [hfg x] using h.map g
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x : M
⊢ ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (↑f x))) = ↑f x
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x : M
⊢ ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (↑f x))) = ↑f x
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ a / a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c : α
h : IsUnit b
a : α
⊢ a / b * b = a
[PROOFSTEP]
rw [div_eq_mul_inv, h.inv_mul_cancel_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c : α
h : IsUnit b
a : α
⊢ a * b / b = a
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_cancel_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ a * (1 / a) = 1
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ 1 / a * a = 1
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ IsUnit a⁻¹
[PROOFSTEP]
rcases h with ⟨u, hu⟩
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹
[PROOFSTEP]
rw [← hu, ← Units.val_inv_eq_inv_val]
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
[PROOFSTEP]
exact Units.isUnit _
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
[PROOFSTEP]
exact ha.mul hb.inv
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
[PROOFSTEP]
exact Units.mul_left_inj h.inv.unit'
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b
[PROOFSTEP]
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ b / (a * b) = 1 / a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b✝ c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c a : α
h : IsUnit b
⊢ a * b * (1 / b) = a
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b
[PROOFSTEP]
rw [mul_comm, h.div_mul_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * b / a = b
[PROOFSTEP]
rw [mul_comm, h.mul_div_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * (b / a) = b
[PROOFSTEP]
rw [mul_comm, h.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a✝ b✝ c d : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b
[PROOFSTEP]
rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a✝ b c✝ d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b
[PROOFSTEP]
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
[PROOFSTEP]
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm, hd.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / (a / b) = b
[PROOFSTEP]
rw [div_div_eq_mul_div, h.mul_div_cancel_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / b / a = b⁻¹
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Add α
inst✝¹ : Semigroup α
inst✝ : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c
[PROOFSTEP]
simp [left_distrib, hd, he]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, -b = a * ↑(Equiv.neg α).symm b_1) ↔ a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = -a * ↑(Equiv.neg α).symm b_1) ↔ a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c
[PROOFSTEP]
simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b
[PROOFSTEP]
simpa only [add_sub_cancel] using dvd_sub H h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c
[PROOFSTEP]
exact dvd_add_left h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b
[PROOFSTEP]
simpa only [← sub_eq_add_neg] using dvd_add_left ((dvd_neg (α := α)).2 h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c
[PROOFSTEP]
rw [sub_eq_add_neg, dvd_add_right h, dvd_neg (α := α)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c
[PROOFSTEP]
rw [← sub_add_cancel b c, dvd_add_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b
[PROOFSTEP]
rw [← dvd_neg (α := α), neg_sub]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y
[PROOFSTEP]
convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y
[PROOFSTEP]
rw [mul_sub_left_distrib, mul_sub_right_distrib]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * x - a * y + (a * y - b * y)
[PROOFSTEP]
simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]


[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a b c : M →* N), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ c✝ : M →* N
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ c✝ : M →* N
x✝ : M
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
apply mul_assoc
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a : M →* N), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
x✝ : M
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
apply one_mul
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a : M →* N), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ : M →* N
x✝ : M
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
apply mul_one
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
⊢ (fun x => ↑f x ^ n) 1 = 1
[PROOFSTEP]
simp
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } x *
      OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } y
[PROOFSTEP]
simp [mul_pow]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      0 f =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          0 f)
      x =
    ↑1 x
[PROOFSTEP]
simp
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (n + 1) f =
    f *
      (fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        n f
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
n : ℕ
f : M →* N
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (n + 1) f)
      x =
    ↑(f *
          (fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            n f)
      x
[PROOFSTEP]
simp [pow_succ]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
⊢ ∀ (a b : M →* N), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ : M →* N
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
a✝ b✝ : M →* N
x✝ : M
⊢ ↑(a✝ * b✝) x✝ = ↑(b✝ * a✝) x✝
[PROOFSTEP]
apply mul_comm
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
⊢ ∀ (a b : M →* G), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ b✝ : M →* G
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ b✝ : M →* G
x✝ : M
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
apply div_eq_mul_inv
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℤ
f : M →* G
⊢ (fun x => ↑f x ^ n) 1 = 1
[PROOFSTEP]
simp
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℤ
f : M →* G
x y : M
⊢ OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } x *
      OneHom.toFun { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) } y
[PROOFSTEP]
simp [mul_zpow]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      0 f =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          0 f)
      x =
    ↑1 x
[PROOFSTEP]
simp
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (Int.ofNat (Nat.succ n)) f =
    f *
      (fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        (Int.ofNat n) f
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (Int.ofNat (Nat.succ n)) f)
      x =
    ↑(f *
          (fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            (Int.ofNat n) f)
      x
[PROOFSTEP]
simp [zpow_ofNat, pow_succ]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
⊢ (fun n f =>
        { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
          map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
      (Int.negSucc n) f =
    ((fun n f =>
          { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
            map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
        (↑(Nat.succ n)) f)⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
n : ℕ
f : M →* G
x : M
⊢ ↑((fun n f =>
            { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
              map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
          (Int.negSucc n) f)
      x =
    ↑((fun n f =>
              { toOneHom := { toFun := fun x => ↑f x ^ n, map_one' := (_ : ↑f 1 ^ n = 1) },
                map_mul' := (_ : ∀ (x y : M), ↑f (x * y) ^ n = ↑f x ^ n * ↑f y ^ n) })
            (↑(Nat.succ n)) f)⁻¹
      x
[PROOFSTEP]
simp [Nat.succ_eq_add_one, zpow_ofNat]
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
⊢ ∀ (a : M →* G), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ : M →* G
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
M✝ : Type uM
N : Type uN
P : Type uP
Q : Type uQ
M : Type ?u.8567
G : Type ?u.8570
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
src✝ : CommMonoid (M →* G) := commMonoid
a✝ : M →* G
x✝ : M
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply mul_left_inv
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ (fun x => ↑(↑f x) y) 1 = 1
[PROOFSTEP]
simp [f.map_one, one_apply]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
x₁ x₂ : M
⊢ OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } (x₁ * x₂) =
    OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } x₁ *
      OneHom.toFun { toFun := fun x => ↑(↑f x) y, map_one' := (_ : ↑(↑f 1) y = 1) } x₂
[PROOFSTEP]
simp [f.map_mul, mul_apply]
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
⊢ (fun g =>
        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
      1 =
    1
[PROOFSTEP]
ext1 f
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
f : M →* N
⊢ ↑((fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
          1)
      f =
    ↑1 f
[PROOFSTEP]
exact one_comp f
[GOAL]
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
⊢ OneHom.toFun
      {
        toFun := fun g =>
          { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
            map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
        map_one' :=
          (_ :
            (fun g =>
                  { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                    map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                1 =
              1) }
      (g₁ * g₂) =
    OneHom.toFun
        {
          toFun := fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
          map_one' :=
            (_ :
              (fun g =>
                    { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                      map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                  1 =
                1) }
        g₁ *
      OneHom.toFun
        {
          toFun := fun g =>
            { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
              map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
          map_one' :=
            (_ :
              (fun g =>
                    { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                      map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                  1 =
                1) }
        g₂
[PROOFSTEP]
ext1 f
[GOAL]
case h
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
f : M →* N
⊢ ↑(OneHom.toFun
          {
            toFun := fun g =>
              { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
            map_one' :=
              (_ :
                (fun g =>
                      { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                        map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                    1 =
                  1) }
          (g₁ * g₂))
      f =
    ↑(OneHom.toFun
            {
              toFun := fun g =>
                { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                  map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
              map_one' :=
                (_ :
                  (fun g =>
                        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                      1 =
                    1) }
            g₁ *
          OneHom.toFun
            {
              toFun := fun g =>
                { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                  map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) },
              map_one' :=
                (_ :
                  (fun g =>
                        { toOneHom := { toFun := comp g, map_one' := (_ : comp g 1 = 1) },
                          map_mul' := (_ : ∀ (f₁ f₂ : M →* N), comp g (f₁ * f₂) = comp g f₁ * comp g f₂) })
                      1 =
                    1) }
            g₂)
      f
[PROOFSTEP]
exact mul_comp g₁ g₂ f


[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : SetLike σ R
inst✝ : AddSubmonoidClass σ R
A : ι → σ
i : ι
⊢ AddCommMonoid { x // x ∈ A i }
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝² : Ring R
inst✝¹ : SetLike σ R
inst✝ : AddSubgroupClass σ R
A : ι → σ
i : ι
⊢ AddCommGroup { x // x ∈ A i }
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ ↑(algebraMap S R) s ∈ A 0
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ s • 1 ∈ A 0
[PROOFSTEP]
exact (A 0).smul_mem s <| SetLike.one_mem_graded _
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n : ℕ
⊢ ↑n ∈ A 0
[PROOFSTEP]
induction' n with _ n_ih
[GOAL]
case zero
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ ↑Nat.zero ∈ A 0
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0
[PROOFSTEP]
exact zero_mem (A 0)
[GOAL]
case succ
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(Nat.succ n✝) ∈ A 0
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
case succ
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0
[PROOFSTEP]
exact add_mem n_ih (SetLike.one_mem_graded _)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0
[PROOFSTEP]
induction z
[GOAL]
case ofNat
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0
[PROOFSTEP]
rw [Int.ofNat_eq_coe, Int.cast_ofNat]
[GOAL]
case ofNat
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0
[PROOFSTEP]
exact SetLike.nat_cast_mem_graded _ _
[GOAL]
case negSucc
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0
[PROOFSTEP]
rw [Int.cast_negSucc]
[GOAL]
case negSucc
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
[PROOFSTEP]
exact neg_mem (SetLike.nat_cast_mem_graded _ _)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(r * r') n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (DFinsupp.support r ×ˢ DFinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
[PROOFSTEP]
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(↑(↑(of (fun i => (fun i => { x // x ∈ A i }) i) (i.fst + i.snd)) (GradedMonoid.GMul.mul (↑r i.fst) (↑r' i.snd)))
          n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (DFinsupp.support r ×ˢ DFinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
[PROOFSTEP]
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
rw [mul_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(DFinsupp.sum r fun i ai =>
            DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]; congr; ext
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(DFinsupp.sum r fun i ai =>
            DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in DFinsupp.support r,
      ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul (↑r i) aj)) n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
congr
[GOAL]
case e_f
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ (fun i =>
      ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul (↑r i) aj)) n)) =
    fun i => (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) i (↑r i)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (x✝ + j)) (GradedMonoid.GMul.mul (↑r x✝) aj)) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (↑r x✝)
[PROOFSTEP]
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]
[GOAL]
case e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ ∑ i in DFinsupp.support r',
      ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝ + i)) (GradedMonoid.GMul.mul (↑r x✝) (↑r' i))) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (↑r x✝)
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_f
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ (fun i => ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝ + i)) (GradedMonoid.GMul.mul (↑r x✝) (↑r' i))) n)) = fun i =>
    (fun j rj => if x✝ + j = n then ↑(↑r x✝) * ↑rj else 0) i (↑r' i)
[PROOFSTEP]
ext
[GOAL]
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) =
    (fun j rj => if x✝¹ + j = n then ↑(↑r x✝¹) * ↑rj else 0) x✝ (↑r' x✝)
[PROOFSTEP]
dsimp only
[GOAL]
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) =
    if x✝¹ + x✝ = n then ↑(↑r x✝¹) * ↑(↑r' x✝) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) = ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) (x✝¹ + x✝)) =
    ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
rw [of_eq_same]
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
x✝¹ x✝ : ι
⊢ ↑(GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝)) = ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) = 0
[PROOFSTEP]
rw [of_eq_of_ne _ _ _ _ h]
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑0 = 0
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' j)
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
  exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' j)
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r) fun i ri =>
      DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) =
    ↑r * ↑(↑r' j)
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = ↑r * ↑(↑r' j)
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = ↑r * ↑(↑r' j)
[PROOFSTEP]
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r' then ↑r * ↑(↑r' j) else 0) = ↑r * ↑(↑r' j)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∈ DFinsupp.support r'
⊢ ↑r * ↑(↑r' j) = ↑r * ↑(↑r' j)
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : ¬j ∈ DFinsupp.support r'
⊢ 0 = ↑r * ↑(↑r' j)
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : ¬j ∈ DFinsupp.support r'
⊢ 0 = ↑r * ↑(↑r' j)
[PROOFSTEP]
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r j) * ↑r'
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
  exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r j) * ↑r'
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r') fun i₂ x₂ =>
      DFinsupp.sum r fun i₁ x₁ => if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    ↑(↑r j) * ↑r'
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = ↑(↑r j) * ↑r'
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = ↑(↑r j) * ↑r'
[PROOFSTEP]
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r then ↑(↑r j) * ↑r' else 0) = ↑(↑r j) * ↑r'
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∈ DFinsupp.support r
⊢ ↑(↑r j) * ↑r' = ↑(↑r j) * ↑r'
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : ¬j ∈ DFinsupp.support r
⊢ 0 = ↑(↑r j) * ↑r'
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : ¬j ∈ DFinsupp.support r
⊢ 0 = ↑(↑r j) * ↑r'
[PROOFSTEP]
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
  exact DFinsupp.sum_zero
· rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
  exact fun x _ H => h ((self_le_add_right i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r) fun i ri =>
      DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) =
    0
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = 0
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = 0
[PROOFSTEP]
rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ∀ (x : ι), x ∈ DFinsupp.support r' → i + x = n → False
[PROOFSTEP]
exact fun x _ H => h ((self_le_add_right i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
  exact DFinsupp.sum_zero
· rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
  exact fun x _ H => h ((self_le_add_left i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r') fun i₂ x₂ =>
      DFinsupp.sum r fun i₁ x₁ => if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    0
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = 0
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = 0
[PROOFSTEP]
rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ∀ (x : ι), x ∈ DFinsupp.support r → x + i = n → False
[PROOFSTEP]
exact fun x _ H => h ((self_le_add_left i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring R
inst✝⁶ : SetLike σ R
inst✝⁵ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁴ : CanonicallyOrderedAddMonoid ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i
[PROOFSTEP]
rw [eq_tsub_iff_add_eq_of_le h, add_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = if i ≤ n then ↑(↑r (n - i)) * ↑r' else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r (n - i)) * ↑r'
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = if i ≤ n then ↑r * ↑(↑r' (n - i)) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' (n - i))
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p : Submodule S R
⊢ 1 ∈ p ^ 0
[PROOFSTEP]
rw [← one_le, pow_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ (i + j)
[PROOFSTEP]
rw [pow_add]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ i * p✝ ^ j
[PROOFSTEP]
exact Submodule.mul_mem_mul hp hq
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) 0) GradedMonoid.GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
i✝ j✝ : ι
x✝¹ : { x // x ∈ A i✝ }
x✝ : { x // x ∈ A j✝ }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) (i✝ + j✝))
      (GradedMonoid.GMul.mul x✝¹ x✝) =
    ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) i✝) x✝¹ *
      ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) j✝) x✝
[PROOFSTEP]
rfl