-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Localization.essSurj_mapArrow :
    L.mapArrow.EssSurj where
  mem_essImage f

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ f ≅ L.mapArrow.obj (Arrow.mk φ.f)

Tactic:
refine Arrow.isoMk eX.symm (eY.symm ≪≫ Localization.isoOfHom L W φ.s φ.hs) ?_

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk φ.f)).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W φ.s ⋯).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨X, ⟨eX⟩⟩ : ∃ (X : C), Nonempty (L.obj X ≅ f.left) :=
  ⟨_, ⟨L.objObjPreimageIso f.left⟩⟩

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
⊢ L.mapArrow.essImage f

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨Y, ⟨eY⟩⟩ : ∃ (Y : C), Nonempty (L.obj Y ≅ f.right) :=
  ⟨_, ⟨L.objObjPreimageIso f.right⟩⟩

Result:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
⊢ L.mapArrow.essImage f

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
⊢ L.mapArrow.essImage f

Tactic:
have := Localization.essSurj L W

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
⊢ L.mapArrow.essImage f

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk φ.f)).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W φ.s ⋯).hom

Tactic:
dsimp

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ eX.inv ≫ L.map φ.f = f.hom ≫ eY.inv ≫ L.map φ.s

Proof state:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L W (eX.hom ≫ f.hom ≫ eY.inv)

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ L.mapArrow.essImage f

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ eX.inv ≫ L.map φ.f = f.hom ≫ eY.inv ≫ L.map φ.s

Tactic:
simp only [← cancel_epi eX.hom, Iso.hom_inv_id_assoc, reassoc_of% hφ,
  MorphismProperty.LeftFraction.map_comp_map_s]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ L.mapArrow.essImage f

Tactic:
refine ⟨Arrow.mk φ.f, ⟨Iso.symm ?_⟩⟩

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
f : Arrow D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯
⊢ f ≅ L.mapArrow.obj (Arrow.mk φ.f)