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

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

Tactic:
simp only [← cancel_mono (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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
t₁ : (LeftFraction.ofHom W f₁).Y' ⟶ Z
t₂ : (LeftFraction.ofHom W f₂).Y' ⟶ Z
hst : (LeftFraction.ofHom W f₁).s ≫ t₁ = (LeftFraction.ofHom W f₂).s ≫ t₂
hft : (LeftFraction.ofHom W f₁).f ≫ t₁ = (LeftFraction.ofHom W f₂).f ≫ t₂
ht : W ((LeftFraction.ofHom W f₁).s ≫ t₁)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

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

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

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

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

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

Tactic:
simpa using ht

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

Tactic:
simp only [id_comp] 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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
t₁ t₂ : Y ⟶ Z
hft : f₁ ≫ t₁ = f₂ ≫ t₂
ht : W (𝟙 Y ≫ t₁)
hst : t₁ = t₂
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

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

Tactic:
rw [← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
  ← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
  LeftFraction.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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
h : LeftFractionRel (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

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

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

Result:
no goals

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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
h : LeftFractionRel (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

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

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

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

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