awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_4 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J₁) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J₁), (W j).ContainsIdentities]
    [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst_1 : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → Functor.{v₁, v₂, u₁, u₂} (C₂ j) (D₂ j)
W₂ : (j : J₂) → MorphismProperty.{v₁, u₁} (C₂ j)
inst_2 : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst_3 : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C₂ ((e : (a : J₁) → J₂) j)) (D₂ ((e : (a : J₁) → J₂) j)) :=
  fun (j : J₁) ↦ L₂ ((e : (a : J₁) → J₂) j)
E : ((j : J₁) → C₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this :
  CatCommSq E.functor
    (Functor.pi (C := fun (j : J₁) ↦ C₂ ((e : (a : J₁) → J₂) j)) (D := fun (i : J₁) ↦ D₂ ((e : (a : J₁) → J₂) i)) L₁)
    (Functor.pi (C := C₂) (D := D₂) L₂) E'.functor
X Y : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)
f : X ⟶ Y
hf : MorphismProperty.pi (C := fun (i : J₁) ↦ C₂ ((e : (a : J₁) → J₂) i)) (fun (j : J₁) ↦ W₂ ((e : (a : J₁) → J₂) j)) f
i : J₂
of_equiv :
  ∀
    (H :
      ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y),
        W₂ j g →
          W₂ j' (X := obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (Pi.eqToEquivalence C₂ h)) X)
            (map (Equivalence.functor (Pi.eqToEquivalence C₂ h)) g)),
    W₂ i (E.functor.map f i)
⊢ W₂ i (E.functor.map f i)

Tactic:
have H : ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y) (_ : W₂ j g),
        W₂ j' ((Pi.eqToEquivalence C₂ h).functor.map g) := by
      rintro j _ rfl _ _ g hg
      exact hg
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_4 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J₁) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J₁), (W j).ContainsIdentities]
    [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst_1 : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → Functor.{v₁, v₂, u₁, u₂} (C₂ j) (D₂ j)
W₂ : (j : J₂) → MorphismProperty.{v₁, u₁} (C₂ j)
inst_2 : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst_3 : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C₂ ((e : (a : J₁) → J₂) j)) (D₂ ((e : (a : J₁) → J₂) j)) :=
  fun (j : J₁) ↦ L₂ ((e : (a : J₁) → J₂) j)
E : ((j : J₁) → C₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this :
  CatCommSq E.functor
    (Functor.pi (C := fun (j : J₁) ↦ C₂ ((e : (a : J₁) → J₂) j)) (D := fun (i : J₁) ↦ D₂ ((e : (a : J₁) → J₂) i)) L₁)
    (Functor.pi (C := C₂) (D := D₂) L₂) E'.functor
X Y : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)
f : X ⟶ Y
hf : MorphismProperty.pi (C := fun (i : J₁) ↦ C₂ ((e : (a : J₁) → J₂) i)) (fun (j : J₁) ↦ W₂ ((e : (a : J₁) → J₂) j)) f
i : J₂
H :
  ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y),
    W₂ j g →
      W₂ j' (X := obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (Pi.eqToEquivalence C₂ h)) X)
        (map (Equivalence.functor (Pi.eqToEquivalence C₂ h)) g)
⊢ W₂ i (E.functor.map f i)

Tactic:
H (e.apply_symm_apply i) _ (hf (e.symm i))

Premises used: Equiv.apply_symm_apply, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_4 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J₁) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J₁), (W j).ContainsIdentities]
    [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst_1 : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → Functor.{v₁, v₂, u₁, u₂} (C₂ j) (D₂ j)
W₂ : (j : J₂) → MorphismProperty.{v₁, u₁} (C₂ j)
inst_2 : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst_3 : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C₂ ((e : (a : J₁) → J₂) j)) (D₂ ((e : (a : J₁) → J₂) j)) :=
  fun (j : J₁) ↦ L₂ ((e : (a : J₁) → J₂) j)
E : ((j : J₁) → C₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this :
  CatCommSq E.functor
    (Functor.pi (C := fun (j : J₁) ↦ C₂ ((e : (a : J₁) → J₂) j)) (D := fun (i : J₁) ↦ D₂ ((e : (a : J₁) → J₂) i)) L₁)
    (Functor.pi (C := C₂) (D := D₂) L₂) E'.functor
X Y : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)
f : X ⟶ Y
hf : MorphismProperty.pi (C := fun (i : J₁) ↦ C₂ ((e : (a : J₁) → J₂) i)) (fun (j : J₁) ↦ W₂ ((e : (a : J₁) → J₂) j)) f
i : J₂
H :
  ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y),
    W₂ j g →
      W₂ j' (X := obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (Pi.eqToEquivalence C₂ h)) X)
        (map (Equivalence.functor (Pi.eqToEquivalence C₂ h)) g)
⊢ W₂ i (E.functor.map f i)

Tactic:
exact H (e.apply_symm_apply i) _ (hf (e.symm i))

Premises used: Equiv.apply_symm_apply, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
h_empty :
  ∀ [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
h_empty :
  ∀ [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
h_empty :
  ∀ [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
inst_2 : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
h_empty :
  ∀ [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
inst_2 : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst_3 : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
⊢ ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence

Tactic:
haveI : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
inst_2 : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst_3 : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)

Premises used: CategoryTheory.Functor.IsLocalization.of_isEquivalence
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
inst_2 : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst_3 : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
h_empty :
  ∀ (x x_1 : (i : PEmpty.{w + 1}) → C i) (x_2 : x ⟶ x_1),
    MorphismProperty.pi (C := C) W x_2 → MorphismProperty.isomorphisms ((i : PEmpty.{w + 1}) → C i) x_2
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)

Premises used: CategoryTheory.Functor.IsLocalization.of_isEquivalence
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)
inst_2 : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst_3 : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x x_1 : (i : PEmpty.{w + 1}) → C i
x_2 : x ⟶ x_1
h : MorphismProperty.pi (C := C) W x_2
h_empty : ∀ (i : PEmpty.{w + 1}), IsIso (x_2 i)
⊢ MorphismProperty.isomorphisms ((i : PEmpty.{w + 1}) → C i) x_2

Tactic:
rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.isIso_pi_iff
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
h_option :
  ∀ [Fintype J],
    (∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
        [∀ (j : J), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : Option J → Type u₁} {D : Option J → Type u₂} [inst : (j : Option J) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
        [∀ (j : Option J), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [Fintype J],
    (∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
        [∀ (j : J), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : Option J → Type u₁} {D : Option J → Type u₂} [inst : (j : Option J) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
        [∀ (j : Option J), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
h_option :
  ∀ [inst : (j : Option J) → Category.{v₁, u₁} (C j)] [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)]
    (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)) (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j))
    [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [inst : (j : Option J) → Category.{v₁, u₁} (C j)] [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)]
    (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)) (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j))
    [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_2 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
h_option :
  ∀ [inst : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [inst : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_3 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
inst_2 : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)
h_option :
  ∀ [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_4 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
inst_2 : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)
inst_3 : ∀ (j : Option J), (W j).ContainsIdentities
h_option :
  ∀ [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_5 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
inst_2 : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)
inst_3 : ∀ (j : Option J), (W j).ContainsIdentities
inst_4 : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) :=
  Functor.prod (L none)
    (Functor.pi (C := fun (j : J) ↦ C (some j)) (D := fun (j : J) ↦ D (some j)) fun (j : J) ↦ L (some j))
⊢ Iso (C := C none × ((j : J) → C (some j)) ⥤ D none)
    ((Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C)) ⋙ Functor.pi (C := C) (D := D) L) ⋙
      Pi.eval D none)
    ((L₁ ⋙ Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D))) ⋙ Pi.eval D none)

Tactic:
apply Iso.refl

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_5 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
inst_2 : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)
inst_3 : ∀ (j : Option J), (W j).ContainsIdentities
inst_4 : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) :=
  Functor.prod (L none)
    (Functor.pi (C := fun (j : J) ↦ C (some j)) (D := fun (j : J) ↦ D (some j)) fun (j : J) ↦ L (some j))
i : J
⊢ Iso (C := C none × ((j : J) → C (some j)) ⥤ D (some i))
    ((Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C)) ⋙ Functor.pi (C := C) (D := D) L) ⋙
      Pi.eval D (some i))
    ((L₁ ⋙ Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D))) ⋙ Pi.eval D (some i))

Tactic:
apply Iso.refl

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_5 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C : Option J → Type u₁
D : Option J → Type u₂
inst_1 : (j : Option J) → Category.{v₁, u₁} (C j)
inst_2 : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j)
W : (j : Option J) → MorphismProperty.{v₁, u₁} (C j)
inst_3 : ∀ (j : Option J), (W j).ContainsIdentities
inst_4 : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) :=
  Functor.prod (L none)
    (Functor.pi (C := fun (j : J) ↦ C (some j)) (D := fun (j : J) ↦ D (some j)) fun (j : J) ↦ L (some j))
h_option :
  ∀
    (this :
      CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
        (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))),
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
haveI : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L)
      (Pi.optionEquivalence D).symm.functor :=
        ⟨NatIso.pi' (by rintro (_ | i) <;> apply Iso.refl)⟩