-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma trans {X Y : C} {z₁ z₂ z₃ : W.LeftFraction X Y}
    [HasLeftCalculusOfFractions W]
    (h₁₂ : LeftFractionRel z₁ z₂) (h₂₃ : LeftFractionRel z₂ z₃) :
    LeftFractionRel z₁ z₃

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ LeftFractionRel z₁ z₃

Tactic:
refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.s ≫ t₁ ≫ v₄ ≫ w = z₃.s ≫ u₃ ≫ v₅ ≫ w

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.f ≫ t₁ ≫ v₄ ≫ w = z₃.f ≫ u₃ ≫ v₅ ≫ w

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_3
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W (z₁.s ≫ t₁ ≫ v₄ ≫ w)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_3
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W (z₁.s ≫ t₁ ≫ v₄ ≫ w)

Tactic:
rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.assoc]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_3
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s ≫ u₂) ≫ v₅ ≫ w)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
h₁₂ : LeftFractionRel z₁ z₂
h₂₃ : LeftFractionRel z₂ z₃
⊢ LeftFractionRel z₁ z₃

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

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
h₂₃ : LeftFractionRel z₂ z₃
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁ z₃

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.refine_3
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s ≫ u₂) ≫ v₅ ≫ w)

Tactic:
exact W.comp_mem _ _ hu (W.comp_mem _ _ hv₅ hw)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac :
  (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃)).f ≫ (LeftFraction.mk v₄ v₅ hv₅).s =
    (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃)).s ≫ (LeftFraction.mk v₄ v₅ hv₅).f
⊢ LeftFractionRel z₁ z₃

Tactic:
simp only [Category.assoc] at fac

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
⊢ LeftFractionRel z₁ z₃