awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x : K
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
      (obj
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
        X x)
      ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))
    ((map
            (comp (D := (j : J) → C (g j))
              { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
                map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ :
                ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
              { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
                map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ :
                ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
            f' ≫
          fun (b : K) ↦ 𝟙 (Y (g (f b))))
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
          X x)
        ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))
    (CategoryStruct.comp (Y := fun (i : K) ↦ X (g (f i))) (fun (b : K) ↦ 𝟙 (X (g (f b)))) (fun (i : K) ↦ f' (g (f i)))
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
          X x)
        ((fun (i : K) ↦ (Y (g (f i)) : C (g (f i)))) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
simp :
  Eq (α :=
    Quiver.Hom (V := (j : K) → C (g (f j))) (fun (i : K) ↦ X (g (f i)))
      (obj
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
        Y))
    (CategoryStruct.comp (Y := fun (i : K) ↦ Y (g (f i))) (fun (i : K) ↦ f' (g (f i))) fun (b : K) ↦ 𝟙 (Y (g (f b))))
    ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫
      map
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ :
            ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ :
            ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
        f')
⊢ Eq (α := obj (comap C (g ∘ f)) X ⟶ obj (comap C g ⋙ comap (C ∘ g) f) Y)
    (map (comap C (g ∘ f)) f' ≫ fun (b : K) ↦ 𝟙 (Y (g (f b))))
    ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫ map (comap C g ⋙ comap (C ∘ g) f) f')

Tactic:
simp only [comap, Function.comp]

Premises used: Function.comp, CategoryTheory.Pi.comap
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x : K
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) x)
      (obj
        (comp (D := (j : J) → C (g j))
          { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
            map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
          { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
            map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
        Y x))
    (CategoryStruct.comp (Y := fun (i : K) ↦ Y (g (f i))) (fun (i : K) ↦ f' (g (f i))) (fun (b : K) ↦ 𝟙 (Y (g (f b))))
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
          Y x))
    (((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫
          map
            (comp (D := (j : J) → C (g j))
              { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
                map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ :
                ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
              { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
                map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ :
                ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
            f')
        x :
      Quiver.Hom.{v₁, u₁} (V := (fun (j : K) ↦ (C ∘ g) (f j)) x) ((fun (i : K) ↦ (X (g (f i)) : C (g (f i)))) x)
        (obj
          (comp (D := (j : J) → C (g j))
            { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
              map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := ⋯, map_comp := ⋯ }
            { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
              map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := ⋯, map_comp := ⋯ })
          Y x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    Eq (α := obj (comap C h ⋙ eval (C ∘ h) j) X ⟶ obj (eval C (h j)) Y)
      (map (comap C h ⋙ eval (C ∘ h) j) f ≫
        Iso.hom
          ((fun (x : (i : I) → C i) ↦
              (Iso.refl (obj (comap C h ⋙ eval (C ∘ h) j) x) :
                obj (comap C h ⋙ eval (C ∘ h) j) x ≅ obj (comap C h ⋙ eval (C ∘ h) j) x))
            Y))
      (Iso.hom
          ((fun (x : (i : I) → C i) ↦
              (Iso.refl (obj (comap C h ⋙ eval (C ∘ h) j) x) :
                obj (comap C h ⋙ eval (C ∘ h) j) x ≅ obj (comap C h ⋙ eval (C ∘ h) j) x))
            X) ≫
        map (eval C (h j)) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.hom ≫ f.inv) i = 𝟙 (X i)
rw₁ : Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 X i : X i ⟶ X i) (𝟙 (X i) : X i ⟶ X i)
rw₂ rw₃ : Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 (X i)) (𝟙 (X i))
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Pi.comp_apply, CategoryTheory.Pi.id_apply
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.inv ≫ f.hom) i = 𝟙 (Y i)
rw₁ : Eq.{v₁ + 1} (α := Y i ⟶ Y i) (𝟙 Y i : Y i ⟶ Y i) (𝟙 (Y i) : Y i ⟶ Y i)
rw₂ rw₃ : Eq.{v₁ + 1} (α := Y i ⟶ Y i) (𝟙 (Y i)) (𝟙 (Y i))
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)

Tactic:
rw [← comp_apply, Iso.inv_hom_id, id_apply]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pi.comp_apply, CategoryTheory.Pi.id_apply
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := X i ≅ X i) (isoApp (C := C) (Iso.refl X) i) (Iso.refl (X i))

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ isoApp (C := C) f.symm i = (isoApp (C := C) f i).symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
f : X ≅ Y
g : Y ≅ Z
i : I
⊢ isoApp (C := C) (f ≪≫ g) i = isoApp (C := C) f i ≪≫ isoApp (C := C) g i

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
subst : Eq.{v₁ + 1} (α := x i ⟶ x i) (eqToHom ⋯ i : x i ⟶ x i) (eqToHom ⋯ : x i ⟶ x i)
⊢ Eq.{v₁ + 1} (α := x i ⟶ x' i) (eqToHom h i : x i ⟶ x' i) (eqToHom ⋯ : x i ⟶ x' i)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
x : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := x i ⟶ x i) (eqToHom ⋯ i : x i ⟶ x i) (eqToHom ⋯ : x i ⟶ x i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f : (i : I) → Functor.{v₃, v₁, u₃, u₁} A (C i)
i : I
⊢ pi' (C := C) f ⋙ Pi.eval C i = f i

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
h_map : autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1
h_obj : ∀ (X : A), f.obj X = f'.obj X
⊢ f = f'

Tactic:
apply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
h_obj : ∀ (i : I), f.obj X i = f'.obj X i
⊢ f.obj X = f'.obj X

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
i : I
⊢ f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i

Tactic:
specialize h i
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X

Tactic:
have := congr_obj h X
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X
⊢ f.obj X i = f'.obj X i

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
h_map : ∀ (i : I), f.map g i = (eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯) i
⊢ f.map g = eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
⊢ f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i

Tactic:
specialize h i
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h_1 : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ (f ⋙ Pi.eval C i).map g = eqToHom ⋯ ≫ (f' ⋙ Pi.eval C i).map g ≫ eqToHom ⋯

Tactic:
have := congr_hom h g
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h_1 : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this : (f ⋙ Pi.eval C i).map g = eqToHom ⋯ ≫ (f' ⋙ Pi.eval C i).map g ≫ eqToHom ⋯
⊢ f.map g i = (eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯) i

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst_1 : (i : I) → Category.{v₂, u₂} (D i)
F_1 G_1 : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) (D i)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x x_1 : E
f : x ⟶ x_1
w : ∀ (i : I), Eq.{v₁ + 1} ((F.map f ≫ fun (i : I) ↦ (τ i).app x_1) i) (((fun (i : I) ↦ (τ i).app x) ≫ G.map f) i)
⊢ (F.map f ≫ fun (i : I) ↦ (τ i).app x_1) = (fun (i : I) ↦ (τ i).app x) ≫ G.map f

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst_1 : (i : I) → Category.{v₂, u₂} (D i)
F_1 G_1 : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) (D i)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x x_1 : E
f : x ⟶ x_1
i : I
⊢ Eq.{v₁ + 1} ((F.map f ≫ fun (i : I) ↦ (τ i).app x_1) i) (((fun (i : I) ↦ (τ i).app x) ≫ G.map f) i)

Tactic:
(τ i).naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst_1 : (i : I) → Category.{v₂, u₂} (D i)
F_1 G_1 : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) (D i)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x x_1 : E
f : x ⟶ x_1
i : I
⊢ Eq.{v₁ + 1} ((F.map f ≫ fun (i : I) ↦ (τ i).app x_1) i) (((fun (i : I) ↦ (τ i).app x) ≫ G.map f) i)

Tactic:
exact (τ i).naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
mp : IsIso f → ∀ (i : I), IsIso (f i)
mpr : (∀ (i : I), IsIso (f i)) → IsIso f
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
h : IsIso f
i : I
⊢ IsIso (f i)

Tactic:
(Pi.isoApp (asIso f) i).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Pi.isoApp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
h : IsIso f
i : I
⊢ IsIso (f i)

Tactic:
exact (Pi.isoApp (asIso f) i).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Pi.isoApp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
h : ∀ (i : I), IsIso (f i)
⊢ IsIso f

Tactic:
exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
subst : Equivalence.{v₁, v₁, u₁, u₁} (C i) (C i)
⊢ Equivalence.{v₁, v₁, u₁, u₁} (C i) (C j)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ Equivalence.{v₁, v₁, u₁, u₁} (C i) (C i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
subst : Eq (α := ((i : I) → C i) ⥤ C i) (eval C i ⋙ Equivalence.functor (eqToEquivalence C ⋯)) (eval C i)
⊢ Eq (α := ((i : I) → C i) ⥤ C j) (eval C i ⋙ Equivalence.functor (eqToEquivalence C h)) (eval C j)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ Eq (α := ((i : I) → C i) ⥤ C i) (eval C i ⋙ Equivalence.functor (eqToEquivalence C ⋯)) (eval C i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' j' : J
h : i' = j'
subst :
  Eq (α := Functor.{v₁, v₁, u₁, u₁} (C (f i')) (C (f i'))) (Equivalence.functor (eqToEquivalence C ⋯))
    (Equivalence.functor (eqToEquivalence (fun (i' : J) ↦ C (f i')) ⋯))
⊢ Eq (α := Functor.{v₁, v₁, u₁, u₁} (C (f i')) (C (f j'))) (Equivalence.functor (eqToEquivalence C ⋯))
    (Equivalence.functor (eqToEquivalence (fun (i' : J) ↦ C (f i')) h))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' : J
⊢ Eq (α := Functor.{v₁, v₁, u₁, u₁} (C (f i')) (C (f i'))) (Equivalence.functor (eqToEquivalence C ⋯))
    (Equivalence.functor (eqToEquivalence (fun (i' : J) ↦ C (f i')) ⋯))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
e : J ≃ I
i : I
⊢ (e : (a : J) → I) ((e.symm : (a : I) → J) i : J) = i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
C' : Option J → Type u₁
inst_1 : (i : Option J) → Category.{v₁, u₁} (C' i)
⊢ Iso (C := C' none × ((j : J) → C' (some j)) ⥤ C' none × ((j : J) → C' (some j)))
    ((pi' (C := C') fun (i : Option J) ↦
        match (motive := (i : Option J) → C' none × ((j : J) → C' (some j)) ⥤ C' i) i with
        | none => Prod.fst (C' none) ((j : J) → C' (some j))
        | some i => Prod.snd (C' none) ((j : J) → C' (some j)) ⋙ eval (fun (j : J) ↦ C' (some j)) i) ⋙
      Functor.prod' (eval C' none) (pi' (C := fun (j : J) ↦ C' (some j)) fun (i : J) ↦ eval C' (some i)))
    (𝟭 (C' none × ((j : J) → C' (some j))))

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst_1 : (i : I) → Category.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) (D i)
inst_2 : ∀ (i : I), (F i).IsEquivalence
⊢ (Functor.pi (C := C) (D := D) F).IsEquivalence

Tactic:
(pi (fun i => (F i).asEquivalence)).isEquivalence_functor

Premises used: CategoryTheory.Equivalence.pi, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Functor.pi
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i)
    (Iso.hom (α_ X Y Z) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i)
    (Iso.hom (α_ (X i) (Y i) (Z i)) :
      tensorObj.{v₁, u₁} (𝒞 := inst i) (tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (Y i)) (Z i) ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (tensorObj.{v₁, u₁} (𝒞 := inst i) (Y i) (Z i)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i)
    (Iso.inv (α_ X Y Z) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i)
    (Iso.inv (α_ (X i) (Y i) (Z i)) :
      tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (tensorObj.{v₁, u₁} (𝒞 := inst i) (Y i) (Z i)) ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst i) (tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (Y i)) (Z i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ≅
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i)
    (isoApp (C := C) (α_ X Y Z) i) (α_ (X i) (Y i) (Z i))

Tactic:
rfl

Premises used: CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) X i ⟶ X i)
    (Iso.hom (λ_ X) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) X i ⟶ X i)
    (Iso.hom (λ_ (X i)) : tensorObj.{v₁, u₁} (𝒞 := inst i) (tensorUnit.{v₁, u₁} (C i) (𝒞 := inst i)) (X i) ⟶ X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) X i)
    (Iso.inv (λ_ X) i : X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) X i)
    (Iso.inv (λ_ (X i)) : X i ⟶ tensorObj.{v₁, u₁} (𝒞 := inst i) (tensorUnit.{v₁, u₁} (C i) (𝒞 := inst i)) (X i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) X i ≅ X i)
    (isoApp (C := C) (λ_ X) i) (λ_ (X i))

Tactic:
rfl

Premises used: CategoryTheory.Pi.isoApp, rfl