[GOAL]
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
⊢ A₁.fst.unop = A₂.fst.unop
[PROOFSTEP]
rw [h₁]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : e A₁ ≫ eqToHom (_ : A₁.fst.unop = A₂.fst.unop) = e A₂
⊢ A₁ = A₂
[PROOFSTEP]
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
h₁ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst = A₂.fst
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom (_ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop = A₂.fst.unop) =
    e A₂
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = A₂
[PROOFSTEP]
rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : Δ.unop ⟶ Δ₂.unop
hα₂ : Epi α₂
h₁ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only at h₁
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : Δ.unop ⟶ Δ₂.unop
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
subst h₁
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
α₂ : Δ.unop ⟶ Δ₁.unop
hα₂ : Epi α₂
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₁, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
α₂ : Δ.unop ⟶ Δ₁.unop
hα₂ : Epi α₂
h₂ : α₁ = α₂
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only [h₂]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Function.Injective fun A =>
    { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
      snd := ↑(Hom.toOrderHom (e A)) }
[PROOFSTEP]
rintro ⟨Δ₁, α₁⟩ ⟨Δ₂, α₂⟩ h₁
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂ : { α // Epi α }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
⊢ { fst := Δ₁, snd := α₁ } = { fst := Δ₂, snd := α₂ }
[PROOFSTEP]
induction' Δ₁ using Opposite.rec with Δ₁
[GOAL]
case mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := Δ₂, snd := α₂ }
[PROOFSTEP]
induction' Δ₂ using Opposite.rec with Δ₂
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
have h₂ : Δ₁ = Δ₂ := by
  ext1
  simpa only [Fin.mk_eq_mk] using h₁.1
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ Δ₁ = Δ₂
[PROOFSTEP]
ext1
[GOAL]
case a
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ len Δ₁ = len Δ₂
[PROOFSTEP]
simpa only [Fin.mk_eq_mk] using h₁.1
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
h₂ : Δ₁ = Δ₂
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
subst h₂
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₁ }, snd := α₂ }
[PROOFSTEP]
refine' ext _ _ rfl _
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ e { fst := { unop := Δ₁ }, snd := α₁ } ≫
      eqToHom (_ : { fst := { unop := Δ₁ }, snd := α₁ }.fst.unop = { fst := { unop := Δ₁ }, snd := α₂ }.fst.unop) =
    e { fst := { unop := Δ₁ }, snd := α₂ }
[PROOFSTEP]
ext : 2
[GOAL]
case mk.mk.mk.mk.a.h
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ ↑(Hom.toOrderHom
        (e { fst := { unop := Δ₁ }, snd := α₁ } ≫
          eqToHom
            (_ : { fst := { unop := Δ₁ }, snd := α₁ }.fst.unop = { fst := { unop := Δ₁ }, snd := α₂ }.fst.unop))) =
    ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
[PROOFSTEP]
exact eq_of_heq h₁.2
[GOAL]
C : Type u_1
inst✝ : Category.{?u.3923, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Epi (𝟙 Δ.unop)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ A.fst = Δ
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → A.fst = Δ
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ A.fst = Δ
[PROOFSTEP]
dsimp at h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ
[PROOFSTEP]
rw [h]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
[PROOFSTEP]
rfl
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → EqId A
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ EqId A
[PROOFSTEP]
rcases A with ⟨_, ⟨f, hf⟩⟩
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : { fst := fst✝, snd := { val := f, property := hf } }.fst = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
simp only at h
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : fst✝ = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
subst h
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
refine' ext _ _ rfl _
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
[PROOFSTEP]
haveI := hf
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
[PROOFSTEP]
simp only [eqToHom_refl, comp_id]
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } = e (id fst✝)
[PROOFSTEP]
exact eq_id_of_epi f
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ len A.fst.unop = len Δ.unop
[PROOFSTEP]
rw [eqId_iff_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ len A.fst.unop = len Δ.unop
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → len A.fst.unop = len Δ.unop
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ len A.fst.unop = len Δ.unop
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → A.fst = Δ
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst = Δ
[PROOFSTEP]
rw [← unop_inj_iff]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst.unop = Δ.unop
[PROOFSTEP]
ext
[GOAL]
case mpr.a
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len A.fst.unop = len Δ.unop
[PROOFSTEP]
exact h
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
rw [eqId_iff_len_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop ↔ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len Δ.unop ≤ len A.fst.unop → len A.fst.unop = len Δ.unop
[PROOFSTEP]
exact le_antisymm (len_le_of_epi (inferInstance : Epi A.e))
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ Mono (e A)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → Mono (e A)
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ Mono (e A)
[PROOFSTEP]
dsimp at h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono (e A)
[PROOFSTEP]
subst h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (e (id Δ))
[PROOFSTEP]
dsimp only [id, e]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 Δ.unop)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono (e A) → EqId A
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ EqId A
[PROOFSTEP]
rw [eqId_iff_len_le]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
exact len_le_of_mono h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
dsimp only [ιSummand, Iso.hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιCoprod s.N A ≫ (iso s Δ).hom = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
erw [colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
n : ℕ
⊢ ιSummand s (IndexSet.id (op [n])) = ι s n
[PROOFSTEP]
erw [ιSummand_eq, X.map_id, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
n : ℕ
⊢ ι s (len (IndexSet.id (op [n])).fst.unop) = ι s n
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ NatTrans.app f Δ = φ s f (len A.fst.unop) ≫ Y.map (IndexSet.e A).op
[PROOFSTEP]
simp only [ιSummand_eq_assoc, φ, assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op ≫ NatTrans.app f Δ =
    ι s (len A.fst.unop) ≫ NatTrans.app f (op [len A.fst.unop]) ≫ Y.map (IndexSet.e A).op
[PROOFSTEP]
erw [NatTrans.naturality]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ f = g
[PROOFSTEP]
rw [← cancel_epi (s.iso Δ).hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ (iso s Δ).hom ≫ f = (iso s Δ).hom ≫ g
[PROOFSTEP]
ext A
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
A : IndexSet Δ
⊢ Sigma.ι (summand s.N Δ) A ≫ (iso s Δ).hom ≫ f = Sigma.ι (summand s.N Δ) A ≫ (iso s Δ).hom ≫ g
[PROOFSTEP]
simpa only [ιSummand_eq, iso_hom, map, colimit.ι_desc_assoc, Cofan.mk_ι_app] using h A
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
⊢ f = g
[PROOFSTEP]
ext Δ
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ NatTrans.app f Δ = NatTrans.app g Δ
[PROOFSTEP]
apply s.hom_ext'
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ NatTrans.app f Δ = ιSummand s A ≫ NatTrans.app g Δ
[PROOFSTEP]
intro A
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ NatTrans.app f Δ = ιSummand s A ≫ NatTrans.app g Δ
[PROOFSTEP]
induction' Δ using Opposite.rec with Δ
[GOAL]
case h.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝ : IndexSet Δ✝
Δ : SimplexCategory
A : IndexSet { unop := Δ }
⊢ ιSummand s A ≫ NatTrans.app f { unop := Δ } = ιSummand s A ≫ NatTrans.app g { unop := Δ }
[PROOFSTEP]
induction' Δ using SimplexCategory.rec with n
[GOAL]
case h.h.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ NatTrans.app f { unop := [n] } = ιSummand s A ≫ NatTrans.app g { unop := [n] }
[PROOFSTEP]
dsimp
[GOAL]
case h.h.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ NatTrans.app f { unop := [n] } = ιSummand s A ≫ NatTrans.app g { unop := [n] }
[PROOFSTEP]
simp only [s.ιSummand_comp_app, h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ ιSummand s A ≫ desc s Δ F = F A
[PROOFSTEP]
dsimp only [ιSummand, desc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ (ιCoprod s.N A ≫ (iso s Δ).hom) ≫ (iso s Δ).inv ≫ Sigma.desc F = F A
[PROOFSTEP]
simp only [assoc, Iso.hom_inv_id_assoc, ιCoprod]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ Sigma.ι (summand s.N Δ) A ≫ Sigma.desc F = F A
[PROOFSTEP]
erw [colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ)
[PROOFSTEP]
convert (inferInstance : IsIso ((s.iso Δ).hom ≫ e.hom.app Δ))
[GOAL]
case h.e'_5
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
⊢ map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ = (iso s Δ).hom ≫ NatTrans.app e.hom Δ
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
b✝ : IndexSet Δ
⊢ Sigma.ι (summand (fun n => N s n) Δ) b✝ ≫ map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ =
    Sigma.ι (summand (fun n => N s n) Δ) b✝ ≫ (iso s Δ).hom ≫ NatTrans.app e.hom Δ
[PROOFSTEP]
simp [map]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ ιSummand s A ≫ X.map p = ιSummand s (IndexSet.epiComp A p)
[PROOFSTEP]
dsimp [ιSummand]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (Sigma.ι (fun A => N s (len A.fst.unop)) A ≫ Sigma.desc fun A => ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op) ≫
      X.map p =
    Sigma.ι (fun A => N s (len A.fst.unop)) (IndexSet.epiComp A p) ≫
      Sigma.desc fun A => ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
erw [colimit.ι_desc, colimit.ι_desc, Cofan.mk_ι_app, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len { as := A }.as.fst.unop) ≫ X.map (IndexSet.e { as := A }.as).op) ≫ X.map p =
    ι s (len { as := IndexSet.epiComp A p }.as.fst.unop) ≫ X.map (IndexSet.e { as := IndexSet.epiComp A p }.as).op
[PROOFSTEP]
dsimp only [IndexSet.epiComp, IndexSet.e]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len A.fst.unop) ≫ X.map (↑A.snd).op) ≫ X.map p = ι s (len A.fst.unop) ≫ X.map (p.unop ≫ ↑A.snd).op
[PROOFSTEP]
rw [op_comp, X.map_comp, assoc, Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : Hom S₁ S₂
h : ∀ (n : ℕ), f Φ₁ n = f Φ₂ n
⊢ Φ₁ = Φ₂
[PROOFSTEP]
rcases Φ₁ with ⟨F₁, f₁, c₁⟩
[GOAL]
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₂ : Hom S₁ S₂
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f Φ₂ n
⊢ mk F₁ f₁ = Φ₂
[PROOFSTEP]
rcases Φ₂ with ⟨F₂, f₂, c₂⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
⊢ mk F₁ f₁ = mk F₂ f₂
[PROOFSTEP]
have h' : f₁ = f₂ := by
  ext
  apply h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
⊢ f₁ = f₂
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
x✝ : ℕ
⊢ f₁ x✝ = f₂ x✝
[PROOFSTEP]
apply h
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
h' : f₁ = f₂
⊢ mk F₁ f₁ = mk F₂ f₂
[PROOFSTEP]
subst h'
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ mk F₁ f₁ = mk F₂ f₁
[PROOFSTEP]
simp only [mk.injEq, and_true]
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ F₁ = F₂
[PROOFSTEP]
apply S₁.s.hom_ext
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ ∀ (n : ℕ), Splitting.φ S₁.s F₁ n = Splitting.φ S₁.s F₂ n
[PROOFSTEP]
intro n
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
n : ℕ
⊢ Splitting.φ S₁.s F₁ n = Splitting.φ S₁.s F₂ n
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
n : ℕ
⊢ Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n])
[PROOFSTEP]
rw [c₁, c₂]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.183784, u_1} C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝ ⟶ Y✝
Φ₂₃ : Y✝ ⟶ Z✝
n : ℕ
⊢ Splitting.ι X✝.s n ≫ NatTrans.app (Φ₁₂.F ≫ Φ₂₃.F) (op [n]) =
    (fun n => Split.Hom.f Φ₁₂ n ≫ Split.Hom.f Φ₂₃ n) n ≫ Splitting.ι Z✝.s n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.183784, u_1} C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝ ⟶ Y✝
Φ₂₃ : Y✝ ⟶ Z✝
n : ℕ
⊢ Splitting.ι X✝.s n ≫ NatTrans.app Φ₁₂.F (op [n]) ≫ NatTrans.app Φ₂₃.F (op [n]) =
    (Split.Hom.f Φ₁₂ n ≫ Split.Hom.f Φ₂₃ n) ≫ Splitting.ι Z✝.s n
[PROOFSTEP]
simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Hom.f Φ₁ n = Hom.f Φ₂ n
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Splitting.ιSummand S₁.s A ≫ NatTrans.app Φ.F Δ = Hom.f Φ (len A.fst.unop) ≫ Splitting.ιSummand S₂.s A
[PROOFSTEP]
erw [S₁.s.ιSummand_eq, S₂.s.ιSummand_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]


[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rw [simply_connected_def, equiv_punit_iff_unique]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (Nonempty (FundamentalGroupoid X) ∧ ∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SimplyConnectedSpace X
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rw [simply_connected_iff_unique_homotopic] at *
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
tauto
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y → PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
intro
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
constructor
[GOAL]
case left
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y
[PROOFSTEP]
infer_instance
[GOAL]
case right
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
infer_instance
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
[PROOFSTEP]
cases h
[GOAL]
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
[PROOFSTEP]
rw [simply_connected_iff_unique_homotopic]
[GOAL]
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), Path.Homotopic p₁ p₂
[PROOFSTEP]
convert simply_connected_iff_paths_homotopic (Y := Y)
[GOAL]
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), Path.Homotopic p₁ p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)
[PROOFSTEP]
simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]
[GOAL]
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), Path.Homotopic p₁ p₂) ↔ ∀ (x y : Path a✝¹ a✝), Setoid.Rel (Path.Homotopic.setoid a✝¹ a✝) x y
[PROOFSTEP]
rfl


[GOAL]
x : SimplexCategory
⊢ Fintype (ConcreteCategory.forget.obj x)
[PROOFSTEP]
change (Fintype (Fin _))
[GOAL]
x : SimplexCategory
⊢ Fintype (Fin (len x + 1))
[PROOFSTEP]
infer_instance
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ (fun i => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g j) ∈ toTopObj y
[PROOFSTEP]
simp only [Finset.sum_congr, toTopObj, Set.mem_setOf]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ ∑ i : (forget SimplexCategory).obj y, ∑ x_1 in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
[PROOFSTEP]
rw [← Finset.sum_biUnion]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
have hg := g.2
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ↑g ∈ toTopObj x
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
dsimp [toTopObj] at hg
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ∑ i : (forget SimplexCategory).obj x, ↑g i = 1
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
convert hg
[GOAL]
case h.e'_2.h
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ∑ i : (forget SimplexCategory).obj x, ↑g i = 1
⊢ (Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ) = Finset.univ
[PROOFSTEP]
simp [Finset.eq_univ_iff_forall]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
intro i _ j _ h
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
⊢ (Disjoint on fun i => Finset.filter (fun k => ↑f k = i) Finset.univ) i j
[PROOFSTEP]
rw [Function.onFun, disjoint_iff_inf_le]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
⊢ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ ≤ ⊥
[PROOFSTEP]
intro e he
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ e ∈ ⊥
[PROOFSTEP]
simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ False
[PROOFSTEP]
apply h
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ i = j
[PROOFSTEP]
simp only [Finset.mem_univ, forall_true_left, ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
  Finset.mem_filter, true_and] at he
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : ↑f e = i ∧ ↑f e = j
⊢ i = j
[PROOFSTEP]
rw [← he.1, he.2]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
⊢ Continuous (toTopMap f)
[PROOFSTEP]
refine' Continuous.subtype_mk (continuous_pi fun i => _) _
[GOAL]
x y : SimplexCategory
f : x ⟶ y
i : (forget SimplexCategory).obj y
⊢ Continuous fun a => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑a j
[PROOFSTEP]
dsimp only [coe_toTopMap]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
i : (forget SimplexCategory).obj y
⊢ Continuous fun a => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑a j
[PROOFSTEP]
exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)
[GOAL]
X✝ Y✝ : SimplexCategory
f : X✝ ⟶ Y✝
⊢ Continuous (toTopMap f)
[PROOFSTEP]
continuity
[GOAL]
⊢ ∀ (X : SimplexCategory),
    { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 X) =
      𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X)
[PROOFSTEP]
intro Δ
[GOAL]
Δ : SimplexCategory
⊢ { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ) =
    𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
[PROOFSTEP]
ext f
[GOAL]
case w
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
⊢ ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f =
    ↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f
[PROOFSTEP]
apply toTopObj.ext
[GOAL]
case w.a
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f) =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f)
[PROOFSTEP]
funext i
[GOAL]
case w.a.h
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
i : (forget SimplexCategory).obj Δ
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f) i =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f) i
[PROOFSTEP]
change (Finset.univ.filter fun k => k = i).sum _ = _
[GOAL]
case w.a.h
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
i : (forget SimplexCategory).obj Δ
⊢ ∑ j in Finset.filter (fun k => k = i) Finset.univ, ↑f j =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f) i
[PROOFSTEP]
simp [Finset.sum_filter, CategoryTheory.id_apply]
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g) =
    { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
      { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g
[PROOFSTEP]
ext h
[GOAL]
case w
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
⊢ ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h =
    ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
          { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
      h
[PROOFSTEP]
apply toTopObj.ext
[GOAL]
case w.a
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h) =
    ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
            { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
        h)
[PROOFSTEP]
funext i
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h)
      i =
    ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
              { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
          h)
      i
[PROOFSTEP]
dsimp
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(↑(ContinuousMap.mk (toTopMap (Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))))) h) i =
    ↑(↑(ContinuousMap.mk (toTopMap f) ≫ ContinuousMap.mk (toTopMap g)) h) i
[PROOFSTEP]
rw [CategoryTheory.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, ContinuousMap.coe_mk]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(toTopMap (Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) h) i = ↑(toTopMap g (toTopMap f h)) i
[PROOFSTEP]
simp only [coe_toTopMap]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∑ j in Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ,
      ↑h j =
    ∑ x in Finset.filter (fun k => ↑g k = i) Finset.univ, ∑ j in Finset.filter (fun k => ↑f k = x) Finset.univ, ↑h j
[PROOFSTEP]
erw [← Finset.sum_biUnion]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∑ j in Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ,
      ↑h j =
    ∑ x in
      Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
        Finset.filter (fun k => ↑f k = x) Finset.univ,
      ↑h x
[PROOFSTEP]
apply Finset.sum_congr
[GOAL]
case w.a.h.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ =
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj X✝
hj : j ∈ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ
⊢ j ∈
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
simpa using hj
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj X✝
hj :
  j ∈
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
⊢ j ∈ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ
[PROOFSTEP]
simpa using hj
[GOAL]
case w.a.h.a
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∀ (x : (forget SimplexCategory).obj X✝),
    (x ∈
        Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
          Finset.filter (fun k => ↑f k = x) Finset.univ) →
      ↑h x = ↑h x
[PROOFSTEP]
tauto
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ Set.PairwiseDisjoint ↑(Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
    Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
intro j _ k _ h
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
⊢ (Disjoint on fun x => Finset.filter (fun k => ↑f k = x) Finset.univ) j k
[PROOFSTEP]
rw [Function.onFun, disjoint_iff_inf_le]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
⊢ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ ≤ ⊥
[PROOFSTEP]
intro e he
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ e ∈ ⊥
[PROOFSTEP]
simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ j = k
[PROOFSTEP]
simp only [Finset.mem_univ, forall_true_left, ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
  Finset.mem_filter, true_and] at he
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : ↑f e = j ∧ ↑f e = k
⊢ j = k
[PROOFSTEP]
rw [← he.1, he.2]


[GOAL]
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ↑(starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
refine Submodule.span_induction hx ?_ ?_ (fun _ _ hx hy => ?_) (fun a _ hx => ?_)
[GOAL]
case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ∀ (x : (K →+* ℂ) → ℂ),
    x ∈ Set.range ↑(canonicalEmbedding K) → ↑(starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case refine_1.intro
K : Type u_1
inst✝ : Field K
x✝ : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x✝ ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
x : K
⊢ ↑(starRingEnd ℂ) (↑(canonicalEmbedding K) x φ) = ↑(canonicalEmbedding K) x (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
[GOAL]
case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
⊢ ↑(starRingEnd ℂ) (OfNat.ofNat 0 φ) = OfNat.ofNat 0 (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.zero_apply, Pi.zero_apply, map_zero]
[GOAL]
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
x✝¹ x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
hy : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑(starRingEnd ℂ) ((x✝¹ + x✝) φ) = (x✝¹ + x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
[GOAL]
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
a : ℝ
x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑(starRingEnd ℂ) ((a • x✝) φ) = (a • x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
[GOAL]
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ↑(canonicalEmbedding K))
a : ℝ
x✝ : (K →+* ℂ) → ℂ
hx : ↑(starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)
⊢ ↑a * ↑(starRingEnd ℂ) (x✝ φ) = (a • x✝) (ComplexEmbedding.conjugate φ)
[PROOFSTEP]
exact congrArg ((a : ℂ) * ·) hx
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖↑(canonicalEmbedding K) x‖₊ = Finset.sup Finset.univ fun φ => ‖↑φ x‖₊
[PROOFSTEP]
simp_rw [Pi.nnnorm_def, apply_at]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
obtain hr | hr := lt_or_le r 0
[GOAL]
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
refine iff_of_false ?_ ?_
[GOAL]
case inl.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖↑(canonicalEmbedding K) x‖ ≤ r
case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
exact (hr.trans_le (norm_nonneg _)).not_le
[GOAL]
case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
exact fun h => hr.not_le (le_trans (norm_nonneg _) (h φ))
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
lift r to NNReal using hr
[GOAL]
case inr.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ ‖↑(canonicalEmbedding K) x‖ ≤ ↑r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ ↑r
[PROOFSTEP]
simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
obtain hr | _ := lt_or_le r 0
[GOAL]
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
simp [Metric.closedBall_eq_empty.2 hr]
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by intro x;
  rw [← norm_le_iff, mem_closedBall_zero_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
intro x
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
x : K
⊢ ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
[PROOFSTEP]
rw [← norm_le_iff, mem_closedBall_zero_iff]
[GOAL]
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ Set.Finite (↑(integerLattice K) ∩ Metric.closedBall 0 r)
[PROOFSTEP]
convert (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ ↑(integerLattice K) ∩ Metric.closedBall 0 r =
    ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r ↔
    x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_2.h.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r →
    x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩
[GOAL]
case h.e'_2.h.mp.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x : { x // x ∈ 𝓞 K }
hx : ↑(canonicalEmbedding K) (↑(algebraMap { x // x ∈ 𝓞 K } K) x) ∈ Metric.closedBall 0 r
⊢ ↑(canonicalEmbedding K) (↑(algebraMap { x // x ∈ 𝓞 K } K) x) ∈
    ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r}
[PROOFSTEP]
exact ⟨↑x, ⟨SetLike.coe_mem x, fun φ => (heq x).mp hx φ⟩, rfl⟩
[GOAL]
case h.e'_2.h.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
[PROOFSTEP]
rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
[GOAL]
case h.e'_2.h.mpr.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), ↑(canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
x : K
hx1 : IsIntegral ℤ x
hx2 : ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
⊢ ↑(canonicalEmbedding K) x ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
[PROOFSTEP]
exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
classical
  -- Let `B` be the canonical basis of `(K →+* ℂ) → ℂ`. We prove that the determinant of
    -- the image by `canonicalEmbedding` of the integral basis of `K` is nonzero. This
    -- will imply the result.
let B := Pi.basisFun ℂ (K →+* ℂ)
let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
suffices M.det ≠ 0 by
  rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← is_basis_iff_det] at this
  refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
  rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
    -- In order to prove that the determinant is nonzero, we show that it is equal to the
      -- square of the discriminant of the integral basis and thus it is not zero
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom
rw [show M = N.transpose by {ext : 2; rfl
  }]
rw [Matrix.det_transpose, ← @pow_ne_zero_iff ℂ _ _ _ 2 (by norm_num)]
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
exact
  (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ (fun i => integralBasis K (e i))
      RingHom.equivRatAlgHom).symm
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let B := Pi.basisFun ℂ (K →+* ℂ)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
suffices M.det ≠ 0 by
  rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← is_basis_iff_det] at this
  refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
  rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
    -- In order to prove that the determinant is nonzero, we show that it is equal to the
      -- square of the discriminant of the integral basis and thus it is not zero
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this : Matrix.det M ≠ 0
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← is_basis_iff_det] at this
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this :
  (LinearIndependent ℂ fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) ∧
    Submodule.span ℂ (Set.range fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) = ⊤
⊢ Basis (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
refine basisOfLinearIndependentOfCardEqFinrank ((linearIndependent_equiv e.symm).mpr this.1) ?_
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
this :
  (LinearIndependent ℂ fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) ∧
    Submodule.span ℂ (Set.range fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))) = ⊤
⊢ card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }) = finrank ℂ ((K →+* ℂ) → ℂ)
[PROOFSTEP]
rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_fintype_fun_eq_card, Embeddings.card]
  -- In order to prove that the determinant is nonzero, we show that it is equal to the
    -- square of the discriminant of the integral basis and thus it is not zero
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
⊢ Matrix.det M ≠ 0
[PROOFSTEP]
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det M ≠ 0
[PROOFSTEP]
rw [show M = N.transpose by {ext : 2; rfl
  }]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ M = Matrix.transpose N
[PROOFSTEP]
{ext : 2; rfl
}
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ M = Matrix.transpose N
[PROOFSTEP]
ext : 2
[GOAL]
case a.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
i✝ x✝ : K →+* ℂ
⊢ M i✝ x✝ = Matrix.transpose N i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det (Matrix.transpose N) ≠ 0
[PROOFSTEP]
rw [Matrix.det_transpose, ← @pow_ne_zero_iff ℂ _ _ _ 2 (by norm_num)]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 ≠ 0
[PROOFSTEP]
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 = ↑(algebraMap ℚ ℂ) (Algebra.discr ℚ ↑(integralBasis K))
[PROOFSTEP]
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K } :=
  equivOfCardEq (_ : card (K →+* ℂ) = card (Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }))
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Basis.toMatrix B fun i => ↑(canonicalEmbedding K) (↑(integralBasis K) (↑e i))
N : (fun x => Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (Algebra.embeddingsMatrix ℚ ℂ fun i => ↑(integralBasis K) (↑e i)) :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => ↑(integralBasis K) (↑e i)) RingHom.equivRatAlgHom
⊢ Matrix.det N ^ 2 = ↑(algebraMap ℚ ℂ) (Algebra.discr ℚ (↑(integralBasis K) ∘ ↑e.symm.symm))
[PROOFSTEP]
exact
  (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ (fun i => integralBasis K (e i))
      RingHom.equivRatAlgHom).symm
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Free.ChooseBasisIndex ℤ { x // x ∈ 𝓞 K }
⊢ ↑(latticeBasis K) i = ↑(canonicalEmbedding K) (↑(integralBasis K) i)
[PROOFSTEP]
simp only [latticeBasis, integralBasis_apply, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
  Equiv.apply_symm_apply]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (Set.range ↑(latticeBasis K)) ↔ x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [show Set.range (latticeBasis K) = (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ↑(latticeBasis K) =
    ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' Set.range ↑(integralBasis K)
[PROOFSTEP]
rw [← Set.range_comp]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ↑(latticeBasis K) =
    Set.range (↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) ∘ ↑(integralBasis K))
[PROOFSTEP]
exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈
      Submodule.span ℤ
        (↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' Set.range ↑(integralBasis K)) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈
      ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) ''
        ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by ext; exact mem_span_integralBasis K]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) = ↑(𝓞 K)
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
x✝ : K
⊢ x✝ ∈ ↑(Submodule.span ℤ (Set.range ↑(integralBasis K))) ↔ x✝ ∈ ↑(𝓞 K)
[PROOFSTEP]
exact mem_span_integralBasis K
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ↑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) '' ↑(𝓞 K) ↔
    x ∈ ↑(canonicalEmbedding K) '' ↑(𝓞 K)
[PROOFSTEP]
rfl