-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma map_eq_iff {X Y : C} (f g : LeftFraction W X Y) :
    f.map (LeftFraction.Localization.Q W) (Localization.inverts _ _) =
        g.map (LeftFraction.Localization.Q W) (Localization.inverts _ _) ↔
      LeftFractionRel f g

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯ ↔ LeftFractionRel f g

Tactic:
simp only [← Hom.map_mk _ (Q W)]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ ↔ LeftFractionRel f g

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ → LeftFractionRel f g

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ LeftFractionRel f g

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel f g
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯

Tactic:
congr 1

Result:
case mpr.e_f
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel f g
⊢ Hom.mk f = Hom.mk g

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ LeftFractionRel f g → (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel f g
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ ↔ LeftFractionRel f g

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ → LeftFractionRel f g

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ LeftFractionRel f g → (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ LeftFractionRel f g

Tactic:
rw [← homMk_eq_iff_leftFractionRel, homMk_eq, homMk_eq]

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯

Proof state:
case mpr.e_f
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel f g
⊢ Hom.mk f = Hom.mk g

Tactic:
exact Quot.sound h

Result:
no goals