Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option.refine_1.none
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) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
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 (fun j ↦ W (some j)) f.2
⊢ W none ((Pi.optionEquivalence C).inverse.map f none)

pp: case h_option.refine_1.some
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) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
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 (fun j ↦ W (some j)) f.2
i : J
⊢ W (some i) ((Pi.optionEquivalence C).inverse.map f (some i))

Tactic:
· exact hf₁

Goal state after:
case h_option.refine_1.some
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) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
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 (fun j ↦ W (some j)) f.2
i : J
⊢ W (some i) ((Pi.optionEquivalence C).inverse.map f (some i))