-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean
lemma essSurj_mapComposableArrows_of_hasRightCalculusOfFractions
    [W.HasRightCalculusOfFractions] (n : ℕ) :
    (L.mapComposableArrows n).EssSurj where
  mem_essImage Y

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.HasRightCalculusOfFractions
n : ℕ
Y : ComposableArrows D n
⊢ (L.mapComposableArrows n).essImage Y

Tactic:
have := 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.HasRightCalculusOfFractions
n : ℕ
Y : ComposableArrows D n
this : L.EssSurj
⊢ (L.mapComposableArrows n).essImage Y

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.HasRightCalculusOfFractions
n : ℕ
Y : ComposableArrows D n
this : L.EssSurj
⊢ (L.mapComposableArrows n).essImage Y

Tactic:
induction n with
| zero =>
  obtain ⟨Y, rfl⟩ := mk₀_surjective Y
  exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩
| succ n hn =>
  obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y
  obtain ⟨Y', ⟨e⟩⟩ := hn Y
  obtain ⟨f', hf'⟩ := exists_rightFraction L W
    ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)
  refine ⟨Y'.precomp f'.f,
    ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
  dsimp at hf' ⊢
  simp [← cancel_mono (e.inv.app 0), hf']

Result:
no goals

Proof state:
case zero
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.HasRightCalculusOfFractions
this : L.EssSurj
Y : ComposableArrows D 0
⊢ (L.mapComposableArrows 0).essImage Y

Tactic:
obtain ⟨Y, rfl⟩ := mk₀_surjective Y

Result:
case zero.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.HasRightCalculusOfFractions
this : L.EssSurj
Y : D
⊢ (L.mapComposableArrows 0).essImage (mk₀ Y)

Proof state:
case succ.intro.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ e.inv.app 0 = f'.map L ⋯
⊢ L.map f'.f ≫ e.hom.app 0 = (L.map f'.s ≫ (L.objObjPreimageIso Z).hom) ≫ f

Tactic:
simp [← cancel_mono (e.inv.app 0), hf']

Result:
no goals

Proof state:
case succ.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Tactic:
obtain ⟨Y', ⟨e⟩⟩ := hn Y

Result:
case succ.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Proof state:
case succ
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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D (n + 1)
⊢ (L.mapComposableArrows (n + 1)).essImage Y

Tactic:
obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y

Result:
case succ.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Proof state:
case succ.intro.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv = f'.map L ⋯
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Tactic:
refine ⟨Y'.precomp f'.f,
  ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩

Result:
case succ.intro.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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv = f'.map L ⋯
⊢ ((L.mapComposableArrows (n + 1)).obj (Y'.precomp f'.f)).map' 0 1 ⋯ ⋯ ≫ app' e.hom 0 ⋯ =
    (isoOfHom L W f'.s ⋯ ≪≫ L.objObjPreimageIso Z).hom ≫ (Y.precomp f).map' 0 1 ⋯ ⋯

Proof state:
case zero.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.HasRightCalculusOfFractions
this : L.EssSurj
Y : D
⊢ (L.mapComposableArrows 0).essImage (mk₀ Y)

Tactic:
exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩

Result:
no goals