awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : KleisliCat m
f : X ⟶ Y
g : Y ⟶ Z
⊢ { of := ↾(f ≫ g) : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } } =
    { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫ { of := ↾g }
have h : ∀ (x : { of := X : Kleisli (ofTypeMonad m) }.of),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          { of := ↾(f ≫ g) : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } }.of).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Kleisli.Hom.of
          ({ of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫
            { of := ↾g : { of := Y : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } })))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : KleisliCat m
f : X ⟶ Y
g : Y ⟶ Z
x : { of := X : Kleisli (ofTypeMonad m) }.of
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          { of := ↾(f ≫ g) : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } }.of).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Kleisli.Hom.of
          ({ of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫
            { of := ↾g : { of := Y : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } })))
      x
have h : (f ≫ g) x = do
  let a ← f x
  g a
Tactic: simp [joinM]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α := X.of ⟶ Z.of)
    (fun (x : X.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g).of :
          (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Z.of))
        x)
    (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
            (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
          x)
      fun (x : Y.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) g.of :
          (a : (fun (X : Type u) ↦ X) Y.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Z.of))
        x)
have dsimp : Eq.{u + 1} (α := X.of ⟶ Z.of)
  (fun (x : X.of) ↦
    joinM
      (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)))
  (CategoryStruct.comp (Y := Y.of)
    (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x) fun (x : Y.of) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α := X.of ⟶ Z.of)
    (fun (x : X.of) ↦
      joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)))
    (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x) fun (x : Y.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x)
have h : ∀ (t : X.of),
  Eq (α := m Z.of)
    (joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t)) :
      m Z.of)
    (CategoryStruct.comp (Y := Y.of)
        (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
        (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
      m Z.of)
Tactic: ext t
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
t : X.of
⊢ Eq (α := m Z.of)
    (joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t)) :
      m Z.of)
    (CategoryStruct.comp (Y := Y.of)
        (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
        (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
      m Z.of)
have h : Eq.{u + 1} (α := m Z.of)
  (do
    let a ← (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t
    (TypeCat.Hom.hom g.of : (a : Y.of) → m Z.of) a : m Z.of)
  (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
      (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
    m Z.of)
Tactic: simp [joinM]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
⊢ Iso (C := KleisliCat m ⥤ KleisliCat m) (𝟭 (KleisliCat m))
    (Functor.comp (D := Kleisli (ofTypeMonad m))
      { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
        map_id := ⋯, map_comp := ⋯ }
      { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
        map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
              (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
            x,
        map_id := ⋯, map_comp := ⋯ })
have refine : ∀ {X Y : KleisliCat m} (f : X ⟶ Y),
  Eq (α :=
    Functor.obj (𝟭 (KleisliCat m)) X ⟶
      Functor.obj
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
            map_id := sorry, map_comp := sorry }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := sorry, map_comp := sorry })
        Y)
    (Functor.map (𝟭 (KleisliCat m)) f ≫ Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) Y))
    (Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) X) ≫
      Functor.map
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X : Kleisli (ofTypeMonad m) },
            map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦
              { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } },
            map_id := sorry, map_comp := sorry : KleisliCat m ⥤ Kleisli (ofTypeMonad m) }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := sorry, map_comp := sorry : Kleisli (ofTypeMonad m) ⥤ KleisliCat m })
        f)
Tactic: refine NatIso.ofComponents (fun X => Iso.refl X) fun f => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (𝟭 (KleisliCat m)) X ⟶
      Functor.obj
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
            map_id := ⋯, map_comp := ⋯ }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := ⋯, map_comp := ⋯ })
        Y)
    (Functor.map (𝟭 (KleisliCat m)) f ≫ Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) Y))
    (Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) X) ≫
      Functor.map
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X : Kleisli (ofTypeMonad m) },
            map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦
              { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } },
            map_id := ⋯, map_comp := ⋯ : KleisliCat m ⥤ Kleisli (ofTypeMonad m) }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := ⋯, map_comp := ⋯ : Kleisli (ofTypeMonad m) ⥤ KleisliCat m })
        f)
have change : f >=> pure = pure >=> f
Tactic: change f >=> pure = pure >=> f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        y)
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ x) ≫ f ≫ Iso.inv (λₗ y))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) y)
  (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
  ((tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ y)) ≫ Iso.inv (λₗ y))
Tactic: rw [← Category.assoc, actionUnitIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
z z' : D
f : z ⟶ z'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (tensorObj.{v_1, u_1} (𝒞 := inst) x y ⊴ₗ f) (Iso.hom (αₗ x y z) ≫ x ⊴ₗ y ⊴ₗ f ≫ Iso.inv (αₗ x y z'))
have simp : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y) z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
      z')
  (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f) (Iso.hom (αₗ x y z) ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f) ≫ Iso.inv (αₗ x y z'))
Tactic: simp only [← id_actionHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
z z' : D
f : z ⟶ z'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f) (Iso.hom (αₗ x y z) ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f) ≫ Iso.inv (αₗ x y z'))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y) z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
      z')
  (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f) ((((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ Iso.hom (αₗ x y z')) ≫ Iso.inv (αₗ x y z'))
Tactic: rw [← Category.assoc, ← actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
  (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h))
have rw₁ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
  (f ⊙ₗₘ g ⊙ₗₘ h) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h))
have rw₂ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
  (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (f ⊙ₗₘ g ⊙ₗₘ h)
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (f ⊙ₗₘ g ⊙ₗₘ h)
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h))
have rw₃ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)
      d₁ ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
  (((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (f ⊙ₗₘ g ⊙ₗₘ h)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)
        d₁ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h))
have rw₄ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)
      d₁ ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
  (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h)) (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]