awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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)))
⊢ β.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))
have refine_3 : β.map (W := W) L sorry ≫ L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)) =
  ψ.thd (W := W).map (W := W) L sorry ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
Tactic: nth_rw 1 [L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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)))
⊢ β.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))
have refine_3 : L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = ψ.thd (W := W).map (W := W) L sorry ≫ L.map (β.s (W := W) ≫ γ.s (W := W))
Tactic: rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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))
⊢ β.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))
have refine_3₁ : L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = L.map (ψ.thd (W := W).f (W := W))
Tactic: rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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))
⊢ β.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))
have refine_3₂ : L.map (β.f (W := W)) ≫ L.map (γ.s (W := W)) = L.map (β.f (W := W)) ≫ L.map (γ.s (W := W))
Tactic: rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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
⊢ F.Faithful
have this : L.EssSurj
Tactic: have := Localization.essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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
have refine : ∀ (X₁ X₂ : C) (f g : L.obj X₁ ⟶ L.obj X₂) (hfg : F.map f = F.map g), f = g
Tactic: refine F.faithful_of_comp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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
⊢ f = g
have obtain : ∀ (φ : W.LeftFraction₂ X₁ X₂) (hfg : F.map (φ.fst (W := W).map (W := W) L sorry) = F.map (φ.snd (W := W).map (W := W) L sorry)),
  φ.fst (W := W).map (W := W) L sorry = φ.snd (W := W).map (W := W) L sorry
Tactic: obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g
Cleared hypotheses: f, g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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 ⋯)
⊢ φ.fst (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
have rw : L.map (φ.fst (W := W).f (W := W)) = L.map (φ.snd (W := W).f (W := W))
Tactic: rw [← cancel_mono (L.map φ.s), φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (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
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 ⋯)
⊢ L.map (φ.fst (W := W).f (W := W)) = L.map (φ.snd (W := W).f (W := W))
have a : F.map (L.map (φ.fst (W := W).f (W := W))) = F.map (L.map (φ.snd (W := W).f (W := W)))
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y : C₁
φ : W.RightFraction X Y
⊢ ∃ (ψ : W.LeftFraction X Y), φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W)
have obtain : ∀ (T : C₁) (s : T ⟶ X) (w : W s) (f : T ⟶ Y),
  ∃ (ψ : W.LeftFraction X Y),
    (RightFraction.mk (W := W) s w f).f (W := W) ≫ ψ.s (W := W) =
      (RightFraction.mk (W := W) s w f).s (W := W) ≫ ψ.f (W := W)
Tactic: obtain ⟨T, s, _, f, rfl⟩ := φ.cases
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
⊢ ∃ (ψ : W.LeftFraction X Y),
    (RightFraction.mk (W := W) s w f).f (W := W) ≫ ψ.s (W := W) =
      (RightFraction.mk (W := W) s w f).s (W := W) ≫ ψ.f (W := W)
have dsimp : ∃ (ψ : W.LeftFraction X Y), f ≫ ψ.s (W := W) = s ≫ ψ.f (W := W)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
⊢ ∃ (ψ : W.LeftFraction X Y), f ≫ ψ.s (W := W) = s ≫ ψ.f (W := W)
have this : IsIso (G.map s)
Tactic: have := hW s (by assumption)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this : IsIso (G.map s)
⊢ f ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).s (W :=
        W) =
    s ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).f (W :=
        W)
have this₁ : Functor.map (𝟭 C₁) s ≫ adj.unit.app X = adj.unit.app T ≫ (G ⋙ F).map s
Tactic: have := adj.unit.naturality s
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : Functor.map (𝟭 C₁) s ≫ adj.unit.app X = adj.unit.app T ≫ (G ⋙ F).map s
⊢ f ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).s (W :=
        W) =
    s ≫
      (LeftFraction.mk (W := W) (adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)) (adj.unit.app Y) ⋯).f (W :=
        W)
have dsimp : f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
have rw : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
Tactic: rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
rw : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
have rw₁ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)
Tactic: rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
rw : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
rw₁ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
have rw₂ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map f)
Tactic: rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w : W s
f : T ⟶ Y
this_1 : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
rw : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
rw₁ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)
rw₂ : f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map f)
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
have rw₃ : f ≫ adj.unit.app Y = f ≫ adj.unit.app Y
Tactic: rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
⊢ ∃ (Y' : C₁) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t
have this : IsIso (G.map s)
Tactic: have := hW s (by assumption)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ ∃ (Y' : C₁) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t
have refine : f₁ ≫ adj.unit.app Y = f₂ ≫ adj.unit.app Y
Tactic: refine ⟨_, adj.unit.app Y, hW' _, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ f₁ ≫ adj.unit.app Y = f₂ ≫ adj.unit.app Y
have rw : adj.unit.app X ≫ F.map (G.map f₁) = adj.unit.app X ≫ F.map (G.map f₂)
Tactic: rw [← adj.unit_naturality f₁, ← adj.unit_naturality f₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ adj.unit.app X ≫ F.map (G.map f₁) = adj.unit.app X ≫ F.map (G.map f₂)
have e_a : G.map f₁ = G.map f₂
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map f₁ = G.map f₂
have e_a : G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂
Tactic: rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
e_a : G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂
⊢ G.map f₁ = G.map f₂
have e_a₁ : G.map (s ≫ f₁) = G.map s ≫ G.map f₂
Tactic: rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
e_a : G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂
e_a₁ : G.map (s ≫ f₁) = G.map s ≫ G.map f₂
⊢ G.map f₁ = G.map f₂
have e_a₂ : G.map (s ≫ f₁) = G.map (s ≫ f₂)
Tactic: rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
inst_2 : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
h_1 : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
e_a : G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂
e_a₁ : G.map (s ≫ f₁) = G.map s ≫ G.map f₂
e_a₂ : G.map (s ≫ f₁) = G.map (s ≫ f₂)
⊢ G.map f₁ = G.map f₂
have e_a₃ : G.map (s ≫ f₂) = G.map (s ≫ f₂)
Tactic: rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
⊢ IsIso (Functor.whiskerRight adj.unit W.Q)
have rw : ∀ (X : C₁), IsIso ((Functor.whiskerRight adj.unit W.Q).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
W : MorphismProperty.{v_1, u_1} C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift (W := W) G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac (W := W) G hW W.Q
⊢ G.IsLocalization W
have this : IsIso (Functor.whiskerRight adj.unit W.Q)
Tactic: have : IsIso (Functor.whiskerRight adj.unit W.Q) := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro X
    exact Localization.inverts W.Q W _ (hW' X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : G ⊣ F
j : C₁
⊢ inverseImage (isomorphisms C₂) G (adj.unit.app j)
have simp : IsIso (G.map (adj.unit.app j))
Tactic: simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]