awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map
        (β.app (G₁.obj (R₁.obj b)) ≫
          (L₂ ⋙ H₂).map
            ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
              R₂.map (H₁.map (adj₁.counit.app b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Tactic: slice_rhs 2 4 =>
    rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp]
    rw [← Functor.comp_map G₂ L₃, β.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map
          (β.app (G₁.obj (R₁.obj b)) ≫
            (L₂ ⋙ H₂).map
              ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
                R₂.map (H₁.map (adj₁.counit.app b)))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
          R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Tactic: rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
| R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
have a : R₃.map (H₂.map ((R₂ ⋙ L₂).map (H₁.map (adj₁.counit.app b)) ≫ adj₂.counit.app (H₁.obj b)))
Tactic: rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
| R₃.map (H₂.map ((R₂ ⋙ L₂).map (H₁.map (adj₁.counit.app b)) ≫ adj₂.counit.app (H₁.obj b)))
have a : R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ map (𝟭 D) (H₁.map (adj₁.counit.app b))))
Tactic: rw [adj₂.counit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
| R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
have a : R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ map (𝟭 D) (H₁.map (adj₁.counit.app b))))
Tactic: rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
    rw [adj₂.counit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
      R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ map (𝟭 D) (H₁.map (adj₁.counit.app b))))
Tactic: slice_rhs 4 5 =>
    rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
    rw [adj₂.counit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
          R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ map (𝟭 D) (H₁.map (adj₁.counit.app b))))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
        R₃.map (H₂.map (L₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
          R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
Tactic: simp only [comp_obj, Functor.comp_map, map_comp, id_obj, Functor.id_map, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
| R₃.map (H₂.map (L₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
    R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b)))))
have a : R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))) ≫ map (𝟭 D) (α.natTrans.app (R₁.obj b))))
Tactic: rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (L₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))))) ≫
              R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))) ≫ map (𝟭 D) (α.natTrans.app (R₁.obj b)))) ≫
          R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
Tactic: slice_rhs 4 5 =>
    rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))) ≫ map (𝟭 D) (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
Tactic: simp only [comp_obj, id_obj, Functor.id_map, map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
| R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
    R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b)))))
have a : R₃.map (H₂.map (𝟙 (L₂.obj (G₁.obj (R₁.obj b)))))
Tactic: rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))))) ≫
            R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
have h : adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
      R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
  adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
    R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
      (R₃.map (H₂.map (𝟙 (L₂.obj (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (α.natTrans.app (R₁.obj b)))) ≫
        R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
Tactic: slice_rhs 3 4 =>
    rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
| R₂.map (α.natTrans.app (R₁.obj (R₃.obj c))) ≫
    R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (H.obj (R₃.obj c)))
have a : R₂.map
  (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
    R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c)))))
Tactic: rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (R₃.obj c))) ≫
        R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫
          R₂.map (adj₄.unit.app (H.obj (R₃.obj c))) ≫
            R₂.map (R₄.map (β.natTrans.app (R₃.obj c))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))
have h : Eq (α := G.obj (R₁.obj (R₃.obj c)) ⟶ R₂.obj (R₄.obj (K.obj c)))
  (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
      R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))))
  (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    (R₂.map
          (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
            R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
        R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
      R₂.map (R₄.map (K.map (adj₃.counit.app c))))
Tactic: slice_rhs 2 4 =>
    rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]