[GOAL]
α β : FinBddDistLatCat
e : ↑α.toBddDistLatCat.toDistLatCat ≃o ↑β.toBddDistLatCat.toDistLatCat
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e,
                                  map_sup' :=
                                    (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' :=
                                (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' :=
                                      (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' :=
                                  (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' :=
                                      (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' :=
                                  (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
      let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ :
                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ :
              ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinBddDistLatCat
e : ↑α.toBddDistLatCat.toDistLatCat ≃o ↑β.toBddDistLatCat.toDistLatCat
x✝ : (forget FinBddDistLatCat).obj α
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' :=
                                        (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' :=
                                    (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' :=
                                          (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' :=
                                          (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
          let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : FinBddDistLatCat
e : ↑α.toBddDistLatCat.toDistLatCat ≃o ↑β.toBddDistLatCat.toDistLatCat
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ :
                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ :
              ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
      let src :=
        {
          toSupHom :=
            { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e,
                                  map_sup' :=
                                    (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' :=
                                (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' :=
                                      (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' :=
                                  (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' :=
                                      (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' :=
                                  (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinBddDistLatCat
e : ↑α.toBddDistLatCat.toDistLatCat ≃o ↑β.toBddDistLatCat.toDistLatCat
x✝ : (forget FinBddDistLatCat).obj β
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
          let src :=
            {
              toSupHom :=
                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' :=
                                        (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' :=
                                    (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' :=
                                          (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' :=
                                          (_ : ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toBddDistLatCat.toDistLatCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α β : PreordCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PreordCat
e : ↑α ≃o ↑β
x : (forget PreordCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : PreordCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PreordCat
e : ↑α ≃o ↑β
x : (forget PreordCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
X✝ Y✝ : PreordCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordCatToCat.map a₁✝ = preordCatToCat.map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ Y✝ : PreordCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordCatToCat.map a₁✝ = preordCatToCat.map a₂✝
x : (forget PreordCat).obj X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
exact Functor.congr_obj h x


[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥
[PROOFSTEP]
simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero, Polynomial.C_eq_zero, inv_eq_zero,
  Polynomial.leadingCoeff_eq_zero, or_self_iff]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
by_cases h : annIdealGenerator 𝕜 a = 0
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
[GOAL]
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (↑C (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹)
[PROOFSTEP]
apply Polynomial.isUnit_C.mpr
[GOAL]
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹
[PROOFSTEP]
apply IsUnit.mk0
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0
[PROOFSTEP]
apply inv_eq_zero.not.mpr
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0
[PROOFSTEP]
apply Polynomial.leadingCoeff_eq_zero.not.mpr
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬IsPrincipal.generator (annIdeal 𝕜 a) = 0
[PROOFSTEP]
apply (mul_ne_zero_iff.mp h).1
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a
[PROOFSTEP]
simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a, Ideal.span]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p
[PROOFSTEP]
rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
by_cases h : annIdealGenerator 𝕜 a = 0
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
rw [h, minpoly.eq_zero]
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ ¬IsIntegral 𝕜 a
[PROOFSTEP]
rintro ⟨p, p_monic, hp : aeval a p = 0⟩
[GOAL]
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : Monic p
hp : ↑(aeval a) p = 0
⊢ False
[PROOFSTEP]
refine' p_monic.ne_zero (Ideal.mem_bot.mp _)
[GOAL]
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : Monic p
hp : ↑(aeval a) p = 0
⊢ p ∈ ⊥
[PROOFSTEP]
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
exact
  minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _) fun q q_monic hq =>
    degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq) q_monic.ne_zero
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
⊢ annIdealGenerator 𝕜 a = p
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p
[PROOFSTEP]
rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
[PROOFSTEP]
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
[PROOFSTEP]
rw [eq_comm]
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a
[PROOFSTEP]
apply eq_of_monic_of_associated p_monic _ p_gen
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ Monic (annIdealGenerator 𝕜 a)
[PROOFSTEP]
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)


[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ ↑(stdBasis R (fun _x => R) i) 1 i' = if i = i' then 1 else 0
[PROOFSTEP]
rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (if i' = i then 1 else 0) = if i = i' then 1 else 0
[PROOFSTEP]
congr 1
[GOAL]
case e_c
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (i' = i) = (i = i')
[PROOFSTEP]
rw [eq_iff_iff, eq_comm]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
⊢ stdBasis R φ i = pi (diag i)
[PROOFSTEP]
ext x j
[GOAL]
case h.h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ ↑(stdBasis R φ i) x j = ↑(pi (diag i)) x j
[PROOFSTEP]
convert (update_apply (R := R) (φ := φ) (ι := ι) 0 x i j _).symm
[GOAL]
case h.e'_2.h.e'_1
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = ↑id x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i j : ι
⊢ comp (proj i) (stdBasis R φ j) = diag j i
[PROOFSTEP]
rw [stdBasis_eq_pi_diag, proj_pi]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i) ≤ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
refine' iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ comap (stdBasis R φ i) (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) = ⊤
[PROOFSTEP]
simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ ∀ ⦃x : φ i⦄, x ∈ ⊤ → ∀ (i_1 : ι), i_1 ∈ J → ↑(comp (proj i_1) (stdBasis R φ i)) x = 0
[PROOFSTEP]
rintro b - j hj
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ ↑(comp (proj j) (stdBasis R φ i)) b = 0
[PROOFSTEP]
rw [proj_stdBasis_ne R φ j i, zero_apply]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ j ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
j : ι
hj : j ∈ J
hi : j ∈ I
b : φ j
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hi, hj⟩
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
⊢ ∀ ⦃x : (i : ι) → φ i⦄, x ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) → x ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
intro b hb
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
simp only [mem_iInf, mem_ker, proj_apply] at hb
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
rw [←
  show (∑ i in I, stdBasis R φ i (b i)) = b by
    ext i
    rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
    refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
    intro hiI
    rw [stdBasis_same]
    exact hb _ ((hu trivial).resolve_left hiI)]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) = b
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ Finset.sum I (fun i => ↑(stdBasis R φ i) (b i)) i = b i
[PROOFSTEP]
rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ∑ c in I, ↑(stdBasis R φ c) (b c) i = ↑(stdBasis R φ i) (b i) i
[PROOFSTEP]
refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ¬i ∈ I → ↑(stdBasis R φ i) (b i) i = 0
[PROOFSTEP]
intro hiI
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ ↑(stdBasis R φ i) (b i) i = 0
[PROOFSTEP]
rw [stdBasis_same]
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = 0
[PROOFSTEP]
exact hb _ ((hu trivial).resolve_left hiI)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
exact sum_mem_biSup fun i _ => mem_range_self (stdBasis R φ i) (b i)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i) = ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
refine' le_antisymm (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ hd) _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
[PROOFSTEP]
rwa [hI.coe_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
⊢ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
refine' le_trans (iInf_ker_proj_le_iSup_range_stdBasis R φ this) (iSup_mono fun i => _)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
i : ι
⊢ ⨆ (_ : i ∈ Set.Finite.toFinset hI), range (stdBasis R φ i) ≤ ⨆ (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
rw [Set.Finite.mem_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ (i : ι), range (stdBasis R φ i) = ⊤
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ (i : ι), range (stdBasis R φ i) = ⊤
[PROOFSTEP]
convert top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_stdBasis R φ _)
[GOAL]
case h.e'_2.h.e'_4.h
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x✝ : ι
⊢ range (stdBasis R φ x✝) = ⨆ (_ : x✝ ∈ ?intro.convert_1), range (stdBasis R φ x✝)
[PROOFSTEP]
rename_i i
[GOAL]
case h.e'_2.h.e'_4.h
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
⊢ range (stdBasis R φ i) = ⨆ (_ : i ∈ ?intro.convert_1), range (stdBasis R φ i)
[PROOFSTEP]
exact ((@iSup_pos _ _ _ fun _ => range <| stdBasis R φ i) <| Finset.mem_univ i).symm
[GOAL]
case intro.convert_2
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑Finset.univ ∪ ∅
[PROOFSTEP]
rw [Finset.coe_univ, Set.union_empty]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)) (⨆ (i : ι) (_ : i ∈ J), range (stdBasis R φ i))
[PROOFSTEP]
refine'
  Disjoint.mono (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
    (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨅ (i : ι) (_ : i ∈ Iᶜ), ker (proj i)) (⨅ (i : ι) (_ : i ∈ Jᶜ), ker (proj i))
[PROOFSTEP]
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply, funext_iff]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄,
    ((∀ (i : ι), i ∈ Iᶜ → x i = 0) ∧ ∀ (i : ι), i ∈ Jᶜ → x i = 0) → ∀ (a : ι), x a = OfNat.ofNat 0 a
[PROOFSTEP]
rintro b ⟨hI, hJ⟩ i
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
classical
by_cases hiI : i ∈ I
· by_cases hiJ : i ∈ J
  · exact (h.le_bot ⟨hiI, hiJ⟩).elim
  · exact hJ i hiJ
· exact hI i hiI
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
by_cases hiI : i ∈ I
[GOAL]
case pos
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
by_cases hiJ : i ∈ J
[GOAL]
case pos
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact (h.le_bot ⟨hiI, hiJ⟩).elim
[GOAL]
case neg
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : ¬i ∈ J
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact hJ i hiJ
[GOAL]
case neg
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact hI i hiI
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
[PROOFSTEP]
have hs' : ∀ j : η, LinearIndependent R fun i : ιs j => stdBasis R Ms j (v j i) :=
  by
  intro j
  exact (hs j).map' _ (ker_stdBasis _ _ _)
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
j : η
⊢ LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
[PROOFSTEP]
exact (hs j).map' _ (ker_stdBasis _ _ _)
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
[PROOFSTEP]
apply linearIndependent_iUnion_finite hs'
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ ∀ (i : η) (t : Set η),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
          (⨆ (i : η) (_ : i ∈ t), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
intro j J _ hiJ
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
simp only
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₀ : ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ LinearMap.range (stdBasis R Ms j) :=
  by
  intro j
  rw [span_le, LinearMap.range_coe]
  apply range_comp_subset_range
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
rw [span_le, LinearMap.range_coe]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ⊆ Set.range ↑(stdBasis R Ms j)
[PROOFSTEP]
apply range_comp_subset_range
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₁ :
  span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ ⨆ i ∈ ({ j } : Set _), LinearMap.range (stdBasis R Ms i) :=
  by
  rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
  apply h₀
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
[PROOFSTEP]
rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
apply h₀
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₂ :
  ⨆ j ∈ J, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j : η => Ms j) j) :=
  iSup₂_mono fun i _ => h₀ i
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₃ : Disjoint (fun i : η => i ∈ ({ j } : Set _)) J := by convert Set.disjoint_singleton_left.2 hiJ using 0
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (fun i => i ∈ {j}) J
[PROOFSTEP]
convert Set.disjoint_singleton_left.2 hiJ using 0
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
h₃ : Disjoint (fun i => i ∈ {j}) J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
exact (disjoint_stdBasis_stdBasis _ _ _ _ h₃).mono h₁ h₂
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i)) = Finsupp.single { fst := j, snd := i } 1
[PROOFSTEP]
ext ⟨j', i'⟩
[GOAL]
case h.mk
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
by_cases hj : j = j'
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
subst hj
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j, snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
[PROOFSTEP]
simp only [Pi.basis, LinearEquiv.trans_apply, Basis.repr_self, stdBasis_same, LinearEquiv.piCongrRight,
  Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Basis.repr_symm_apply, LinearEquiv.coe_mk, ne_eq, Sigma.mk.inj_iff,
  heq_eq_eq, true_and]
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single i 1) i' = ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
[PROOFSTEP]
symm
  -- Porting note: `Sigma.mk.inj` not found in the following, replaced by `Sigma.mk.inj_iff.mp`
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' } = ↑(Finsupp.single i 1) i'
[PROOFSTEP]
exact
  Finsupp.single_apply_left (fun i i' (h : (⟨j, i⟩ : Σ j, ιs j) = ⟨j, i'⟩) => eq_of_heq (Sigma.mk.inj_iff.mp h).2) _ _ _
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, LinearEquiv.piCongrRight]
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := fun f i => ↑(s i).repr (f i),
                      map_add' :=
                        (_ :
                          ∀ (x y : (j : η) → (fun j => Ms j) j),
                            Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                              Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (f : (i : η) → (fun j => Ms j) i),
                        AddHom.toFun
                            { toFun := fun f i => ↑(s i).repr (f i),
                              map_add' :=
                                (_ :
                                  ∀ (x y : (j : η) → (fun j => Ms j) j),
                                    Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) }
                            (c • f) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f i => ↑(s i).repr (f i),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : (j : η) → (fun j => Ms j) j),
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                          (x + y) =
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                          Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                            y) }
                              f) },
              invFun := fun f i => ↑(LinearEquiv.symm (s i).repr) (f i),
              left_inv :=
                (_ :
                  LeftInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun),
              right_inv :=
                (_ :
                  Function.RightInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun) }
          (↑(stdBasis R Ms j) (↑(s j) i)) j')
      i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
dsimp
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(s j').repr (↑(stdBasis R Ms j) (↑(s j) i) j')) i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
rw [stdBasis_ne _ _ _ _ (Ne.symm hj), LinearEquiv.map_zero, Finsupp.zero_apply, Finsupp.single_eq_of_ne]
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ { fst := j, snd := i } ≠ { fst := j', snd := i' }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case neg.refl
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
hj : ¬j = j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms ji.fst) (↑(s ji.fst) ji.snd)) = Finsupp.single ji 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
i : η
⊢ ↑(basisFun R η) i = ↑(stdBasis R (fun x => R) i) 1
[PROOFSTEP]
simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply, stdBasis_apply]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Semiring R
inst✝² : (i : η) → AddCommMonoid (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : Fintype η
x : η → R
i : η
⊢ ↑(↑(basisFun R η).repr x) i = x i
[PROOFSTEP]
simp [basisFun]
[GOAL]
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
⊢ ↑(stdBasis R n m) (i, j) = stdBasisMatrix i j 1
[PROOFSTEP]
ext a b
[GOAL]
case a.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hi : i = a
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hj : j = b
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hj : j = b
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp [stdBasis, hi, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, StdBasisMatrix.apply_same]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := b } a b = 1
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := b }.fst) (↑(Pi.basisFun R m) { fst := a, snd := b }.snd) a
      b =
    1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, hi, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hj, and_false, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := j } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := j }.fst) (↑(Pi.basisFun R m) { fst := a, snd := j }.snd) a
      b =
    0
[PROOFSTEP]
simp [hj]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hi, and_true, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := b } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := b }.fst) (↑(Pi.basisFun R m) { fst := i, snd := b }.snd) a
      b =
    0
[PROOFSTEP]
simp [hi, hj, Ne.symm hi, LinearMap.stdBasis_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hi, hj, and_self, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := j } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := j }.fst) (↑(Pi.basisFun R m) { fst := i, snd := j }.snd) a
      b =
    0
[PROOFSTEP]
simp [hi, hj, Ne.symm hj, Ne.symm hi, LinearMap.stdBasis_ne]