awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (goal)
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst_4 : RF.IsRightDerivedFunctor α W
this :
  α =
    Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom
⊢ IsIso α
have rw : IsIso
  (Iso.inv (Localization.fac (W := W) F hF L) ≫
    L.whiskerLeft
      ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α
have mp : RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
mp : RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α
have mpr : RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W
have simp : RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'
Tactic: simp only [isRightDerivedFunctor_iff_isLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X
have dsimp : α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X
Tactic: dsimp only [rightDerivedNatTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
⊢ G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)
have rw : G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
Tactic: rw [isRightDerivedFunctor_iff_isLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (hypothesis)
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
have this : RF.IsLeftKanExtension α
Tactic: have := IsRightDerivedFunctor.isLeftKanExtension _ α W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (hypothesis)
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
have this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
Tactic: have : HasRightDerivedFunctor F W ↔ HasLeftKanExtension W.Q F :=
    ⟨fun h => h.hasLeftKanExtension', fun h => ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
have rw : W.Q.HasLeftKanExtension F ↔ L.HasLeftKanExtension F
Tactic: rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
rw : W.Q.HasLeftKanExtension F ↔ L.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
have rw₁ : W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F
Tactic: rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_2} H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
e : F ≅ F'
W : MorphismProperty.{v_1, u_1} C
⊢ F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
have rw : W.Q.HasLeftKanExtension F ↔ F'.HasRightDerivedFunctor W
Tactic: rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
    hasLeftExtension_iff_of_iso₂ W.Q e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_2} H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
e : F ≅ F'
W : MorphismProperty.{v_1, u_1} C
rw : W.Q.HasLeftKanExtension F ↔ F'.HasRightDerivedFunctor W
⊢ F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
have rw₁ : W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F'
Tactic: rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
    hasLeftExtension_iff_of_iso₂ W.Q e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (goal)
Goal:
C : Type u_1
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_2} H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
e : F ≅ F'
W : MorphismProperty.{v_1, u_1} C
rw : W.Q.HasLeftKanExtension F ↔ F'.HasRightDerivedFunctor W
rw₁ : W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F'
⊢ F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
have rw₂ : W.Q.HasLeftKanExtension F' ↔ W.Q.HasLeftKanExtension F'
Tactic: rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
    hasLeftExtension_iff_of_iso₂ W.Q e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.RightDerived (hypothesis)
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
⊢ F.HasRightDerivedFunctor W
have this : RF.IsLeftKanExtension α
Tactic: have := IsRightDerivedFunctor.isLeftKanExtension RF α W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesMonomorphisms
inst_4 : G.PreservesMonomorphisms
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono ((F ⋙ G).map f)
have rw : Mono (G.map (F.map f))
Tactic: rw [comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesEpimorphisms
inst_4 : G.PreservesEpimorphisms
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi ((F ⋙ G).map f)
have rw : Epi (G.map (F.map f))
Tactic: rw [comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesMonomorphisms
f : G ⟶ F
inst_3 : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (G.map π)
have suffices : Mono (G.map π ≫ f.app Y)
Tactic: suffices Mono (G.map π ≫ f.app Y) from mono_of_mono (G.map π) (f.app Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesMonomorphisms
f : G ⟶ F
inst_3 : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (G.map π ≫ f.app Y)
have rw : Mono (f.app X ≫ F.map π)
Tactic: rw [f.naturality π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesEpimorphisms
f : F ⟶ G
inst_3 : ∀ (X : C), Epi (f.app X)
X Y : C
π : X ⟶ Y
hπ : Epi π
⊢ Epi (G.map π)
have suffices : Epi (f.app X ≫ G.map π)
Tactic: suffices Epi (f.app X ≫ G.map π) from epi_of_epi (f.app X) (G.map π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesEpimorphisms
f : F ⟶ G
inst_3 : ∀ (X : C), Epi (f.app X)
X Y : C
π : X ⟶ Y
hπ : Epi π
⊢ Epi (f.app X ≫ G.map π)
have rw : Epi (F.map π ≫ f.app Y)
Tactic: rw [← f.naturality π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono f
have apply : Mono (F.map f)
Tactic: apply F.mono_of_mono_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono (F.map f)
have suffices : F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
Tactic: suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ mono_comp _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi f
have apply : Epi (F.map f)
Tactic: apply F.epi_of_epi_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)
have suffices : F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
Tactic: suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ epi_comp _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h
have H₁ : Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
  ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
Tactic: replace H := congr_arg (adj.homEquiv X Z) H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H :
  Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
⊢ g = h
have rwa : ∀
  (H :
    Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
      ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h))),
  g = h
Tactic: rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H :
  Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
rwa :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h))),
    g = h
⊢ g = h
have rwa₁ : ∀
  (H :
    Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
      (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h)),
  g = h
Tactic: rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H :
  Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
rwa :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h))),
    g = h
rwa₁ :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h)),
    g = h
⊢ g = h
have rwa₂ : ∀
  (H :
    Eq.{v₁ + 1} (α := Y ⟶ G.obj Z) ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g : Y ⟶ G.obj Z)
      ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h : Y ⟶ G.obj Z)),
  g = h
Tactic: rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H :
  Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
rwa :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h))),
    g = h
rwa₁ :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h)),
    g = h
rwa₂ :
  ∀
    (H :
      Eq.{v₁ + 1} (α := Y ⟶ G.obj Z) ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g : Y ⟶ G.obj Z)
        ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h : Y ⟶ G.obj Z)),
    g = h
⊢ g = h
have rwa₃ : ∀ (H : g = h), g = h
Tactic: rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h
have H₁ : Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
  (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
Tactic: replace H := congr_arg (adj.homEquiv Z Y).symm H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H :
  Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
⊢ g = h
have rwa : ∀
  (H :
    Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
      (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)),
  g = h
Tactic: rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H :
  Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
rwa :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)),
    g = h
⊢ g = h
have rwa₁ : ∀
  (H :
    Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
      (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h ≫ f : F.obj Z ⟶ Y)),
  g = h
Tactic: rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H :
  Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
rwa :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)),
    g = h
rwa₁ :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h ≫ f : F.obj Z ⟶ Y)),
    g = h
⊢ g = h
have rwa₂ : ∀
  (H :
    Eq.{v₂ + 1} (α := F.obj Z ⟶ X) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g : F.obj Z ⟶ X)
      (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h : F.obj Z ⟶ X)),
  g = h
Tactic: rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H :
  Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
rwa :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)),
    g = h
rwa₁ :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h ≫ f : F.obj Z ⟶ Y)),
    g = h
rwa₂ :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ X) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g : F.obj Z ⟶ X)
        (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h : F.obj Z ⟶ X)),
    g = h
⊢ g = h
have rwa₃ : ∀ (H : g = h), g = h
Tactic: rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f
have rw : F.map (g ≫ f) = F.map h ≫ F.map f
Tactic: rw [← F.map_comp, hgh, F.map_comp]