awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)

Tactic:
IsLocalization.of_equivalences L₁
      ((W none).prod (MorphismProperty.pi (fun j => W (some j)))) (Functor.pi L) _
      (Pi.optionEquivalence C).symm (Pi.optionEquivalence D).symm ?_ ?_

Premises used: Option.some, CategoryTheory.MorphismProperty.prod, Option.none, CategoryTheory.Pi.optionEquivalence, CategoryTheory.MorphismProperty.pi, CategoryTheory.Functor.pi, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.IsLocalization.of_equivalences
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
h_option :
  MorphismProperty.prod (W none) (MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) fun (j : J) ↦ W (some j)) ≤
    (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
      (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C)))
h_option₁ : (MorphismProperty.pi (C := C) W).IsInvertedBy (Functor.pi (C := C) (D := D) L)
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
refine IsLocalization.of_equivalences L₁
      ((W none).prod (MorphismProperty.pi (fun j => W (some j)))) (Functor.pi L) _
      (Pi.optionEquivalence C).symm (Pi.optionEquivalence D).symm ?_ ?_

Premises used: Option.some, CategoryTheory.MorphismProperty.prod, Option.none, CategoryTheory.Pi.optionEquivalence, CategoryTheory.MorphismProperty.pi, CategoryTheory.Functor.pi, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.IsLocalization.of_equivalences
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
h_option :
  ∀ (Y₁ : C none) (Y₂ : (i : J) → C (some i)) (f : (X₁, X₂) ⟶ (Y₁, Y₂)),
    MorphismProperty.prod (W none) (MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) fun (j : J) ↦ W (some j)) f →
      (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
        (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f
⊢ ∀ ⦃Y : C none × ((i : J) → C (some i))⦄ (f : (X₁, X₂) ⟶ Y),
    MorphismProperty.prod (W none) (MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) fun (j : J) ↦ W (some j)) f →
      (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
        (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f

Tactic:
⟨Y₁, Y₂⟩
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
h_option :
  ∀ (hf₁ : W none f.1) (hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2),
    (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
      (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f
⊢ MorphismProperty.prod (W none) (MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) fun (j : J) ↦ W (some j)) f →
    (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
      (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f

Tactic:
⟨hf₁, hf₂⟩
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2
⊢ (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f

Tactic:
⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.Pi.optionEquivalence, Exists.intro, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.Equivalence.inverse
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2
h_option :
  MorphismProperty.pi (C := C) W (X := obj (Equivalence.inverse (Pi.optionEquivalence C)) (X₁, X₂))
    (map (Equivalence.inverse (Pi.optionEquivalence C)) f)
⊢ (MorphismProperty.pi (C := C) W).isoClosure.inverseImage
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) f

Tactic:
refine ⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2
⊢ W none (X := obj (Equivalence.inverse (Pi.optionEquivalence C)) (X₁, X₂) none) (Y :=
    obj (Equivalence.inverse (Pi.optionEquivalence C)) (Y₁, Y₂) none)
    (map (Equivalence.inverse (Pi.optionEquivalence C)) f none)

Tactic:
hf₁
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2
⊢ W none (X := obj (Equivalence.inverse (Pi.optionEquivalence C)) (X₁, X₂) none) (Y :=
    obj (Equivalence.inverse (Pi.optionEquivalence C)) (Y₁, Y₂) none)
    (map (Equivalence.inverse (Pi.optionEquivalence C)) f none)

Tactic:
exact hf₁
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (C := fun (i : J) ↦ C (some i)) (fun (j : J) ↦ W (some j)) f.2
i : J
⊢ W (some i) (X := obj (Equivalence.inverse (Pi.optionEquivalence C)) (X₁, X₂) (some i)) (Y :=
    obj (Equivalence.inverse (Pi.optionEquivalence C)) (Y₁, Y₂) (some i))
    (map (Equivalence.inverse (Pi.optionEquivalence C)) f (some i))

Tactic:
apply hf₂
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
h_option : ∀ (j : Option J), (W j).IsInvertedBy (L j)
⊢ (MorphismProperty.pi (C := C) W).IsInvertedBy (Functor.pi (C := C) (D := D) L)

Tactic:
apply MorphismProperty.IsInvertedBy.pi

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.pi
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
⊢ MorphismProperty.IsInvertedBy (C := C none) (W none) (L none)

Tactic:
apply Localization.inverts

Premises used: CategoryTheory.Localization.inverts
-- 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))
this :
  CatCommSq (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence C))) L₁ (Functor.pi (C := C) (D := D) L)
    (Equivalence.functor (Equivalence.symm (Pi.optionEquivalence D)))
i : J
⊢ MorphismProperty.IsInvertedBy (C := C (some i)) (W (some i)) (L (some i))

Tactic:
apply Localization.inverts

Premises used: CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
⊢ L₂ ⋙ E'.inverse ≅ E.inverse ⋙ L₁

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
have :
  ∀ (this : CatCommSq E.functor L₁ L₂ E'.functor),
    IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
      (W.functorCategory (Discrete J))
⊢ IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
    (W.functorCategory (Discrete J))

Tactic:
have : CatCommSq E.functor L₁ L₂ E'.functor :=
    ⟨(Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft _ E'.counitIso.symm ≪≫
      Functor.associator _ _ _≪≫ isoWhiskerLeft _ ((Functor.associator _ _ _).symm ≪≫
      isoWhiskerRight (by exact Iso.refl _) _) ≪≫ (Functor.associator _ _ _).symm ≪≫
      isoWhiskerRight ((Functor.associator _ _ _).symm ≪≫
      isoWhiskerRight E.unitIso.symm L₁) _ ≪≫ isoWhiskerRight L₁.leftUnitor _⟩
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
⊢ IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
    (W.functorCategory (Discrete J))

Tactic:
Functor.IsLocalization.of_equivalences L₁
    (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_

Premises used: CategoryTheory.MorphismProperty.pi, CategoryTheory.Functor.IsLocalization.of_equivalences