awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ))
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
have h₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (fst R R))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
    (fst R R))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (fst R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (fst R R))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ))
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
have h₂ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (snd R R))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
    (snd R R))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (fst R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (fst R R))
have h₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (fst R R ▷ R ≫ μ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
Tactic: simp only [lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (fst R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
have h₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
  (fst R R ▷ R) (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (snd R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (snd R R))
have h₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (snd R R ▷ R ≫ μ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
Tactic: simp only [lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (snd R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
have h₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
  (snd R R ▷ R) (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X : C
a b c : X ⟶ R
⊢ a * (b + c) = a * b + a * c
have revert : ∀ {X : C} (a b c : X ⟶ R), a * (b + c) = a * b + a * c
Tactic: revert X a b c
Cleared hypotheses: X, a, b, c
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
⊢ ∀ {X : C} (a b c : X ⟶ R), a * (b + c) = a * b + a * c
have rw : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) R (tensorObj.{v, u} (𝒞 := inst) R R) ⟶ R) (R ◁ σ ≫ μ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
Tactic: rw [← mul_add_iff, RingObj.mul_add R]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) R (tensorObj.{v, u} (𝒞 := inst) R R) ⟶ R) (R ◁ σ ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
⊢ ∀ {X : C} (a b c : X ⟶ R), a * (b + c) = a * b + a * c
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) R (tensorObj.{v, u} (𝒞 := inst) R R) ⟶ R)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
Tactic: rw [← mul_add_iff, RingObj.mul_add R]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X : C
a b c : X ⟶ R
⊢ (a + b) * c = a * c + b * c
have revert : ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c
Tactic: revert X a b c
Cleared hypotheses: X, a, b, c
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
⊢ ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c
have rw : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
Tactic: rw [← add_mul_iff, RingObj.add_mul R]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
⊢ ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
Tactic: rw [← add_mul_iff, RingObj.add_mul R]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y₁ Y₂))
    (F.map (f ⊗ₘ g)) (F.map (f ▷ X₂ ≫ Y₁ ◁ g))
have rw : (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
  ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫
    (fData.μIso Y₁ X₂).inv ≫ F.obj Y₁ ◁ F.map g ≫ (fData.μIso Y₁ Y₂).hom
Tactic: rw [fData.tensorHom_eq, Functor.map_comp, fData.whiskerRight_eq, fData.whiskerLeft_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ X₂ : D
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂))
have mk : ∀
  (μIso :
    (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
  (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
    (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
      (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
          F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
        ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
          (∀ (X Y Z : D),
              F.map (Iso.hom (α_ X Y Z)) =
                ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                      ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                    α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                      (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
            (∀ (X : D),
                F.map (Iso.hom (λ_ X)) =
                  ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                      λ_ (F.obj X)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (ρ_ X)) =
                    ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                        ρ_ (F.obj X)).hom) →
                F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂))
Tactic: cases fData
Cleared hypotheses: fData
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Z₁ Z₂))
    (F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
have mk : ∀
  (μIso :
    (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
  (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
    (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
      (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
          F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
        ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
          (∀ (X Y Z : D),
              F.map (Iso.hom (α_ X Y Z)) =
                ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                      ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                    α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                      (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
            (∀ (X : D),
                F.map (Iso.hom (λ_ X)) =
                  ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                      λ_ (F.obj X)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (ρ_ X)) =
                    ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                        ρ_ (F.obj X)).hom) →
                Eq (α :=
                  F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Z₁ Z₂))
                  (F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
Tactic: cases fData
Cleared hypotheses: fData
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ F.map (Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z)) =
    F.map
      (Iso.hom (α_ (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y Z) ≫
        Iso.hom (α_ W X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have simp : Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
    (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj W) (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj W) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
          F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫
            F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z ≫
              F.obj W ◁ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom ≫
                  F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                    Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) =
  Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
    Iso.hom (α_ (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X)) (F.obj Y) (F.obj Z)) ≫
      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) ◁ (fData.μIso Y Z).hom ≫
        (fData.μIso W X).inv ▷ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z) ≫
          Iso.hom (α_ (F.obj W) (F.obj X) (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
            F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
Tactic: simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc,
      Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom,
      comp_whiskerRight, whisker_assoc, assoc, fData.whiskerLeft_eq, whiskerLeft_comp,
      Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc, hom_inv_whiskerRight_assoc,
      Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
| F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫ F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z
have a : F.obj W ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z))
Tactic: rw [← whiskerLeft_comp, hom_inv_whiskerRight]