awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
⊢ (𝟙 (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 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: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
⊢ (𝟙 (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 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: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
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₁
⊢ (𝟙 (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 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: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
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₁
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₁
⊢ (𝟙 (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 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₁)) ≫ α.app X₁ =
  𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
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₁
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₁
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₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.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 hγ₄ : G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
  𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
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₁
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₁
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₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
hγ₄ :
  G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.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 hγ₅ : G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = 𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app 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₁))
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₁))
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₁
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₁
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₁
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₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
hγ₄ :
  G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
hγ₅ : G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = 𝟙 (G'.obj (L₁.obj X₁)) ≫ α.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 hγ₆ : G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = α.app X₁
Tactic: rw [Category.assoc, Category.assoc, Category.assoc, Category.comp_id,
      Category.id_comp, Category.id_comp, Category.id_comp, ← eq₁, reassoc_of% eq₂,
      hε (G.obj X₁), reassoc_of% eq₃, ← L₂.map_comp, adj.left_triangle_components,
      Functor.map_id, Category.comp_id]
-- 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₂)
⊢ ∀ (Y : D₂), η.app (F'.obj Y) ≫ F'.map (ε.app Y) = 𝟙 (F'.obj Y)
have suffices : F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 F'
Tactic: suffices F'.leftUnitor.inv ≫ whiskerLeft F' η ≫ (Functor.associator _ _ _).inv ≫
      whiskerRight ε F' ≫ F'.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₂)
⊢ F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 F'
have hγ : β ≫
    L₂.whiskerLeft
      (F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom) =
  β ≫ L₂.whiskerLeft (𝟙 F')
Tactic: apply F'.rightDerived_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
        (F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom) =
    β ≫ L₂.whiskerLeft (𝟙 F')
have hγ : ∀ (X₂ : C₂),
  (β ≫
          L₂.whiskerLeft
            (F'.leftUnitor.inv ≫
              F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom)).app
      X₂ =
    (β ≫ L₂.whiskerLeft (𝟙 F')).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
            (F'.leftUnitor.inv ≫
              F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom)).app
      X₂ =
    (β ≫ L₂.whiskerLeft (𝟙 F')).app X₂
have eq₁ : map (𝟭 D₁) (β.app X₂) ≫ η.app ((L₂ ⋙ F').obj X₂) = η.app ((F ⋙ L₁).obj X₂) ≫ (G' ⋙ F').map (β.app X₂)
Tactic: have eq₁ := η.naturality (β.app X₂)