awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
j : WidePullbackShape ι
⊢ Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
        { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
          π :=
            {
              app := fun (X_1 : WidePullbackShape ι) ↦
                Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                  Functor.obj.{w, v, w, u}
                      (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                    Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                  X_1
                  (terminal.from
                    (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                      (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                  fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
              naturality := ⋯ } })
      (Pi.lift fun (j : ι) ↦ s.π.app (some j))
      (NatTrans.app
        (Cone.π
          { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
            π :=
              {
                app := fun (X_1 : WidePullbackShape ι) ↦
                  Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                    Functor.obj.{w, v, w, u}
                        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                      Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                    X_1
                    (terminal.from
                      (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                    fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                naturality := ⋯ } })
        none))
    (s.π.app none)

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
dsimp : f = Pi.lift fun (j : ι) ↦ s.π.app (some j)
⊢ f = Pi.lift fun (j : ι) ↦ s.π.app (some j)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
h₁ :
  ∀ (j : ι),
    f ≫ Pi.π (fun (x : ι) ↦ X) j =
      CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X) (Pi.lift fun (j : ι) ↦ s.π.app (some j))
        (Pi.π (fun (x : ι) ↦ X) j)
⊢ f = Pi.lift fun (j : ι) ↦ s.π.app (some j)

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
h₁ :
  f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
      (limit.lift (Discrete.functor fun (x : ι) ↦ X) (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j)))
      (Pi.π (fun (x : ι) ↦ X) j)
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X) (Pi.lift fun (j : ι) ↦ s.π.app (some j))
      (Pi.π (fun (x : ι) ↦ X) j)

Tactic:
dsimp only [Limits.Pi.lift]

Premises used: CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j = NatTrans.app (Cone.π (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j))) { as := j }
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
      (limit.lift (Discrete.functor fun (x : ι) ↦ X) (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j)))
      (Pi.π (fun (x : ι) ↦ X) j)

Tactic:
rw [limit.lift_π]

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j = s.π.app (some j)
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j = NatTrans.app (Cone.π (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j))) { as := j }

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
h₁ h₂ :
  f ≫ Pi.π (fun (x : ι) ↦ X) j =
    f ≫
      NatTrans.app
        (Cone.π
          { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
            π :=
              {
                app := fun (X_1 : WidePullbackShape ι) ↦
                  Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                    Functor.obj.{w, v, w, u}
                        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                      Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                    X_1
                    (terminal.from
                      (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                    fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                naturality := ⋯ } })
        (some j)
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j = s.π.app (some j)

Tactic:
rw [← h (some j)]

Premises used: Option.some
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
intro :
  ∀ (val : Fintype ι),
    HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
      (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
      Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))
⊢ HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
    (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
val : Fintype ι
⊢ HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
    (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))

Tactic:
⟨⟨wideCospan.limitCone ι X⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
val : Fintype ι
⊢ HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
    (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))

Tactic:
exact ⟨⟨wideCospan.limitCone ι X⟩⟩
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
⊢ HasWidePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X

Tactic:
hasWidePullback _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.CechNerveTerminalFrom.hasWidePullback, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
⊢ HasLimit.{w, w, v, u} (wideCospan ι X)

Tactic:
hasWidePullback _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.CechNerveTerminalFrom.hasWidePullback, CategoryTheory.CechNerveTerminalFrom.wideCospan, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
⊢ Eq.{v + 1} (α := (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X)
    (CategoryStruct.comp (Y := limit.{w, w, v, u} (wideCospan ι X))
        (Iso.inv (limitIsoPi ι X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ limit.{w, w, v, u} (wideCospan ι X))
        (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
          (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X) :
      (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X)
    (Pi.π (fun (x : ι) ↦ X) j : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.CechNerveTerminalFrom.wideCospan
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
rw :
  Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
        (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
        (CategoryStruct.comp (Y := limit.{w, w, v, u} (wideCospan ι X))
            (Iso.inv (limitIsoPi ι X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ limit.{w, w, v, u} (wideCospan ι X))
            (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
              (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X) :
          (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
      limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
      (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)
rw₁ rw₂ :
  Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X) (WidePullback.π (fun (x : ι) ↦ terminal.from X) j)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j)
⊢ Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
        (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
        (Pi.π (fun (x : ι) ↦ X) j : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
      limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
      (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)

Tactic:
rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).inverse = e'.inverse ⋙ eA.inverse

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
w : ∀ (Y : B'), (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Tactic:
ext Y