awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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
⊢ (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)
have of_equiv : (MorphismProperty.pi (C := fun (i : J₁) ↦ C₂ ((e : (a : J₁) → J₂) i)) fun (j : J₁) ↦ W₂ ((e : (a : J₁) → J₂) j)) ≤
  (MorphismProperty.pi (C := C₂) W₂).isoClosure.inverseImage E.functor
Tactic: refine IsLocalization.of_equivalences (Functor.pi L₁)
      (MorphismProperty.pi (fun j => (W₂ (e j)))) (Functor.pi L₂)
      (MorphismProperty.pi W₂) E E' ?_
      (MorphismProperty.IsInvertedBy.pi _ _ (fun _ => Localization.inverts _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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
⊢ (MorphismProperty.pi (C := C₂) W₂).isoClosure.inverseImage E.functor f
have of_equiv : ∀ (i : J₂), W₂ i (E.functor.map f i)
Tactic: refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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₂
⊢ W₂ i (E.functor.map f i)
have 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)
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (hypothesis)
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)
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
Tactic: haveI : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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)
have 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
Tactic: refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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
⊢ MorphismProperty.isomorphisms ((i : PEmpty.{w + 1}) → C i) x_2
have h_empty : ∀ (i : PEmpty.{w + 1}), IsIso (x_2 i)
Tactic: rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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))
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have 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)
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)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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)
have 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)))
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 ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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)))
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have h_option₁ : (MorphismProperty.pi (C := C) W).IsInvertedBy (Functor.pi (C := C) (D := D) L)
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 ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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 × ((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
have 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
Tactic: ⟨Y₁, Y₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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₂)
⊢ 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
have 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
Tactic: ⟨hf₁, hf₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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
have h_option : MorphismProperty.pi (C := C) W (X := obj (Equivalence.inverse (Pi.optionEquivalence C)) (X₁, X₂))
  (map (Equivalence.inverse (Pi.optionEquivalence C)) f)
Tactic: refine ⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨Iso.refl _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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.pi (C := C) W).IsInvertedBy (Functor.pi (C := C) (D := D) L)
have h_option : ∀ (j : Option J), (W j).IsInvertedBy (L j)
Tactic: apply MorphismProperty.IsInvertedBy.pi
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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
⊢ IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
    (W.functorCategory (Discrete J))
have 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))
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 _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
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))
have refine_1 : (MorphismProperty.pi (C := fun (i : J) ↦ C) fun (x : J) ↦ W) ≤
  MorphismProperty.inverseImage (MorphismProperty.isoClosure (W.functorCategory (Discrete J))) E.functor
Tactic: refine Functor.IsLocalization.of_equivalences L₁
    (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_