-- Mathlib/CategoryTheory/Localization/Equivalence.lean
/-- If `L₁ : C₁ ⥤ D` is a localization functor for `W₁ : MorphismProperty C₁`, then it is also
the case of a functor `L₂ : C₂ ⥤ D` for a suitable `W₂ : MorphismProperty C₂` when
we have an equivalence of category `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`. -/
lemma of_equivalence_source (L₁ : C₁ ⥤ D) (W₁ : MorphismProperty C₁)
    (L₂ : C₂ ⥤ D) (W₂ : MorphismProperty C₂)
    (E : C₁ ≌ C₂) (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂)
    [L₁.IsLocalization W₁] (iso : E.functor ⋙ L₂ ≅ L₁) : L₂.IsLocalization W₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
⊢ L₂.IsLocalization W₂

Tactic:
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf => by
  obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
  exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')

Result:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂.IsLocalization W₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ W₂.Q

Tactic:
calc
  L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
  _ ≅ _ := isoWhiskerRight E.counitIso.symm _
  _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
        Functor.associator _ _ _
  _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
        isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
          isoWhiskerRight iso _)
  _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
        isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
  _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
  _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
  _ ≅ W₂.Q := leftUnitor _

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Tactic:
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf

Result:
case intro.intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
w✝¹ w✝ : C₂
f' : w✝¹ ⟶ w✝
hf' : W₂ f'
e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂.IsLocalization W₂

Tactic:
exact
  { inverts := hW₂
    isEquivalence :=
      Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂)
        (E.functor ⋙ W₂.Q) (Localization.lift (E.functor ⋙ W₂.Q) h L₁) (by
          calc
            L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
            _ ≅ _ := isoWhiskerRight E.counitIso.symm _
            _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                  Functor.associator _ _ _
            _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                  isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
                    isoWhiskerRight iso _)
            _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
                  isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
            _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
            _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
            _ ≅ W₂.Q := leftUnitor _)
        (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _)  ≪≫ iso) }

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
w✝¹ w✝ : C₂
f' : w✝¹ ⟶ w✝
hf' : W₂ f'
e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Tactic:
exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
  (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')

Result:
no goals