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 : MonoidalRightAction.{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 _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d')) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      d')
    (Iso.hom (ρᵣ d) ≫ f) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))
have rw₄ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    d')
  (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
  (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
⊢ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
⊢ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
⊢ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
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]
-- 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw : (inv f ≫ f) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
Tactic: rw [← comp_actionHomLeft, IsIso.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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
rw : (inv f ≫ f) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ 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, IsIso.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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
rw : (inv f ≫ f) ⊵ᵣ 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)
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ 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, IsIso.inv_hom_id, id_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
⊢ Eq (α :=
    Quiver.Hom (V := (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (Functor.obj (curriedActionMop C D) x)
      (tensorObj (𝒞 := monoidalOppositeCategory)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
        (Functor.obj (curriedActionMop C D) x)))
    (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
      (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj (curriedActionMop C D) x))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
        (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x)))
have h : Eq (α :=
  Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
    (unmop
      (tensorObj (𝒞 := monoidalOppositeCategory)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
        (Functor.obj (curriedActionMop C D) x))))
  (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x))))
  (Quiver.Hom.unmop
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
      (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj (curriedActionMop C D) x))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := sorry })
        (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
Tactic: apply MonoidalOpposite.hom_ext