awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx : Eq.{u_10 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P) (0 : P)
i : ι
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
have mpr : ∀
  (hx :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P))
  (i : ι), Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
Tactic: rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
Cleared hypotheses: hx, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx : Eq.{u_10 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P) (0 : P)
i : ι
mpr :
  ∀
    (hx :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) Finset.univ i →
          Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P))
    (i : ι), Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
have rw : ∀ (hx : Eq.{u_10 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0) (i j : ι),
  Membership.mem (γ := Finset ι) Finset.univ j → LE.le.{u_10} (α := P) (0 : P) ((Q j : (a : Mᵢ j) → P) (x j) : P)
Tactic: rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
Cleared hypotheses: hx, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (Mᵢ i)
inst_2 : AddCommGroup P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ Eq.{u_7 + 1} (α := P) (polar (⇑(pi (Mᵢ := Mᵢ) Q) : (a : (i : ι) → Mᵢ i) → P) x y)
    (∑ i : ι, polar (⇑(Q i) : (a : Mᵢ i) → P) (x i) (y i))
have dsimp : HSub.hSub (β := P)
    (HSub.hSub (α := P) (β := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (x + y) : P)
      ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P))
    ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) y : P) =
  ∑ i : ι,
    HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) ((Q i : (a : Mᵢ i) → P) (x i + y i) : P) ((Q i : (a : Mᵢ i) → P) (x i) : P))
      ((Q i : (a : Mᵢ i) → P) (y i) : P)
Tactic: dsimp [polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (Mᵢ i)
inst_2 : AddCommGroup P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (x + y) : P)
        ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P))
      ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) y : P) =
    ∑ i : ι,
      HSub.hSub (β := P)
        (HSub.hSub (α := P) (β := P) ((Q i : (a : Mᵢ i) → P) (x i + y i) : P) ((Q i : (a : Mᵢ i) → P) (x i) : P))
        ((Q i : (a : Mᵢ i) → P) (y i) : P)
have simp_rw : HSub.hSub (β := P)
    (HSub.hSub (α := P) (β := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (x + y) : P)
      ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P))
    ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) y : P) =
  HSub.hSub (α := P) (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1 + y x_1))
      (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1)) -
    ∑ x : ι, (Q x : (a : Mᵢ x) → P) (y x)
Tactic: simp_rw [Finset.sum_sub_distrib, pi_apply, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (Mᵢ i)
inst_2 : AddCommGroup P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
simp_rw :
  HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (x + y) : P)
        ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P))
      ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) y : P) =
    HSub.hSub (α := P) (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1 + y x_1))
        (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1)) -
      ∑ x : ι, (Q x : (a : Mᵢ x) → P) (y x)
⊢ HSub.hSub (β := P)
      (HSub.hSub (α := P) (β := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (x + y) : P)
        ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P))
      ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) y : P) =
    ∑ i : ι,
      HSub.hSub (β := P)
        (HSub.hSub (α := P) (β := P) ((Q i : (a : Mᵢ i) → P) (x i + y i) : P) ((Q i : (a : Mᵢ i) → P) (x i) : P))
        ((Q i : (a : Mᵢ i) → P) (y i) : P)
have simp_rw₁ : HSub.hSub (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) ((x + y) i)) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) -
    ∑ i : ι, (Q i : (a : Mᵢ i) → P) (y i) =
  HSub.hSub (α := P) (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1 + y x_1)) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) -
    ∑ i : ι, (Q i : (a : Mᵢ i) → P) (y i)
Tactic: simp_rw [Finset.sum_sub_distrib, pi_apply, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (Mᵢ i)
inst_2 : AddCommGroup P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
inst_6 : Invertible (α := R) 2
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
⊢ HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R ((i : ι) → Mᵢ i) P)
      (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      ((pi (Mᵢ := Mᵢ) Q).polarBilin (R := R) (M := (i : ι) → Mᵢ i) (N := P) : LinearMap.BilinMap R ((i : ι) → Mᵢ i) P) =
    ∑ i : ι,
      LinearMap.compl₁₂
        (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
          (Q i).polarBilin)
        (LinearMap.proj (φ := Mᵢ) i) (LinearMap.proj (φ := Mᵢ) i)
have rw : Eq (α := LinearMap.BilinMap R ((i : ι) → Mᵢ i) P)
  (∑ x : ι,
    HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R ((i : ι) → Mᵢ i) P)
      (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (LinearMap.compl₁₂ (Q x).polarBilin (LinearMap.proj (φ := Mᵢ) x) (LinearMap.proj (φ := Mᵢ) x)))
  (∑ i : ι,
    LinearMap.compl₁₂
      (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (Q i).polarBilin)
      (LinearMap.proj (φ := Mᵢ) i) (LinearMap.proj (φ := Mᵢ) i))
Tactic: rw [polarBilin_pi, Finset.smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y)
                Z).toModuleCat :
          Type u))
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)).toModuleCat :
          Type u)))
    (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))
    ((𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u))
            (ModuleCat.of R (↑Z.toModuleCat : Type u))) ≫
        (𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u))) ⊗ₘ
          𝟙 (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≫
      Iso.hom
          (α_ (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑Y.toModuleCat : Type u))
            (ModuleCat.of R (↑Z.toModuleCat : Type u))) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u))
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (ModuleCat.of R (↑Y.toModuleCat : Type u)) (ModuleCat.of R (↑Z.toModuleCat : Type u)))) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z).toModuleCat : Type u))))
have dsimp : Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
  (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
          Z.toModuleCat) ≫
      (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat)) ≫
    Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
Tactic: dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
⊢ Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
            Z.toModuleCat) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
          𝟙 Z.toModuleCat)) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
have rw : Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
  (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
      𝟙 Z.toModuleCat) ≫
    Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
Tactic: rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
rw :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
⊢ Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
            Z.toModuleCat) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
          𝟙 Z.toModuleCat)) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
have rw₁ : Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
  (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
      𝟙 Z.toModuleCat) ≫
    Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
      𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
Tactic: rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
rw :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
rw₁ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
⊢ Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
            Z.toModuleCat) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
          𝟙 Z.toModuleCat)) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
have rw₂ : Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
  (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
      𝟙 Z.toModuleCat) ≫
    Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)
Tactic: rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
rw :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
rw₁ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
rw₂ :
  Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
        𝟙 Z.toModuleCat) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)
⊢ Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
            Z.toModuleCat) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat) ⊗ₘ
          𝟙 Z.toModuleCat)) ≫
      Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) ≫
        𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) Y.toModuleCat Z.toModuleCat))
have rw₃ : Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat)
        Z.toModuleCat) ≫
    Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat)
Tactic: rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id,
          Category.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))
                X).toModuleCat :
          Type u))
      (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (ModuleCat.ofHom (Isometry.toLinearMap (Hom.toIsometry (Iso.hom (λ_ X)))))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (ModuleCat.of R (↑(toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) : Type u))
          (ModuleCat.of R (↑X.toModuleCat : Type u))) ≫
      𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ▷ ModuleCat.of R (↑X.toModuleCat : Type u) ≫
        Iso.hom (λ_ (ModuleCat.of R (↑X.toModuleCat : Type u))))
have dsimp : ModuleCat.ofHom
    (Isometry.toLinearMap (N := R) (Q₁ :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form) (Q₂ :=
      X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
    𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ▷ X.toModuleCat ≫ Iso.hom (λ_ X.toModuleCat)
Tactic: dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
      𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ▷ X.toModuleCat ≫ Iso.hom (λ_ X.toModuleCat)
have erw : ModuleCat.ofHom
    (Isometry.toLinearMap (N := R) (Q₁ :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form) (Q₂ :=
      X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
      Iso.hom (λ_ X.toModuleCat)
Tactic: erw [MonoidalCategory.id_whiskerRight]