awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
refine_2 :
  L.map (φ'.f (W := W)) ≫ L.map (α.s (W := W)) = ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))
refine_2₁ : L.map (φ'.f (W := W)) ≫ L.map (α.s (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₂ refine_2₃ : L.map (φ'.f (W := W)) ≫ L.map (α.s (W := W)) = L.map (φ'.f (W := W)) ≫ L.map (α.s (W := W))
⊢ φ'.map (W := W) L ⋯ ≫ L.map (φ'.s (W := W)) ≫ L.map (α.s (W := W)) =
    ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))

Tactic:
rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s,
      L.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
obtain :
  ∀ (α : W.LeftFraction₂ X Y) (hα : f = α.fst (W := W).map (W := W) L ⋯) (hα' : f' = α.snd (W := W).map (W := W) L ⋯),
    ∃ (φ : W.LeftFraction₃ X Y),
      f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₃ X Y),
    f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨α, hα, hα'⟩ := exists_leftFraction₂ L W f f'

Premises used: CategoryTheory.Localization.exists_leftFraction₂
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
have :
  ∀ (β : W.LeftFraction X Y) (hβ : f'' = β.map (W := W) L ⋯),
    ∃ (φ : W.LeftFraction₃ X Y),
      f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₃ X Y),
    f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯

Tactic:
have ⟨β, hβ⟩ := exists_leftFraction L W f''
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
obtain :
  ∀ (γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W)))
    (hγ :
      (RightFraction.mk (W := W) (α.s (W := W)) ⋯ (β.s (W := W))).f (W := W) ≫ γ.s (W := W) =
        (RightFraction.mk (W := W) (α.s (W := W)) ⋯ (β.s (W := W))).s (W := W) ≫ γ.f (W := W)),
    ∃ (φ : W.LeftFraction₃ X Y),
      f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₃ X Y),
    f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.s).exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.LeftFraction₂.hs, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.LeftFraction.s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
rw : IsIso (L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)))
⊢ IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))

Tactic:
rw [L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
⊢ IsIso (L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
⊢ IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))

Tactic:
have : IsIso (L.map (β.s ≫ γ.s)) := by
    rw [L.map_comp]
    infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
⊢ ∃ (φ : W.LeftFraction₃ X Y),
    f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯

Tactic:
⟨ψ, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_1 : f = ψ.fst (W := W).map (W := W) L ⋯
refine_2 : f' = ψ.snd (W := W).map (W := W) L ⋯
refine_3 : f'' = ψ.thd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₃ X Y),
    f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯ ∧ f'' = φ.thd (W := W).map (W := W) L ⋯

Tactic:
refine ⟨ψ, ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_1 :
  f ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = ψ.fst (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
refine_1₁ : f ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₂ : α.fst (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₃ : α.fst (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W) ≫ γ.f (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₄ :
  α.fst (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W)) ≫ L.map (γ.f (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₅ : L.map (α.fst (W := W).f (W := W)) ≫ L.map (γ.f (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₆ refine_1₇ :
  L.map (α.fst (W := W).f (W := W)) ≫ L.map (γ.f (W := W)) = L.map (α.f (W := W)) ≫ L.map (γ.f (W := W))
⊢ f = ψ.fst (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), LeftFraction.map_comp_map_s, hα, hγ,
      L.map_comp, LeftFraction.map_comp_map_s_assoc, L.map_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_2 :
  f' ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
refine_2₁ : f' ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₂ : α.snd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₃ : α.snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W) ≫ γ.f (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₄ :
  α.snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W)) ≫ L.map (γ.f (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₅ : L.map (α.snd (W := W).f (W := W)) ≫ L.map (γ.f (W := W)) = L.map (ψ.snd (W := W).f (W := W))
refine_2₆ refine_2₇ :
  L.map (α.snd (W := W).f (W := W)) ≫ L.map (γ.f (W := W)) = L.map (α.f' (W := W)) ≫ L.map (γ.f (W := W))
⊢ f' = ψ.snd (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), LeftFraction.map_comp_map_s, hα', hγ,
      L.map_comp, LeftFraction.map_comp_map_s_assoc, L.map_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_3 :
  β.map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) =
    ψ.thd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
⊢ f'' = ψ.thd (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), hβ]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_3 :
  β.map (W := W) L ⋯ ≫ L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)) =
    ψ.thd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
⊢ β.map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W)) =
    ψ.thd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))

Tactic:
nth_rw 1 [L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst (W := W).map (W := W) L ⋯
hα' : f' = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.s (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
ψ : W.LeftFraction₃ X Y :=
  LeftFraction₃.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.f (W := W) ≫ γ.s (W := W))
    (β.s (W := W) ≫ γ.s (W := W)) ⋯
this : IsIso (L.map (β.s (W := W) ≫ γ.s (W := W)))
refine_3 :
  L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = ψ.thd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
refine_3₁ : L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = L.map (ψ.thd (W := W).f (W := W))
refine_3₂ refine_3₃ : L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = L.map (β.f (W := W)) ≫ L.map (γ.s (W := W))
⊢ β.map (W := W) L ⋯ ≫ L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)) =
    ψ.thd (W := W).map (W := W) L ⋯ ≫ L.map (β.s (W := W) ≫ γ.s (W := W))

Tactic:
rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
⊢ F.Faithful

Tactic:
F.faithful_of_comp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_)

Premises used: CategoryTheory.Functor.faithful_of_comp_essSurj
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
refine : ∀ (X₁ X₂ : C) (f g : L.obj X₁ ⟶ L.obj X₂) (hfg : F.map f = F.map g), f = g
⊢ F.Faithful

Tactic:
refine F.faithful_of_comp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_)

Premises used: CategoryTheory.Functor.faithful_of_comp_essSurj
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
f g : L.obj X₁ ⟶ L.obj X₂
hfg : F.map f = F.map g
obtain :
  ∀ (φ : W.LeftFraction₂ X₁ X₂)
    (hfg : F.map (φ.fst (W := W).map (W := W) L ⋯) = F.map (φ.snd (W := W).map (W := W) L ⋯)),
    φ.fst (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
⊢ f = g

Tactic:
obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g

Premises used: CategoryTheory.Localization.exists_leftFraction₂, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst (W := W).map (W := W) L ⋯) = F.map (φ.snd (W := W).map (W := W) L ⋯)
rw : L.map (φ.fst (W := W).f (W := W)) = L.map (φ.snd (W := W).f (W := W))
⊢ φ.fst (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map φ.s), φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.MorphismProperty.LeftFraction₂.snd, CategoryTheory.MorphismProperty.LeftFraction₂.fst, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst (W := W).map (W := W) L ⋯) = F.map (φ.snd (W := W).map (W := W) L ⋯)
a : F.map (L.map (φ.fst (W := W).f (W := W))) = F.map (L.map (φ.snd (W := W).f (W := W)))
⊢ L.map (φ.fst (W := W).f (W := W)) = L.map (φ.snd (W := W).f (W := W))

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_4 : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst (W := W).map (W := W) L ⋯) = F.map (φ.snd (W := W).map (W := W) L ⋯)
⊢ F.map (L.map (φ.fst (W := W).f (W := W))) = F.map (L.map (φ.snd (W := W).f (W := W)))

Tactic:
simpa only [← F.map_comp, φ.fst.map_comp_map_s, φ.snd.map_comp_map_s] using
    hfg =≫ F.map (L.map φ.s)

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.MorphismProperty.LeftFraction₂.snd, CategoryTheory.MorphismProperty.LeftFraction₂.fst, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s