awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₆ : F.map (a₂.f (W := W) ≫ t₂) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₆ : F.map (a₂.f (W := W) ≫ t₂) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₇ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₆ : F.map (a₂.f (W := W) ≫ t₂) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₇ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₈ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W)) ≫ F.map t₂
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₆ : F.map (a₂.f (W := W) ≫ t₂) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₇ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₈ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W)) ≫ F.map t₂
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₉ : F.map (a₂.f (W := W)) ≫ F.map t₂ = F.map (a₂.f (W := W)) ≫ F.map t₂
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X : C
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).map (W := W) F hF = 𝟙 (F.obj X)
have rw : (ofHom W (𝟙 X)).map (W := W) F hF = 𝟙 (F.obj X)
Tactic: rw [Hom.map_mk, map_ofHom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X : C
rw : (ofHom W (𝟙 X)).map (W := W) F hF = 𝟙 (F.obj X)
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).map (W := W) F hF = 𝟙 (F.obj X)
have rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
Tactic: rw [Hom.map_mk, map_ofHom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X : C
rw : (ofHom W (𝟙 X)).map (W := W) F hF = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).map (W := W) F hF = 𝟙 (F.obj X)
have rw₂ : Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
Tactic: rw [Hom.map_mk, map_ofHom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.map (W := W) (f ≫ g) F hF = Hom.map (W := W) f F hF ≫ Hom.map (W := W) g F hF
have obtain : ∀ (f : W.LeftFraction X Y),
  Hom.map (W := W) (Hom.mk (W := W) f ≫ g) F hF = (Hom.mk (W := W) f).map (W := W) F hF ≫ Hom.map (W := W) g F hF
Tactic: obtain ⟨f, rfl⟩ := Hom.mk_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
g : Y ⟶ Z
f : W.LeftFraction X Y
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ g) F hF = (Hom.mk (W := W) f).map (W := W) F hF ≫ Hom.map (W := W) g F hF
have obtain : ∀ (g : W.LeftFraction Y Z),
  Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF =
    (Hom.mk (W := W) f).map (W := W) F hF ≫ (Hom.mk (W := W) g).map (W := W) F hF
Tactic: obtain ⟨g, rfl⟩ := Hom.mk_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF =
    (Hom.mk (W := W) f).map (W := W) F hF ≫ (Hom.mk (W := W) g).map (W := W) F hF
have dsimp : Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
have obtain : ∀ (z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W)))
  (fac :
    (RightFraction.mk (W := W) (f.s (W := W)) sorry (g.f (W := W))).f (W := W) ≫ z.s (W := W) =
      (RightFraction.mk (W := W) (f.s (W := W)) sorry (g.f (W := W))).s (W := W) ≫ z.f (W := W)),
  Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
Tactic: obtain ⟨z, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
      (RightFraction.mk f.s f.hs g.f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac :
  (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).f (W := W) ≫ z.s (W := W) =
    (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).s (W := W) ≫ z.f (W := W)
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
have rw : (f.comp₀ (W := W) g z).map (W := W) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
Tactic: rw [homMk_comp_homMk f g z fac, Hom.map_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
⊢ (mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).map (W := W) F hF =
    f.map (W := W) F hF ≫ g.map (W := W) F hF
have this : IsIso (F.map (g.s (W := W)))
Tactic: have := hF _ g.hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this : IsIso (F.map (g.s (W := W)))
⊢ (mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).map (W := W) F hF =
    f.map (W := W) F hF ≫ g.map (W := W) F hF
have this₁ : IsIso (F.map (z.s (W := W)))
Tactic: have := hF _ z.hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
⊢ (mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).map (W := W) F hF =
    f.map (W := W) F hF ≫ g.map (W := W) F hF
have rw : F.map ((mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) sorry).f (W := W)) =
  f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
Tactic: rw [← cancel_mono (F.map g.s), assoc, map_comp_map_s,
      ← cancel_mono (F.map z.s), assoc, assoc, ← F.map_comp,
      ← F.map_comp, map_comp_map_s, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
⊢ F.map ((mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).f (W := W)) =
    f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
have dsimp : F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
⊢ F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
have rw : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
Tactic: rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
rw : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
⊢ F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
have rw₁ : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W)) ≫ F.map (z.f (W := W))
Tactic: rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
rw : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
rw₁ : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W)) ≫ F.map (z.f (W := W))
⊢ F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
have rw₂ : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = F.map (f.f (W := W)) ≫ F.map (z.f (W := W))
Tactic: rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ (Q W ⋙ lift (W := W) F hF).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
have dsimp : Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
Tactic: dsimp [lift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
have rw : Hom.map (W := W) (homMk (W := W) (ofHom W f)) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
Tactic: rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]