mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
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₁) → 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₂ : 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)

Tactic:
_

Goal state after:
case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
⊢ ∀ [inst : (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)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
⊢ ∀ [inst : (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)

Tactic:
_

Goal state after:
case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝¹ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝ : (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)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝¹ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝ : (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₂)

Tactic:
_

Goal state after:
case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝² : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝¹ : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝ : ∀ (j : J₂), (W₂ j).ContainsIdentities
⊢ ∀ [∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)], (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝² : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝¹ : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝ : ∀ (j : J₂), (W₂ j).ContainsIdentities
⊢ ∀ [∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)], (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)

Tactic:
_

Goal state after:
case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
⊢ (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ : (i : J₁) → C₂ (e i)
⊢ ∀ ⦃Y : (i : J₁) → C₂ (e i)⦄ (f : X✝ ⟶ Y),
    MorphismProperty.pi (fun j ↦ W₂ (e j)) f → (MorphismProperty.pi W₂).isoClosure.inverseImage E.functor f

Tactic:
_

Goal state after:
case of_equiv
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₁) → 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ Y✝ : (i : J₁) → C₂ (e i)
⊢ ∀ (f : X✝ ⟶ Y✝),
    MorphismProperty.pi (fun j ↦ W₂ (e j)) f → (MorphismProperty.pi W₂).isoClosure.inverseImage E.functor f
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case 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}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case 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 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)] (L : (j : PEmpty.{w + 1}) → C j ⥤ D j)
    (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case 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 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)] (L : (j : PEmpty.{w + 1}) → C j ⥤ D j)
    (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case 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✝ : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
⊢ ∀ (L : (j : PEmpty.{w + 1}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case 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✝ : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
⊢ ∀ [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case 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✝¹ : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
⊢ ∀ [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case 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✝¹ : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
⊢ ∀ [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case 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✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
J : Type 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) → 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_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
        (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
        [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case h_option
J : Type w
inst✝ : 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) → 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_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
      (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
      [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
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_1 : (j : Option J) → Category.{v₂, u₂} (D j)]
    (L : (j : Option J) → C j ⥤ D j) (W : (j : Option J) → MorphismProperty (C j))
    [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case h_option
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)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
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)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case h_option
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))
    [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
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)
⊢ ∀ [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case h_option
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
⊢ ∀ [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
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
⊢ ∀ [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
_

Goal state after:
case h_option
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)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.tensor
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
⊢ motive ⟦f.tensor g⟧

Tactic:
| @tensor W X Y Z f g hf hg =>

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((Hom.whiskerLeft unit f✝).comp (l_hom Y✝)) = projectMapAux f✝¹ ((l_hom X✝).comp f✝)

Tactic:
| l_naturality =>

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F

Tactic:
refine natTrans_ext L W (fun X₁ ↦ ?_)

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
⊢ (LaxMonoidal.ofBifunctor.leftMapᵣ F).app (L.obj X₁) =
    (LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
          ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫
            LaxMonoidal.ofBifunctor.bottomMapᵣ F).app
      (L.obj X₁)