[GOAL]
α β : BddDistLatCat
e : ↑α.toDistLatCat ≃o ↑β.toDistLatCat
⊢ ((let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.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 : ↑β.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toDistLatCat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.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
α β : BddDistLatCat
e : ↑α.toDistLatCat ≃o ↑β.toDistLatCat
x✝ : (forget BddDistLatCat).obj α
⊢ ↑((let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.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 : ↑β.toDistLatCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toDistLatCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.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]
α β : BddDistLatCat
e : ↑α.toDistLatCat ≃o ↑β.toDistLatCat
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ :
                  ∀ (a b : ↑β.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toDistLatCat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toDistLatCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toDistLatCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.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 : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toDistLatCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.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
α β : BddDistLatCat
e : ↑α.toDistLatCat ≃o ↑β.toDistLatCat
x✝ : (forget BddDistLatCat).obj β
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toDistLatCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toDistLatCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toDistLatCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.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 : ↑β.toDistLatCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toDistLatCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.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 : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toDistLatCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toDistLatCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.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]
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
x : (forget NonemptyFinLinOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
x : (forget NonemptyFinLinOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
A B : NonemptyFinLinOrdCat
x✝¹ x✝ : A ⟶ B
h :
  (fun f =>
        ↑(let_fun this := f;
          this))
      x✝¹ =
    (fun f =>
        ↑(let_fun this := f;
          this))
      x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
ext x
[GOAL]
case w
A B : NonemptyFinLinOrdCat
x✝¹ x✝ : A ⟶ B
h :
  (fun f =>
        ↑(let_fun this := f;
          this))
      x✝¹ =
    (fun f =>
        ↑(let_fun this := f;
          this))
      x✝
x : (forget NonemptyFinLinOrdCat).obj A
⊢ ↑x✝¹ x = ↑x✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
refine' ⟨_, ConcreteCategory.mono_of_injective f⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f → Function.Injective ↑f
[PROOFSTEP]
intro
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ↑f
[PROOFSTEP]
intro a₁ a₂ h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
⊢ a₁ = a₂
[PROOFSTEP]
let X := NonemptyFinLinOrdCat.of (ULift (Fin 1))
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
⊢ a₁ = a₂
[PROOFSTEP]
let g₁ : X ⟶ A := ⟨fun _ => a₁, fun _ _ _ => by rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₁) x✝² ≤ (fun x => a₁) x✝¹
[PROOFSTEP]
rfl
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
⊢ a₁ = a₂
[PROOFSTEP]
let g₂ : X ⟶ A := ⟨fun _ => a₂, fun _ _ _ => by rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₂) x✝² ≤ (fun x => a₂) x✝¹
[PROOFSTEP]
rfl
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ a₁ = a₂
[PROOFSTEP]
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
have eq : g₁ ≫ f = g₂ ≫ f := by
  ext
  exact h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ g₁ ≫ f = g₂ ≫ f
[PROOFSTEP]
ext
[GOAL]
case w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
x✝ : (forget NonemptyFinLinOrdCat).obj X
⊢ ↑(g₁ ≫ f) x✝ = ↑(g₂ ≫ f) x✝
[PROOFSTEP]
exact h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ ≫ f = g₂ ≫ f
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
rw [cancel_mono] at eq
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ = g₂
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
rw [eq]
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f → Function.Surjective ↑f
[PROOFSTEP]
intro
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ Function.Surjective ↑f
[PROOFSTEP]
dsimp only [Function.Surjective]
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, ↑f a = b
[PROOFSTEP]
by_contra' hf'
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
hf' : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
[PROOFSTEP]
rcases hf' with ⟨m, hm⟩
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
⊢ False
[PROOFSTEP]
let Y := NonemptyFinLinOrdCat.of (ULift (Fin 2))
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
⊢ False
[PROOFSTEP]
let p₁ : B ⟶ Y :=
  ⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
    by
    simp only
    split_ifs with h₁ h₂ h₂
    any_goals apply Fin.zero_le
    · exfalso
      exact h₁ (lt_of_le_of_lt h h₂)
    · rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
    (fun b => if b < m then { down := 0 } else { down := 1 }) x₂
[PROOFSTEP]
simp only
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ < m then { down := 0 } else { down := 1 }) ≤ if x₂ < m then { down := 0 } else { down := 1 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 0 } ≤ { down := 1 }
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
any_goals apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 0 } ≤ { down := 1 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ False
[PROOFSTEP]
exact h₁ (lt_of_le_of_lt h h₂)
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
rfl
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
⊢ False
[PROOFSTEP]
let p₂ : B ⟶ Y :=
  ⟨fun b => if b ≤ m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
    by
    simp only
    split_ifs with h₁ h₂ h₂
    any_goals apply Fin.zero_le
    · exfalso
      exact h₁ (h.trans h₂)
    · rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
    (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂
[PROOFSTEP]
simp only
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ ≤ m then { down := 0 } else { down := 1 }) ≤ if x₂ ≤ m then { down := 0 } else { down := 1 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
any_goals apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False
[PROOFSTEP]
exact h₁ (h.trans h₂)
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
[PROOFSTEP]
rfl
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ False
[PROOFSTEP]
have h : p₁ m = p₂ m := by
  congr
  rw [← cancel_epi f]
  ext a
  simp only [coe_of, comp_apply]
  change ite _ _ _ = ite _ _ _
  split_ifs with h₁ h₂ h₂
  any_goals rfl
  · exfalso
    exact h₂ (le_of_lt h₁)
  · exfalso
    exact hm a (eq_of_le_of_not_lt h₂ h₁)
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ ↑p₁ m = ↑p₂ m
[PROOFSTEP]
congr
[GOAL]
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ p₁ = p₂
[PROOFSTEP]
rw [← cancel_epi f]
[GOAL]
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ f ≫ p₁ = f ≫ p₂
[PROOFSTEP]
ext a
[GOAL]
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ ↑(f ≫ p₁) a = ↑(f ≫ p₂) a
[PROOFSTEP]
simp only [coe_of, comp_apply]
[GOAL]
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ ↑{ toFun := fun b => if b < m then { down := 0 } else { down := 1 },
          monotone' :=
            (_ :
              ∀ (x₁ x₂ : ↑B),
                x₁ ≤ x₂ →
                  (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
                    (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
      (↑f a) =
    ↑{ toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
          monotone' :=
            (_ :
              ∀ (x₁ x₂ : ↑B),
                x₁ ≤ x₂ →
                  (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
                    (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
      (↑f a)
[PROOFSTEP]
change ite _ _ _ = ite _ _ _
[GOAL]
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (if ↑f a < m then { down := 0 } else { down := 1 }) = if ↑f a ≤ m then { down := 0 } else { down := 1 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 0 } = { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 1 } = { down := 1 }
[PROOFSTEP]
any_goals rfl
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 0 } = { down := 0 }
[PROOFSTEP]
rfl
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }
[PROOFSTEP]
rfl
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }
[PROOFSTEP]
rfl
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 1 } = { down := 1 }
[PROOFSTEP]
rfl
[GOAL]
case neg
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ False
[PROOFSTEP]
exact h₂ (le_of_lt h₁)
[GOAL]
case pos
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ False
[PROOFSTEP]
exact hm a (eq_of_le_of_not_lt h₂ h₁)
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
h : ↑p₁ m = ↑p₂ m
⊢ False
[PROOFSTEP]
simp [FunLike.coe] at h
[GOAL]
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Function.Surjective ↑f → Epi f
[PROOFSTEP]
intro h
[GOAL]
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
h : Function.Surjective ↑f
⊢ Epi f
[PROOFSTEP]
exact ConcreteCategory.epi_of_surjective f h
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
⊢ IsSplitEpi f
[PROOFSTEP]
have H : ∀ y : Y, Nonempty (f ⁻¹' { y }) := by
  rw [epi_iff_surjective] at hf
  intro y
  exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
⊢ ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
rw [epi_iff_surjective] at hf
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Function.Surjective ↑f
⊢ ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
intro y
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Function.Surjective ↑f
y : ↑Y
⊢ Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
⊢ IsSplitEpi f
[PROOFSTEP]
let φ : Y → X := fun y => (H y).some.1
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
⊢ IsSplitEpi f
[PROOFSTEP]
have hφ : ∀ y : Y, f (φ y) = y := fun y => (H y).some.2
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ IsSplitEpi f
[PROOFSTEP]
refine' IsSplitEpi.mk' ⟨⟨φ, _⟩, _⟩
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ Monotone φ
case refine'_2
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ { toFun := φ, monotone' := ?refine'_1 } ≫ f = 𝟙 Y
[PROOFSTEP]
swap
[GOAL]
case refine'_2
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ { toFun := φ, monotone' := ?refine'_1 } ≫ f = 𝟙 Y
[PROOFSTEP]
ext b
[GOAL]
case refine'_2.w
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : (forget NonemptyFinLinOrdCat).obj Y
⊢ ↑({ toFun := φ, monotone' := ?refine'_1 } ≫ f) b = ↑(𝟙 Y) b
[PROOFSTEP]
apply hφ
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ Monotone φ
[PROOFSTEP]
intro a b
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
⊢ a ≤ b → φ a ≤ φ b
[PROOFSTEP]
contrapose
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
⊢ ¬φ a ≤ φ b → ¬a ≤ b
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ¬φ a ≤ φ b
⊢ ¬a ≤ b
[PROOFSTEP]
simp only [not_le] at h ⊢
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
⊢ b < a
[PROOFSTEP]
suffices b ≤ a by
  apply lt_of_le_of_ne this
  rintro rfl
  exfalso
  simp at h
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
this : b ≤ a
⊢ b < a
[PROOFSTEP]
apply lt_of_le_of_ne this
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
this : b ≤ a
⊢ b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b})))
this : b ≤ b
⊢ False
[PROOFSTEP]
exfalso
[GOAL]
case h
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b})))
this : b ≤ b
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
⊢ b ≤ a
[PROOFSTEP]
have H : f (φ b) ≤ f (φ a) := f.monotone (le_of_lt h)
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H✝ : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
H : ↑f (φ b) ≤ ↑f (φ a)
⊢ b ≤ a
[PROOFSTEP]
simpa only [hφ] using H
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
letI : NonemptyFinLinOrd (Set.image f ⊤) := ⟨by infer_instance⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
⊢ Nonempty ↑(↑f '' ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let I := NonemptyFinLinOrdCat.of (Set.image f ⊤)
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let e : X ⟶ I := ⟨fun x => ⟨f x, ⟨x, by tauto⟩⟩, fun x₁ x₂ h => f.monotone h⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
x : ↑X
⊢ x ∈ ⊤ ∧ ↑f x = ↑f x
[PROOFSTEP]
tauto
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let m : I ⟶ Y := ⟨fun y => y.1, by tauto⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
⊢ Monotone fun y => ↑y
[PROOFSTEP]
tauto
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : Epi e := by
  rw [epi_iff_surjective]
  rintro ⟨_, y, h, rfl⟩
  exact ⟨y, rfl⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Epi e
[PROOFSTEP]
rw [epi_iff_surjective]
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Function.Surjective ↑e
[PROOFSTEP]
rintro ⟨_, y, h, rfl⟩
[GOAL]
case mk.intro.intro
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
y : ↑X
h : y ∈ ⊤
⊢ ∃ a, ↑e a = { val := ↑f y, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f y) }
[PROOFSTEP]
exact ⟨y, rfl⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝ : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this : Epi e
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : StrongEpi e := strongEpi_of_epi e
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝¹ : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this✝ : Epi e
this : StrongEpi e
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝² : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this✝¹ : Epi e
this✝ : StrongEpi e
this : Mono m
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
exact ⟨⟨I, m, e, rfl⟩⟩


[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ hammingDist x x = 0
[PROOFSTEP]
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ ∀ (x_1 : ι), x_1 ∈ univ → ¬x x_1 ≠ x x_1
[PROOFSTEP]
exact fun _ _ H => H rfl
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingDist y x
[PROOFSTEP]
simp_rw [hammingDist, ne_comm]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
[PROOFSTEP]
classical
unfold hammingDist
refine le_trans (card_mono ?_) (card_union_le _ _)
rw [← filter_or]
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
[PROOFSTEP]
unfold hammingDist
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ card (filter (fun i => x i ≠ z i) univ) ≤
    card (filter (fun i => x i ≠ y i) univ) + card (filter (fun i => y i ≠ z i) univ)
[PROOFSTEP]
refine le_trans (card_mono ?_) (card_union_le _ _)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun i => x i ≠ y i) univ ∪ filter (fun i => y i ≠ z i) univ
[PROOFSTEP]
rw [← filter_or]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun a => x a ≠ y a ∨ y a ≠ z a) univ
[PROOFSTEP]
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist z x + hammingDist z y
[PROOFSTEP]
rw [hammingDist_comm z]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y
[PROOFSTEP]
exact hammingDist_triangle _ _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist y z
[PROOFSTEP]
rw [hammingDist_comm y]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y
[PROOFSTEP]
exact hammingDist_triangle _ _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
⊢ swap hammingDist = hammingDist
[PROOFSTEP]
funext x y
[GOAL]
case h.h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y
[PROOFSTEP]
exact hammingDist_comm _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 → x = y
[PROOFSTEP]
simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ, forall_true_left,
  imp_self]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist x y = 0
[PROOFSTEP]
rw [H]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist y y = 0
[PROOFSTEP]
exact hammingDist_self _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ 0 = hammingDist x y ↔ x = y
[PROOFSTEP]
rw [eq_comm, hammingDist_eq_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ 0 < hammingDist x y ↔ x ≠ y
[PROOFSTEP]
rw [← hammingDist_ne_zero, iff_not_comm, not_lt, le_zero_iff]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y < 1 ↔ x = y
[PROOFSTEP]
rw [Nat.lt_one_iff, hammingDist_eq_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x
[PROOFSTEP]
rw [hammingDist_comm, hammingDist_zero_right]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) ≤ hammingNorm x
[PROOFSTEP]
simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf₁ : ∀ (i : ι), Injective (f i)
hf₂ : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) = hammingNorm x
[PROOFSTEP]
simpa only [← hammingDist_zero_right, hf₂] using hammingDist_comp f hf₁ (y := fun _ ↦ 0)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝⁴ : (i : ι) → DecidableEq (γ i)
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (γ i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0
[PROOFSTEP]
simp_rw [smul_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝⁴ : (i : ι) → DecidableEq (γ i)
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (γ i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0
[PROOFSTEP]
simp_rw [smul_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝¹ : (i : ι) → DecidableEq (γ i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (x - y)
[PROOFSTEP]
simp_rw [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), dist x x = 0
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming x)) = 0
[PROOFSTEP]
exact_mod_cast hammingDist_self
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), dist x y = dist y x
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) = ↑(hammingDist (↑ofHamming y) (↑ofHamming x))
[PROOFSTEP]
exact_mod_cast hammingDist_comm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β), dist x z ≤ dist x y + dist y z
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β),
    ↑(hammingDist (↑ofHamming x) (↑ofHamming z)) ≤
      ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) + ↑(hammingDist (↑ofHamming y) (↑ofHamming z))
[PROOFSTEP]
exact_mod_cast hammingDist_triangle
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝¹ x✝ : Hamming β
⊢ (fun x y => ↑{ val := dist x y, property := (_ : 0 ≤ dist x y) }) x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔
    ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) →
    ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s
[PROOFSTEP]
refine' fun hs => ⟨1, zero_lt_one, fun hab => _⟩
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑(hammingDist (↑ofHamming a✝) (↑ofHamming b✝)) < 1
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
rw_mod_cast [hammingDist_lt_one] at hab
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑ofHamming a✝ = ↑ofHamming b✝
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
rw [ofHamming_inj, ← mem_idRel] at hab
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : (a✝, b✝) ∈ idRel
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
exact hs hab
[GOAL]
case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)
[PROOFSTEP]
rintro ⟨_, hε, hs⟩ ⟨_, _⟩ hab
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : (fst✝, snd✝) ∈ idRel
⊢ (fst✝, snd✝) ∈ s
[PROOFSTEP]
rw [mem_idRel] at hab
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ (fst✝, snd✝) ∈ s
[PROOFSTEP]
rw [hab]
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ (snd✝, snd✝) ∈ s
[PROOFSTEP]
refine' hs (lt_of_eq_of_lt _ hε)
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ ↑(hammingDist (↑ofHamming snd✝) (↑ofHamming snd✝)) = 0
[PROOFSTEP]
exact_mod_cast hammingDist_self _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ (Bornology.cobounded (Hamming β)).sets =
    {s | ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → dist x y ≤ C}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔
    x✝ ∈ {s | ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → dist x y ≤ C}
[PROOFSTEP]
push_cast
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔
    x✝ ∈
      {s |
        ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) ≤ C}
[PROOFSTEP]
refine' iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => _⟩
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝⁴ : Set (Hamming β)
x✝³ : Hamming β
x✝² : x✝³ ∈ x✝⁴ᶜ
x✝¹ : Hamming β
x✝ : x✝¹ ∈ x✝⁴ᶜ
⊢ ↑(hammingDist (↑ofHamming x✝³) (↑ofHamming x✝¹)) ≤ ↑(Fintype.card ι)
[PROOFSTEP]
exact_mod_cast hammingDist_le_card_fintype
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddCommGroup (β i)
⊢ ∀ (x y : Hamming β), dist x y = ‖x - y‖
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddCommGroup (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) = ↑(hammingNorm (↑ofHamming (x - y)))
[PROOFSTEP]
exact_mod_cast hammingDist_eq_hammingNorm