awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
rw₇ : Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft
rw₈ : Q.actLeft = X.X ◁ 𝟙 Q.X ≫ Q.actLeft
rw₉ : Q.actLeft = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Q.X) ≫ Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₁₀ : Q.actLeft = Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₇ : Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
rw₇ : Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₈ : Q.actRight = 𝟙 Q.X ▷ Y.X ≫ Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
rw₇ : Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight
rw₈ : Q.actRight = 𝟙 Q.X ▷ Y.X ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₉ : Q.actRight = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X Y.X) ≫ Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
rw₇ : Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight
rw₈ : Q.actRight = 𝟙 Q.X ▷ Y.X ≫ Q.actRight
rw₉ : Q.actRight = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X Y.X) ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight
have rw₁₀ : Q.actRight = Q.actRight
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ : P.Hom Q } ≫
      { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 P
have h : Hom.hom
    ({ hom := f.hom, left_act_hom := sorry, right_act_hom := sorry : P.Hom Q } ≫
      { hom := f.inv, left_act_hom := sorry, right_act_hom := sorry }) =
  Hom.hom (𝟙 P)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Hom.hom
      ({ hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ : P.Hom Q } ≫
        { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 P)
have h : f.hom ≫ f.inv = 𝟙 P.X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ f.hom ≫ f.inv = 𝟙 P.X
have h : Eq.{v₁ + 1} (α := P.X ⟶ P.X) (𝟙 P.X) (𝟙 P.X)
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ : Q.Hom P } ≫
      { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 Q
have h : Hom.hom
    ({ hom := f.inv, left_act_hom := sorry, right_act_hom := sorry : Q.Hom P } ≫
      { hom := f.hom, left_act_hom := sorry, right_act_hom := sorry }) =
  Hom.hom (𝟙 Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Hom.hom
      ({ hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ : Q.Hom P } ≫
        { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 Q)
have h : f.inv ≫ f.hom = 𝟙 Q.X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ f.inv ≫ f.hom = 𝟙 Q.X
have h : Eq.{v₁ + 1} (α := Q.X ⟶ Q.X) (𝟙 Q.X) (𝟙 Q.X)
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶ X P Q)
    (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q)
    (Iso.inv (α_ R.X P.X Q.X) ≫
      P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
have erw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶ X P Q)
  ((Iso.inv (α_ R.X P.X Q.X) ≫ P.actLeft ▷ Q.X) ≫
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.inv (α_ R.X P.X Q.X) ≫
    P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
Tactic: erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ η ▷ X P Q ≫ actLeft P Q = Iso.hom (λ_ (X P Q))
have refine : Eq (α :=
  Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
    X P Q)
  (CategoryTheory.Functor.map (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
    η ▷ X P Q ≫ actLeft P Q)
  (CategoryTheory.Functor.map (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
    Iso.hom (λ_ (X P Q)))
Tactic: refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      X P Q)
    (CategoryTheory.Functor.map (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      η ▷ X P Q ≫ actLeft P Q)
    (CategoryTheory.Functor.map (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      Iso.hom (λ_ (X P Q)))
have dsimp : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    η ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
  tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
Tactic: dsimp [X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    η ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
have a : η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
  R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      η ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have slice_lhs : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
    (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
        R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X
          (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
    (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) =
  tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
Tactic: slice_lhs 1 2 => rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) :
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
have a : Iso.inv (α_ R.X P.X Q.X) ≫
  P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [whiskerLeft_π_actLeft]