awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₅ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ G.map (R₁.map (adj₁.counit.app X))) ≫ β.natTrans.app X = β.natTrans.app X
h₆ : G.map (adj₁.unit.app (R₁.obj X) ≫ R₁.map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₇ : G.map (𝟙 (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₅ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ G.map (R₁.map (adj₁.counit.app X))) ≫ β.natTrans.app X = β.natTrans.app X
h₆ : G.map (adj₁.unit.app (R₁.obj X) ≫ R₁.map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₇ : G.map (𝟙 (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₈ : 𝟙 (G.obj (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
β : TwoSquare R₁ H G R₂
X : D
h :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
h₁ :
  (G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X))) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₂ :
  G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ (H ⋙ R₂).map (adj₁.counit.app X) =
    β.natTrans.app X
h₃ : G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X) ≫ β.natTrans.app X = β.natTrans.app X
h₄ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₅ : (G.map (adj₁.unit.app (R₁.obj X)) ≫ G.map (R₁.map (adj₁.counit.app X))) ≫ β.natTrans.app X = β.natTrans.app X
h₆ : G.map (adj₁.unit.app (R₁.obj X) ≫ R₁.map (adj₁.counit.app X)) ≫ β.natTrans.app X = β.natTrans.app X
h₇ : G.map (𝟙 (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
h₈ : 𝟙 (G.obj (R₁.obj X)) ≫ β.natTrans.app X = β.natTrans.app X
⊢ G.map (adj₁.unit.app (R₁.obj X)) ≫ β.natTrans.app (L₁.obj (R₁.obj X)) ≫ R₂.map (H.map (adj₁.counit.app X)) =
    β.natTrans.app X
have h₉ : β.natTrans.app X = β.natTrans.app X
Tactic: rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare R₁ H G R₂
d : D
| L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d)
have rw : L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫ adj₂.counit.app (H.obj d)
Tactic: rw [← (mateEquiv adj₁ adj₂).right_inv α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d) =
    app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
      H.map (adj₁.counit.app d)
have conv_lhs : L₂.map ((Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app d) ≫ adj₂.counit.app (H.obj d) =
  app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α) (R₁.obj d) ≫
    H.map (adj₁.counit.app d)
Tactic: conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ G.map (adj₁.unit.app c) ≫ app ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α) (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫ R₂.map (α.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))
have simp : G.map (adj₁.unit.app c) ≫
    adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
  adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Tactic: simp only [id_obj, comp_obj, mateEquiv, Equiv.coe_fn_mk, comp_app, rightUnitor_inv_app,
    Functor.whiskerLeft_app, associator_hom_app, associator_inv_app, Functor.whiskerRight_app,
    Functor.comp_map, leftUnitor_hom_app, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ G.map (adj₁.unit.app c) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
have rw : adj₂.unit.app (G.obj c) ≫
    R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
  adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Tactic: rw [← adj₂.unit_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫ R₂.map (α.natTrans.app (R₁.obj (L₁.obj c)))
have a : R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c))
Tactic: rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
have slice_lhs : adj₂.unit.app (G.obj c) ≫
    R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
  adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Tactic: slice_lhs 2 3 =>
    rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
have rw : adj₂.unit.app (G.obj c) ≫
    (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
  adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Tactic: rw [R₂.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c)))
have a : R₂.map (H.map (𝟙 (L₁.obj c)))
Tactic: rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
have slice_lhs : adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) = adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
Tactic: slice_lhs 3 4 =>
    rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare R₁ H G R₂
c : C
| G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c)
have rw : G.map (adj₁.unit.app c) ≫ (Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app (L₁.obj c)
Tactic: rw [← (mateEquiv adj₁ adj₂).right_inv α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
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₂
α : TwoSquare R₁ H G R₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c) =
    adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
      R₂.map
        (app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α)
          (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))
have conv_lhs : G.map (adj₁.unit.app c) ≫ (Equiv.toFun (mateEquiv adj₁ adj₂) (Equiv.invFun (mateEquiv adj₁ adj₂) α)).app (L₁.obj c) =
  adj₂.unit.app (G.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
    R₂.map
      (app ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ H G R₂) → TwoSquare G L₁ L₂ H) α)
        (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))
Tactic: conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
-- 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
| G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫
    G₂.map (R₂.map (α.natTrans.app (R₁.obj b))) ≫
      G₂.map (R₂.map (H₁.map (adj₁.counit.app b))) ≫ adj₃.unit.app (G₂.obj (R₂.obj (H₁.obj b)))
have a : 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)))) ≫
        G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))
Tactic: rw [← assoc, ← 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 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))) =
    G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫
      G₂.map (R₂.map (α.natTrans.app (R₁.obj b))) ≫
        G₂.map (R₂.map (H₁.map (adj₁.counit.app b))) ≫
          adj₃.unit.app (G₂.obj (R₂.obj (H₁.obj 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
          (L₃.map
            ((G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
              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)))
Tactic: slice_rhs 1 4 => rw [← assoc, ← 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 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)))) ≫
                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 (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)))
Tactic: rw [L₃.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₃.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)))
have a : R₃.map
  (L₃.map
      (G₂.map
        ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
          R₂.map (H₁.map (adj₁.counit.app b)))) ≫
    β.natTrans.app (R₂.obj (H₁.obj b)))
Tactic: rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.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₃.map
        (G₂.map
          ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
            R₂.map (H₁.map (adj₁.counit.app b)))) ≫
      β.natTrans.app (R₂.obj (H₁.obj b)))
have a : 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))))
Tactic: 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
| 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)))
have a : 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))))
Tactic: rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp]
    rw [← Functor.comp_map G₂ L₃, β.naturality]