[GOAL]
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = a + a
[PROOFSTEP]
rw [← two_mul]
[GOAL]
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = 2 * a
[PROOFSTEP]
exact Eq.symm
[GOAL]
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
hx : x ∈ 𝓞 K
⊢ IsIntegral ℤ { val := x, property := hx }
[PROOFSTEP]
obtain ⟨P, hPm, hP⟩ := hx
[GOAL]
case intro.intro
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
P : Polynomial ℤ
hPm : Polynomial.Monic P
hP : Polynomial.eval₂ (algebraMap ℤ K) x P = 0
⊢ IsIntegral ℤ { val := x, property := (_ : ∃ p, Polynomial.Monic p ∧ Polynomial.eval₂ (algebraMap ℤ K) x p = 0) }
[PROOFSTEP]
refine' ⟨P, hPm, _⟩
[GOAL]
case intro.intro
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
P : Polynomial ℤ
hPm : Polynomial.Monic P
hP : Polynomial.eval₂ (algebraMap ℤ K) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ { x // x ∈ 𝓞 K })
      { val := x, property := (_ : ∃ p, Polynomial.Monic p ∧ Polynomial.eval₂ (algebraMap ℤ K) x p = 0) } P =
    0
[PROOFSTEP]
rw [← Polynomial.aeval_def, ← Subalgebra.coe_eq_zero, Polynomial.aeval_subalgebra_coe, Polynomial.aeval_def,
  Subtype.coe_mk, hP]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
⊢ ↑((fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1) = ↑1
[PROOFSTEP]
simp only [Subtype.coe_mk, Subalgebra.coe_one, map_one]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
x y : { x // x ∈ 𝓞 K }
⊢ ↑(OneHom.toFun
        { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
          map_one' :=
            (_ :
              (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 = 1) }
        (x * y)) =
    ↑(OneHom.toFun
          { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
            map_one' :=
              (_ :
                (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 =
                  1) }
          x *
        OneHom.toFun
          { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
            map_one' :=
              (_ :
                (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 =
                  1) }
          y)
[PROOFSTEP]
simp only [Subalgebra.coe_mul, map_mul, Subtype.coe_mk]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun k =>
                  { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                map_one' :=
                  (_ :
                    (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : { x // x ∈ 𝓞 K }),
                  OneHom.toFun
                      {
                        toFun := fun k =>
                          { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                        map_one' :=
                          (_ :
                            (fun k =>
                                  { val := ↑(algebraMap K L) ↑k,
                                    property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        y) })
        0) =
    ↑0
[PROOFSTEP]
simp only [Subtype.coe_mk, Subalgebra.coe_zero, map_zero]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
x y : { x // x ∈ 𝓞 K }
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun k =>
                  { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                map_one' :=
                  (_ :
                    (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : { x // x ∈ 𝓞 K }),
                  OneHom.toFun
                      {
                        toFun := fun k =>
                          { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                        map_one' :=
                          (_ :
                            (fun k =>
                                  { val := ↑(algebraMap K L) ↑k,
                                    property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        y) })
        (x + y)) =
    ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun k =>
                    { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                  map_one' :=
                    (_ :
                      (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : { x // x ∈ 𝓞 K }),
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun k =>
                    { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                  map_one' :=
                    (_ :
                      (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : { x // x ∈ 𝓞 K }),
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          y) })
          y)
[PROOFSTEP]
simp only [map_add, Subalgebra.coe_add, Subtype.coe_mk]
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
⊢ ¬IsField { x // x ∈ 𝓞 K }
[PROOFSTEP]
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
h_inj : Injective ↑(algebraMap ℤ { x // x ∈ 𝓞 K })
⊢ ¬IsField { x // x ∈ 𝓞 K }
[PROOFSTEP]
intro hf
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
h_inj : Injective ↑(algebraMap ℤ { x // x ∈ 𝓞 K })
hf : IsField { x // x ∈ 𝓞 K }
⊢ False
[PROOFSTEP]
exact Int.not_isField (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ↑(integralBasis K)) ↔ x ∈ 𝓞 K
[PROOFSTEP]
rw [integralBasis, Basis.localizationLocalization_span, Subalgebra.range_isScalarTower_toAlgHom,
  Subalgebra.mem_toSubmodule]
[GOAL]
⊢ FiniteDimensional ℚ ℚ
[PROOFSTEP]
convert (inferInstance : FiniteDimensional ℚ ℚ)
[GOAL]
f : Polynomial ℚ
hf : Fact (Irreducible f)
⊢ FiniteDimensional ℚ (AdjoinRoot f)
[PROOFSTEP]
convert (AdjoinRoot.powerBasis hf.out.ne_zero).finiteDimensional


[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ { obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.map (𝟙 x) =
    𝟙 ({ obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.obj x)
[PROOFSTEP]
change (Path.Homotopic.pi fun i => 𝟙 (x i)) = _
[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ (Path.Homotopic.pi fun i => 𝟙 (x i)) = 𝟙 ({ obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.obj x)
[PROOFSTEP]
simp only [FundamentalGroupoid.id_eq_path_refl, Path.Homotopic.pi_lift]
[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Quotient.mk (Path.Homotopic.setoid (fun i => x i) fun i => x i) (Path.pi fun i => Path.refl (x i)) = 𝟙 x
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))
[PROOFSTEP]
change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _
[GOAL]
I : Type u
X : I → TopCat
⊢ piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 ((i : I) → ↑(π.obj (X i)))
[PROOFSTEP]
apply CategoryTheory.Functor.ext ?_ ?_
[GOAL]
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : (i : I) → ↑(π.obj (X i))),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1
[PROOFSTEP]
intros
[GOAL]
I : Type u
X : I → TopCat
X✝ : (i : I) → ↑(π.obj (X i))
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom
          (_ :
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 =
              (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1) ≫
        (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫
          CategoryTheory.eqToHom
            (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y)
[PROOFSTEP]
intros
[GOAL]
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ =
    CategoryTheory.eqToHom
        (_ :
          (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ =
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝) ≫
      (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫
        CategoryTheory.eqToHom
          (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y✝ = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y✝)
[PROOFSTEP]
ext
[GOAL]
case w
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
i✝ : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ i✝ =
    (CategoryTheory.eqToHom
          (_ :
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ =
              (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝) ≫
        (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫
          CategoryTheory.eqToHom
            (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y✝ = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y✝))
      i✝
[PROOFSTEP]
simp
[GOAL]
I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ≫ piToPiTop X = 𝟙 (π.obj (TopCat.of ((i : I) → ↑(X i))))
[PROOFSTEP]
change CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 _
[GOAL]
I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
[PROOFSTEP]
apply CategoryTheory.Functor.ext
[GOAL]
case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
            CategoryTheory.eqToHom
              (_ :
                (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y =
                  (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y))
    _auto✝
[PROOFSTEP]
intro _ _ f
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫
      (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
        CategoryTheory.eqToHom
          (_ :
            (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y✝ =
              (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y✝)
[PROOFSTEP]
suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
[GOAL]
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
this : Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫
      (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
        CategoryTheory.eqToHom
          (_ :
            (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y✝ =
              (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y✝)
[PROOFSTEP]
simpa
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f
[PROOFSTEP]
change Path.Homotopic.pi (fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = _
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (Path.Homotopic.pi fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = f
[PROOFSTEP]
simp
[GOAL]
case h_obj
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1
[PROOFSTEP]
intros
[GOAL]
case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π
[PROOFSTEP]
apply Limits.preservesLimitOfPreservesLimitCone (TopCat.piFanIsLimit.{u, u} X)
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))
[PROOFSTEP]
apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
[PROOFSTEP]
simp only [coneDiscreteComp_obj_mapCone]
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X))
[PROOFSTEP]
apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i => π.obj (X i))
[PROOFSTEP]
exact Grpd.piLimitFanIsLimit _
[GOAL]
A B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    { obj := fun g => g,
            map := fun {x y} p =>
              match x, y, p with
              | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun g => g,
              map := fun {x y} p =>
                match x, y, p with
                | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.obj
          X)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩
[GOAL]
case mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ { obj := fun g => g,
          map := fun {x y} p =>
            match x, y, p with
            | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.map
      (𝟙 (x₀, x₁)) =
    𝟙
      ({ obj := fun g => g,
            map := fun {x y} p =>
              match x, y, p with
              | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.obj
        (x₀, x₁))
[PROOFSTEP]
simp only [CategoryTheory.prod_id, FundamentalGroupoid.id_eq_path_refl]
[GOAL]
case mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 (x₀, x₁)
[PROOFSTEP]
rfl
[GOAL]
A B : TopCat
⊢ prodToProdTop A B ≫ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) =
    𝟙 (CategoryTheory.Grpd.of (↑(π.obj A) × ↑(π.obj B)))
[PROOFSTEP]
change prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 _
[GOAL]
A B : TopCat
⊢ prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) = 𝟭 (↑(π.obj A) × ↑(π.obj B))
[PROOFSTEP]
apply CategoryTheory.Functor.hext
[GOAL]
case h_obj
A B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X =
      (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X
[PROOFSTEP]
intros
[GOAL]
case h_obj
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝ =
    (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝
[PROOFSTEP]
ext
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝).fst =
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).fst
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝).snd =
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).snd
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj X✝ = X✝.fst
[PROOFSTEP]
rfl
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj X✝ = X✝.snd
[PROOFSTEP]
rfl
[GOAL]
case h_map
A B : TopCat
⊢ ∀ (X Y : ↑(π.obj A) × ↑(π.obj B)) (f : X ⟶ Y),
    HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map f)
      ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map f)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩
[GOAL]
case h_map.mk.mk.mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
y₀ : ↑(π.obj A)
y₁ : ↑(π.obj B)
f₀ : (x₀, x₁).fst ⟶ (y₀, y₁).fst
f₁ : (x₀, x₁).snd ⟶ (y₀, y₁).snd
⊢ HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map (f₀, f₁))
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
[PROOFSTEP]
have :
  Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
  And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
[GOAL]
case h_map.mk.mk.mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
y₀ : ↑(π.obj A)
y₁ : ↑(π.obj B)
f₀ : (x₀, x₁).fst ⟶ (y₀, y₁).fst
f₁ : (x₀, x₁).snd ⟶ (y₀, y₁).snd
this :
  Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁
⊢ HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map (f₀, f₁))
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
[PROOFSTEP]
simpa
[GOAL]
A B : TopCat
⊢ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ≫ prodToProdTop A B = 𝟙 (π.obj (TopCat.of (↑A × ↑B)))
[PROOFSTEP]
change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _
[GOAL]
A B : TopCat
⊢ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B = 𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))
[PROOFSTEP]
apply CategoryTheory.Functor.hext
[GOAL]
case h_obj
A B : TopCat
⊢ ∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))),
    (CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X =
      (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X
[PROOFSTEP]
intros
[GOAL]
case h_obj
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝ =
    (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝
[PROOFSTEP]
apply Prod.ext
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝).fst =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).fst
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝).snd =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).snd
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (projLeft A B).obj X✝ = X✝.fst
[PROOFSTEP]
rfl
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (projRight A B).obj X✝ = X✝.snd
[PROOFSTEP]
rfl
[GOAL]
case h_map
A B : TopCat
⊢ ∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y),
    HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
      ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
⊢ HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
have := Path.Homotopic.prod_projLeft_projRight f
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f
⊢ HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
simp only [CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.prod'_obj, prodToProdTop_obj,
  CategoryTheory.Functor.comp_map, CategoryTheory.Functor.prod'_map, projLeft_map, projRight_map,
  CategoryTheory.Functor.id_obj, CategoryTheory.Functor.id_map, heq_eq_eq]
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f
⊢ (prodToProdTop A B).map (Path.Homotopic.projLeft f, Path.Homotopic.projRight f) = f
[PROOFSTEP]
apply this