awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0
i j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
⊢ LE.le.{u_10} (α := P) (0 : P) ((Q j : (a : Mᵢ j) → P) (x j) : P)

Tactic:
exact (h j).1 _

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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)
⊢ 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))

Tactic:
dsimp [polar]

Premises used: QuadraticMap.polar
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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)
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)
⊢ 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:
simp_rw [Finset.sum_sub_distrib, pi_apply, Pi.add_apply]

Premises used: Pi.add_apply, Finset.sum_sub_distrib, QuadraticMap.pi_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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) (∑ i : ι, polar (⇑(Q i) : (a : Mᵢ i) → P) (x i) (y i) : P)
    ((((∑ i : ι, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj (φ := Mᵢ) i) (LinearMap.proj (φ := Mᵢ) i) :
                (a : (i : ι) → Mᵢ i) → ((i : ι) → Mᵢ i) →ₗ[R] P)
              x :
            ((i : ι) → Mᵢ i) →ₗ[R] P) :
          (a : (i : ι) → Mᵢ i) → P)
        y :
      P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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))
⊢ 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)

Tactic:
rw [polarBilin_pi, Finset.smul_sum]

Premises used: QuadraticMap.Ring.polarBilin_pi, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
⊢ 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:
rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
K L M N : QuadraticModuleCat R
f : K ⟶ L
g : M ⟶ N
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) K M).form →qᵢ
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) L N).form)
    (Hom.toIsometry (f ⊗ₘ g)) ((Hom.toIsometry f).tmul (Hom.toIsometry g))

Tactic:
rfl

Premises used: QuadraticMap.Isometry.tmul, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
L M N : QuadraticModuleCat R
f : M ⟶ N
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) L M).form →qᵢ
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) L N).form)
    (Hom.toIsometry (L ◁ f)) ((Isometry.id L.form).tmul (Hom.toIsometry f))

Tactic:
rfl

Premises used: QuadraticMap.Isometry.tmul, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
L M : QuadraticModuleCat R
f : L ⟶ M
N : QuadraticModuleCat R
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) L N).form →qᵢ
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) M N).form)
    (Hom.toIsometry (f ▷ N)) ((Hom.toIsometry f).tmul (Isometry.id N.form))

Tactic:
rfl

Premises used: QuadraticMap.Isometry.tmul, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M : QuadraticModuleCat R
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) M).form →qᵢ M.form)
    (Hom.toIsometry (Iso.hom (λ_ M))) (IsometryEquiv.toIsometry M.form.tensorLId)

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M : QuadraticModuleCat R
⊢ Eq (α :=
    M.form →qᵢ (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) M).form)
    (Hom.toIsometry (Iso.inv (λ_ M))) (IsometryEquiv.toIsometry (IsometryEquiv.symm M.form.tensorLId))

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M : QuadraticModuleCat R
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) M ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form →qᵢ M.form)
    (Hom.toIsometry (Iso.hom (ρ_ M))) (IsometryEquiv.toIsometry M.form.tensorRId)

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M : QuadraticModuleCat R
⊢ Eq (α :=
    M.form →qᵢ (MonoidalCategoryStruct.tensorObj (𝒞 := category) M ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form)
    (Hom.toIsometry (Iso.inv (ρ_ M))) (IsometryEquiv.toIsometry (IsometryEquiv.symm M.form.tensorRId))

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M N K : QuadraticModuleCat R
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) M N) K).form →qᵢ
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) M (MonoidalCategoryStruct.tensorObj (𝒞 := category) N K)).form)
    (Hom.toIsometry (Iso.hom (α_ M N K))) (IsometryEquiv.toIsometry (M.form.tensorAssoc N.form K.form))

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
M N K : QuadraticModuleCat R
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) M (MonoidalCategoryStruct.tensorObj (𝒞 := category) N K)).form →qᵢ
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) M N) K).form)
    (Hom.toIsometry (Iso.inv (α_ M N K)))
    (IsometryEquiv.toIsometry (IsometryEquiv.symm (M.form.tensorAssoc N.form K.form)))

Tactic:
rfl

Premises used: QuadraticMap.IsometryEquiv.toIsometry, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y : QuadraticModuleCat R
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat =
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat Y.toModuleCat

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
⊢ Eq (α :=
    Functor.obj
        (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
          fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y) Z) ⟶
      Functor.obj
        (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
          fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)))
    (CategoryTheory.Functor.map
      (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
        fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Quotient, TensorProduct, AddCon.Quotient, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
⊢ Eq (α :=
    Functor.obj
        (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
          fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)) ⟶
      Functor.obj
        (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
          fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y) Z))
    (CategoryTheory.Functor.map
      (forget₂ (QuadraticModuleCat R) (FC := fun (V W : QuadraticModuleCat R) ↦ V.form →qᵢ W.form) (CC :=
        fun (X : QuadraticModuleCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (Iso.inv (α_ X Y Z)))
    (Iso.inv (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X Y Z : QuadraticModuleCat R
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))
⊢ 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))))

Tactic:
dsimp only [toModuleCat_tensor, ModuleCat.of_coe]

Premises used: ModuleCat.of_coe, QuadraticModuleCat.toModuleCat_tensor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
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)
⊢ 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))))

Tactic:
dsimp only [toModuleCat_tensor, ModuleCat.of_coe]

Premises used: ModuleCat.of_coe, QuadraticModuleCat.toModuleCat_tensor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
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)
⊢ 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:
erw [MonoidalCategory.id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
simp :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat ⟶
      X.toModuleCat)
    (ModuleCat.ofHom
        (Isometry.toLinearMap (N := R) (Q₁ :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form)
          (Q₂ := X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) :
      Quiver.Hom (V := ModuleCat R)
        (ModuleCat.of R
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) :
            Type u))
        (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (Iso.hom (λ_ X.toModuleCat) :
      MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) X.toModuleCat ⟶
        X.toModuleCat)
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat ⟶
      X.toModuleCat)
    (ModuleCat.ofHom
        (Isometry.toLinearMap (N := R) (Q₁ :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form)
          (Q₂ := X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) :
      Quiver.Hom (V := ModuleCat R)
        (ModuleCat.of R
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) :
            Type u))
        (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (Iso.hom (λ_ X.toModuleCat) :
      MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) X.toModuleCat ⟶
        X.toModuleCat)

Tactic:
rfl