awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (f ≫ Iso.inv (λₗ d'))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d')
  (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, 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
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (f ≫ Iso.inv (λₗ d'))
have rw₁ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d')
  (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, 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
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (f ≫ Iso.inv (λₗ d'))
have rw₂ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d')
  ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d')) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, 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
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d')) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (f ≫ Iso.inv (λₗ d'))
have rw₃ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
    d')
  (Iso.hom (λₗ d) ≫ f) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, 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
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d')) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      d')
    (Iso.hom (λₗ d) ≫ f) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (f ≫ Iso.inv (λₗ d'))
have rw₄ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
    d')
  (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
  (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, 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 : C
y z : D
f : y ≅ z
⊢ x ⊴ₗ f.hom ≫ x ⊴ₗ f.inv = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw : x ⊴ₗ (f.hom ≫ f.inv) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
Tactic: rw [← actionHomRight_comp, Iso.hom_inv_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ≅ z
rw : x ⊴ₗ (f.hom ≫ f.inv) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
⊢ x ⊴ₗ f.hom ≫ x ⊴ₗ f.inv = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw₁ : x ⊴ₗ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
Tactic: rw [← actionHomRight_comp, Iso.hom_inv_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ≅ z
rw : x ⊴ₗ (f.hom ≫ f.inv) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₁ : x ⊴ₗ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
⊢ x ⊴ₗ f.hom ≫ x ⊴ₗ f.inv = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
Tactic: rw [← actionHomRight_comp, Iso.hom_inv_id, actionHomRight_id]
-- 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
f : x ≅ y
z : D
⊢ f.hom ⊵ₗ z ≫ f.inv ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw : (f.hom ≫ f.inv) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]
-- 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
f : x ≅ y
z : D
rw : (f.hom ≫ f.inv) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ f.hom ⊵ₗ z ≫ f.inv ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₁ : 𝟙 x ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]
-- 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
f : x ≅ y
z : D
rw : (f.hom ≫ f.inv) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : 𝟙 x ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ f.hom ⊵ₗ z ≫ f.inv ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
Tactic: rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]
-- 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 : C
y z : D
f : y ≅ z
⊢ x ⊴ₗ f.inv ≫ x ⊴ₗ f.hom = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw : x ⊴ₗ (f.inv ≫ f.hom) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← actionHomRight_comp, Iso.inv_hom_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ≅ z
rw : x ⊴ₗ (f.inv ≫ f.hom) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ x ⊴ₗ f.inv ≫ x ⊴ₗ f.hom = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₁ : x ⊴ₗ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← actionHomRight_comp, Iso.inv_hom_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ≅ z
rw : x ⊴ₗ (f.inv ≫ f.hom) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : x ⊴ₗ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ x ⊴ₗ f.inv ≫ x ⊴ₗ f.hom = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
Tactic: rw [← actionHomRight_comp, Iso.inv_hom_id, actionHomRight_id]
-- 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
f : x ≅ y
z : D
⊢ f.inv ⊵ₗ z ≫ f.hom ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw : (f.inv ≫ f.hom) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
Tactic: rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]
-- 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
f : x ≅ y
z : D
rw : (f.inv ≫ f.hom) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
⊢ f.inv ⊵ₗ z ≫ f.hom ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw₁ : 𝟙 y ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
Tactic: rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]
-- 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
f : x ≅ y
z : D
rw : (f.inv ≫ f.hom) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₁ : 𝟙 y ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
⊢ f.inv ⊵ₗ z ≫ f.hom ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
Tactic: rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
⊢ x ⊴ₗ f ≫ x ⊴ₗ inv f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw : x ⊴ₗ (f ≫ inv f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
Tactic: rw [← actionHomRight_comp, IsIso.hom_inv_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ₗ (f ≫ inv f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
⊢ x ⊴ₗ f ≫ x ⊴ₗ inv f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw₁ : x ⊴ₗ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
Tactic: rw [← actionHomRight_comp, IsIso.hom_inv_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ₗ (f ≫ inv f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₁ : x ⊴ₗ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
⊢ x ⊴ₗ f ≫ x ⊴ₗ inv f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
Tactic: rw [← actionHomRight_comp, IsIso.hom_inv_id, actionHomRight_id]
-- 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
f : x ⟶ y
inst_4 : IsIso f
z : D
⊢ f ⊵ₗ z ≫ inv f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw : (f ≫ inv f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]
-- 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
f : x ⟶ y
inst_4 : IsIso f
z : D
rw : (f ≫ inv f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ f ⊵ₗ z ≫ inv f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₁ : 𝟙 x ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]
-- 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
f : x ⟶ y
inst_4 : IsIso f
z : D
rw : (f ≫ inv f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : 𝟙 x ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ f ⊵ₗ z ≫ inv f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
Tactic: rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
⊢ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw : x ⊴ₗ (inv f ≫ f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ₗ (inv f ≫ f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₁ : x ⊴ₗ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
Tactic: rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]
-- 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 : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ₗ (inv f ≫ f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : x ⊴ₗ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
⊢ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
Tactic: rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]