awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y : C × D ⥤ E
T : X_1 ⟶ Y
X X' : C
f : X ⟶ X'
x : D
⊢ NatTrans.app (X_1.curryObj.map f ≫ { app := fun (Y_1 : D) ↦ T.app (X', Y_1), naturality := ⋯ }) x =
    NatTrans.app
      ({ app := fun (Y_1 : D) ↦ T.app (X, Y_1), naturality := ⋯ : NatTrans (X_1.curryObj.obj X) (Y.curryObj.obj X) } ≫
        Y.curryObj.map f)
      x
have w : X_1.map (f ×ₘ 𝟙 x) ≫ T.app (X', x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)
Tactic: dsimp [curryObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y : C × D ⥤ E
T : X_1 ⟶ Y
X X' : C
f : X ⟶ X'
x : D
⊢ X_1.map (f ×ₘ 𝟙 x) ≫ T.app (X', x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)
have w : T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X₁ : C
X₂ : D
Y₁ : C
Y₂ : D
f₁ : (X₁, X₂).1 ⟶ (Y₁, Y₂).1
f₂ : (X₁, X₂).2 ⟶ (Y₁, Y₂).2
⊢ (obj (curry ⋙ uncurry) F).map (f₁, f₂) ≫
      Iso.hom
        ((fun (x : C × D) ↦
            (Iso.refl ((obj (curry ⋙ uncurry) F).obj x) :
              (obj (curry ⋙ uncurry) F).obj x ≅ (obj (curry ⋙ uncurry) F).obj x))
          (Y₁, Y₂)) =
    Iso.hom
        ((fun (x : C × D) ↦
            (Iso.refl ((obj (curry ⋙ uncurry) F).obj x) :
              (obj (curry ⋙ uncurry) F).obj x ≅ (obj (curry ⋙ uncurry) F).obj x))
          (X₁, X₂)) ≫
      (obj (𝟭 (C × D ⥤ E)) F).map (f₁, f₂)
have dsimp : (F.map (f₁ ×ₘ 𝟙 X₂) ≫ F.map (𝟙 Y₁ ×ₘ f₂)) ≫ 𝟙 (F.obj (Y₁, Y₂)) = 𝟙 (F.obj (X₁, X₂)) ≫ F.map (f₁, f₂)
Tactic: dsimp at f₁ f₂ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F : B × C ⥤ D
x x_1 : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (obj uncurry (obj curry F)).map (f₁, f₂) = eqToHom ⋯ ≫ F.map (f₁, f₂) ≫ eqToHom ⋯
have dsimp : F.map (f₁ ×ₘ 𝟙 x₂) ≫ F.map (𝟙 y₁ ×ₘ f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (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₁ F₂ : C × D ⥤ E
h : obj curry F₁ = obj curry F₂
⊢ F₁ = F₂
have rw : obj uncurry (obj curry F₁) = F₂
Tactic: rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (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₁ F₂ : C × D ⥤ E
h : obj curry F₁ = obj curry F₂
rw : obj uncurry (obj curry F₁) = F₂
⊢ F₁ = F₂
have rw₁ : obj uncurry (obj curry F₁) = obj uncurry (obj curry F₂)
Tactic: rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (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₁ F₂ : C × D ⥤ E
h : obj curry F₁ = obj curry F₂
rw : obj uncurry (obj curry F₁) = F₂
rw₁ : obj uncurry (obj curry F₁) = obj uncurry (obj curry F₂)
⊢ F₁ = F₂
have rw₂ : obj uncurry (obj curry F₂) = obj uncurry (obj curry F₂)
Tactic: rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : obj uncurry F₁ = obj uncurry F₂
⊢ F₁ = F₂
have rw : obj curry (obj uncurry F₁) = F₂
Tactic: rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : obj uncurry F₁ = obj uncurry F₂
rw : obj curry (obj uncurry F₁) = F₂
⊢ F₁ = F₂
have rw₁ : obj curry (obj uncurry F₁) = obj curry (obj uncurry F₂)
Tactic: rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : obj uncurry F₁ = obj uncurry F₂
rw : obj curry (obj uncurry F₁) = F₂
rw₁ : obj curry (obj uncurry F₁) = obj curry (obj uncurry F₂)
⊢ F₁ = F₂
have rw₂ : obj curry (obj uncurry F₂) = obj curry (obj uncurry F₂)
Tactic: rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : F₁.flip = F₂.flip
⊢ F₁ = F₂
have rw : F₁.flip.flip = F₂
Tactic: rw [← flip_flip F₁, ← flip_flip F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : F₁.flip = F₂.flip
rw : F₁.flip.flip = F₂
⊢ F₁ = F₂
have rw₁ : F₁.flip.flip = F₂.flip.flip
Tactic: rw [← flip_flip F₁, ← flip_flip F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : F₁.flip = F₂.flip
rw : F₁.flip.flip = F₂
rw₁ : F₁.flip.flip = F₂.flip.flip
⊢ F₁ = F₂
have rw₂ : F₂.flip.flip = F₂.flip.flip
Tactic: rw [← flip_flip F₁, ← flip_flip F₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
x x_1 : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (obj uncurry (F₂ ⋙ (F₁ ⋙ obj curry G).flip).flip).map (f₁, f₂) = eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯
have dsimp : G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
  𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
x x_1 : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (obj uncurry (F₁ ⋙ (F₂ ⋙ (obj curry G).flip).flip)).map (f₁, f₂) =
    eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯
have dsimp : G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
  𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.CurryingThree (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X Y : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X ⟶ Y
x x_1 : C₁
g : x ⟶ x_1
⊢ X.flip₂₃.map g ≫
      {
        app := fun (Y_1 : C₃) ↦
          { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := ⋯ :
            NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
        naturality := ⋯ : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) } =
    {
        app := fun (Y_1 : C₃) ↦
          { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := ⋯ :
            NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
        naturality := ⋯ : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
      Y.flip₂₃.map g
have w : ∀ (x_2 : C₃) (x_3 : C₂),
  ((X.flip₂₃.map g ≫
              {
                app := fun (Y_1 : C₃) ↦
                  { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := sorry :
                    NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
                naturality := sorry : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) }).app
          x_2).app
      x_3 =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (Y_1 : C₃) ↦
              { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := sorry :
                NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
            naturality := sorry : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
          Y.flip₂₃.map g)
        x_2)
      x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.CurryingThree (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X Y : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X ⟶ Y
x x_1 : C₁
g : x ⟶ x_1
x_2 : C₃
x_3 : C₂
⊢ ((X.flip₂₃.map g ≫
              {
                app := fun (Y_1 : C₃) ↦
                  { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := ⋯ :
                    NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
                naturality := ⋯ : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) }).app
          x_2).app
      x_3 =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (Y_1 : C₃) ↦
              { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := ⋯ :
                NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
            naturality := ⋯ : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
          Y.flip₂₃.map g)
        x_2)
      x_3
have w : ((X.map g).app x_3).app x_2 ≫ ((f.app x_1).app x_3).app x_2 = ((f.app x).app x_3).app x_2 ≫ ((Y.map g).app x_3).app x_2
Tactic: simp only [flip₂₃_obj_obj_obj, NatTrans.comp_app, flip₂₃_map_app_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
⊢ ∀ (X : D₁), G'.map (η.app X) ≫ ε.app (G'.obj X) = 𝟙 (G'.obj X)
have suffices : G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom = 𝟙 G'
Tactic: suffices G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (Functor.associator _ _ _).hom ≫
        whiskerLeft G' ε ≫ G'.rightUnitor.hom = 𝟙 _ from
      fun Y₁ ↦ by simpa using congr_app this Y₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
⊢ G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom = 𝟙 G'
have hγ : L₁.whiskerLeft
      (G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
    α =
  L₁.whiskerLeft (𝟙 G') ≫ α
Tactic: apply G'.leftDerived_ext α W₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
⊢ L₁.whiskerLeft
        (G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
      α =
    L₁.whiskerLeft (𝟙 G') ≫ α
have hγ : ∀ (X₁ : C₁),
  (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
Tactic: ext X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
have eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ map (𝟭 D₂) (α.app X₁)
Tactic: have eq₁ := ε.naturality (α.app X₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ map (𝟭 D₂) (α.app X₁)
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
have eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
Tactic: have eq₂ := G'.congr_map (hη X₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ map (𝟭 D₂) (α.app X₁)
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
have eq₃ : (L₁ ⋙ G').map (adj.unit.app X₁) ≫ α.app ((G ⋙ F).obj X₁) =
  α.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₁) X₁) ≫ (G ⋙ L₂).map (adj.unit.app X₁)
Tactic: have eq₃ := α.naturality (adj.unit.app X₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ map (𝟭 D₂) (α.app X₁)
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
eq₃ :
  (L₁ ⋙ G').map (adj.unit.app X₁) ≫ α.app ((G ⋙ F).obj X₁) =
    α.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₁) X₁) ≫ (G ⋙ L₂).map (adj.unit.app X₁)
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
have hγ : (𝟙 (G'.obj (L₁.obj X₁)) ≫
      G'.map (η.app (L₁.obj X₁)) ≫
        𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ 𝟙 (G'.obj (L₁.obj X₁))) ≫
    α.app X₁ =
  𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Tactic: dsimp at eq₁ eq₂ eq₃ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.Adjunction (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
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
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
⊢ (𝟙 (G'.obj (L₁.obj X₁)) ≫
        G'.map (η.app (L₁.obj X₁)) ≫
          𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ 𝟙 (G'.obj (L₁.obj X₁))) ≫
      α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
have eq₄ : G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
Tactic: simp only [Functor.map_comp] at eq₂
Cleared hypotheses: eq₂