-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma MorphismProperty.map_eq_iff_precomp {Y Z : C} (f₁ f₂ : Y ⟶ Z) :
    L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂

Proof state:
case mpr.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
s : Z ⟶ Y
hs : W s
fac : s ≫ f₁ = s ≫ f₂
⊢ L.map f₁ = L.map f₂

Tactic:
simp only [← cancel_epi (Localization.isoOfHom L W s hs).hom,
  Localization.isoOfHom_hom, ← L.map_comp, fac]

Result:
no goals

Proof state:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ : Z ⟶ (RightFraction.ofHom W f₁).X'
t₂ : Z ⟶ (RightFraction.ofHom W f₂).X'
hst : t₁ ≫ (RightFraction.ofHom W f₁).s = t₂ ≫ (RightFraction.ofHom W f₂).s
hft : t₁ ≫ (RightFraction.ofHom W f₁).f = t₂ ≫ (RightFraction.ofHom W f₂).f
ht : W (t₁ ≫ (RightFraction.ofHom W f₁).s)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
dsimp at t₁ t₂ hst hft ht

Result:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hst : t₁ ≫ 𝟙 Y = t₂ ≫ 𝟙 Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Proof state:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
h : RightFractionRel (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

Result:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ : Z ⟶ (RightFraction.ofHom W f₁).X'
t₂ : Z ⟶ (RightFraction.ofHom W f₂).X'
hst : t₁ ≫ (RightFraction.ofHom W f₁).s = t₂ ≫ (RightFraction.ofHom W f₂).s
hft : t₁ ≫ (RightFraction.ofHom W f₁).f = t₂ ≫ (RightFraction.ofHom W f₂).f
ht : W (t₁ ≫ (RightFraction.ofHom W f₁).s)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ 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.HasRightCalculusOfFractions
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
hst : t₁ = t₂
⊢ t₁ ≫ f₁ = t₁ ≫ f₂

Tactic:
rw [hft, hst]

Result:
no goals

Proof state:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hst : t₁ ≫ 𝟙 Y = t₂ ≫ 𝟙 Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
simp only [comp_id] at hst

Result:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
hst : t₁ = t₂
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ 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.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ ↔ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
constructor

Result:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ → ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

case mpr
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
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ (∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂

Proof state:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
h : L.map f₁ = L.map f₂
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
rw [← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
  ← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
  RightFraction.map_eq_iff] at h

Result:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
h : RightFractionRel (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Proof state:
case mp.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
hst : t₁ = t₂
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
exact ⟨Z, t₁, by simpa using ht, by rw [hft, hst]⟩

Result:
no goals

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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
hst : t₁ = t₂
⊢ W t₁

Tactic:
simpa using ht

Result:
no goals

Proof state:
case mpr
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
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ (∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂

Tactic:
rintro ⟨Z, s, hs, fac⟩

Result:
case mpr.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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
s : Z ⟶ Y
hs : W s
fac : s ≫ f₁ = s ≫ f₂
⊢ L.map f₁ = L.map f₂

Proof state:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ → ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
intro h

Result:
case mp
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
Y Z : C
f₁ f₂ : Y ⟶ Z
h : L.map f₁ = L.map f₂
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂