awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
J : Type w
inst : Finite J
C : J → Type u₁
D : J → Type u₂
inst_1 : (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)
inst_3 : ∀ (j : J), (W j).ContainsIdentities
inst_4 : ∀ (j : J), (L j).IsLocalization (W j)
revert :
  ∀ {J : Type w} [Finite J] {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)
⊢ (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)

Tactic:
revert J
-- Module: Mathlib.CategoryTheory.Localization.Pi
Goal:
of_equiv :
  ∀ {α β : Type w} (a : α ≃ β),
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
        [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : β → Type u₁} {D : β → Type u₂} [inst : (j : β) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : β) → Category.{v₂, u₂} (D j)] (L : (j : β) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : β) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : β), (W j).ContainsIdentities]
        [∀ (j : β), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
h_empty :
  ∀ {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)) [∀ (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)
h_option :
  ∀ {α : Type w} [Fintype α],
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
        [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : Option α → Type u₁} {D : Option α → Type u₂} [inst : (j : Option α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : Option α) → Category.{v₂, u₂} (D j)] (L : (j : Option α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : Option α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option α), (W j).ContainsIdentities]
        [∀ (j : Option α), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ {J : Type w} [Finite 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)

Tactic:
apply Finite.induction_empty_option

Premises used: Finite.induction_empty_option
-- 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_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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
of_equiv :
  ∀ [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)
⊢ ∀ [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)

Tactic:
_
-- 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_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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst : (j : J₂) → Category.{v₁, u₁} (C₂ j)
of_equiv :
  ∀ [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)
⊢ ∀ [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)

Tactic:
_
-- 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_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₂ : 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)
of_equiv :
  ∀ [∀ (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₂)
⊢ ∀ [∀ (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₂)

Tactic:
_
-- 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_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₂ : 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
of_equiv :
  ∀ [∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)],
    (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)
⊢ ∀ [∀ (j : 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₁ 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
of_equiv :
  ∀
    (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₂)
⊢ (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)

Tactic:
haveI : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
      (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩
-- 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
⊢ (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)

Tactic:
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 _ _))

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.pi, CategoryTheory.MorphismProperty.pi, CategoryTheory.Localization.inverts, CategoryTheory.Functor.pi, DFunLike.coe, CategoryTheory.Functor.IsLocalization.of_equivalences
-- 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
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
⊢ (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)

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 _ _))

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.pi, CategoryTheory.MorphismProperty.pi, CategoryTheory.Localization.inverts, CategoryTheory.Functor.pi, DFunLike.coe, CategoryTheory.Functor.IsLocalization.of_equivalences
-- 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 : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)
of_equiv :
  ∀ ⦃Y : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)⦄ (f : X ⟶ Y),
    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
⊢ ∀ ⦃Y : (i : J₁) → C₂ ((e : (a : J₁) → J₂) i)⦄ (f : X ⟶ Y),
    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

Tactic:
_
-- 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
⊢ (MorphismProperty.pi (C := C₂) W₂).isoClosure.inverseImage E.functor f

Tactic:
⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, Nonempty.intro, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.MorphismProperty.isoClosure
-- 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
of_equiv : ∀ (i : J₂), W₂ i (E.functor.map f i)
⊢ (MorphismProperty.pi (C := C₂) W₂).isoClosure.inverseImage E.functor f

Tactic:
refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩
-- 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 : J₂
X_1 Y_1 : C₂ j
g : X_1 ⟶ Y_1
hg : W₂ j g
⊢ W₂ j (X := obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (Pi.eqToEquivalence C₂ ⋯)) X_1)
    (map (Equivalence.functor (Pi.eqToEquivalence C₂ ⋯)) g)

Tactic:
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 : J₂
X_1 Y_1 : C₂ j
g : X_1 ⟶ Y_1
hg : W₂ j g
⊢ W₂ j (X := obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (Pi.eqToEquivalence C₂ ⋯)) X_1)
    (map (Equivalence.functor (Pi.eqToEquivalence C₂ ⋯)) g)

Tactic:
exact hg