awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      X.toModuleCat ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫ Iso.hom (ρ_ X.toModuleCat)
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).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 (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑(toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) : Type u))) ≫
      ModuleCat.of R (↑X.toModuleCat : Type u) ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫
        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) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
        Iso.hom (ρ_ X.toModuleCat)
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      X.toModuleCat ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫ Iso.hom (ρ_ X.toModuleCat)

Tactic:
erw [MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_id
-- 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) X.toModuleCat
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) ⟶
      X.toModuleCat)
    (ModuleCat.ofHom
        (Isometry.toLinearMap (N := R) (Q₁ :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form)
          (Q₂ := X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) :
      Quiver.Hom (V := ModuleCat R)
        (ModuleCat.of R
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
                (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) :
            Type u))
        (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (Iso.hom (ρ_ X.toModuleCat) :
      MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ⟶
        X.toModuleCat)
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
        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) X.toModuleCat
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) ⟶
      X.toModuleCat)
    (ModuleCat.ofHom
        (Isometry.toLinearMap (N := R) (Q₁ :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form)
          (Q₂ := X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) :
      Quiver.Hom (V := ModuleCat R)
        (ModuleCat.of R
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
                (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) :
            Type u))
        (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (Iso.hom (ρ_ X.toModuleCat) :
      MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ⟶
        X.toModuleCat)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X : QuadraticModuleCat.{v, u} R
⊢ ModuleCat.of R (↑X.toModuleCat : Type v) = X.toModuleCat

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
V W : QuadraticModuleCat.{v, u} R
x x_1 : V.Hom W
f g : V.form →qᵢ W.form
h : { toIsometry' := f : V.Hom W }.toIsometry = { toIsometry' := g }.toIsometry
⊢ { toIsometry' := f : V.Hom W } = { toIsometry' := g }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
M N : QuadraticModuleCat.{v, u} R
f g : M ⟶ N
h : Hom.toIsometry f = Hom.toIsometry g
⊢ f = g

Tactic:
Hom.ext h

Premises used: QuadraticModuleCat.Hom.ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
M N U : QuadraticModuleCat.{v, u} R
f : M ⟶ N
g : N ⟶ U
⊢ Hom.toIsometry (f ≫ g) = (Hom.toIsometry g).comp (Hom.toIsometry f)

Tactic:
rfl

Premises used: QuadraticMap.Isometry.comp, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
M : QuadraticModuleCat.{v, u} R
⊢ Hom.toIsometry (𝟙 M) = Isometry.id M.form

Tactic:
rfl

Premises used: QuadraticMap.Isometry.id, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X : QuadraticModuleCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (QuadraticModuleCat.{u_1, u} R) (FC := fun (V W : QuadraticModuleCat.{u_1, u} R) ↦ V.form →qᵢ W.form)
        (CC := fun (X : QuadraticModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD :=
        fun (x1 x2 : ModuleCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
      X =
    ModuleCat.of R (↑X.toModuleCat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y : QuadraticModuleCat.{u_1, u} R
f : X ⟶ Y
⊢ CategoryTheory.Functor.map
      (forget₂ (QuadraticModuleCat.{u_1, u} R) (FC := fun (V W : QuadraticModuleCat.{u_1, u} R) ↦ V.form →qᵢ W.form)
        (CC := fun (X : QuadraticModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD :=
        fun (x1 x2 : ModuleCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
      f =
    ModuleCat.ofHom (Hom.toIsometry f).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
Q₁ : QuadraticForm R X
⊢ ofIso (IsometryEquiv.refl Q₁) = Iso.refl (of Q₁)

Tactic:
rfl

Premises used: QuadraticModuleCat.ofIso, QuadraticMap.IsometryEquiv.toIsometry, CategoryTheory.Iso.refl, QuadraticMap.Isometry.id, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : AddCommGroup Y
inst_4 : Module R Y
Q₁ : QuadraticForm R X
Q₂ : QuadraticForm R Y
e : IsometryEquiv Q₁ Q₂
⊢ ofIso e.symm = (ofIso e).symm

Tactic:
rfl

Premises used: QuadraticModuleCat.ofIso, LinearEquiv.symm, QuadraticMap.IsometryEquiv.symm, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : AddCommGroup Y
inst_4 : Module R Y
inst_5 : AddCommGroup Z
inst_6 : Module R Z
Q₁ : QuadraticForm R X
Q₂ : QuadraticForm R Y
Q₃ : QuadraticForm R Z
e : IsometryEquiv Q₁ Q₂
f : IsometryEquiv Q₂ Q₃
⊢ ofIso (e.trans f) = ofIso e ≪≫ ofIso f

Tactic:
rfl

Premises used: QuadraticModuleCat.ofIso, QuadraticMap.Isometry.comp, QuadraticMap.IsometryEquiv.toIsometry, CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑X.toModuleCat : Type v)
change :
  (QuadraticModuleCat.Hom.toIsometry (i.hom ≫ i.inv) : (a : (↑X.toModuleCat : Type v)) → (↑X.toModuleCat : Type v)) x =
    x
⊢ (QuadraticModuleCat.Hom.toIsometry i.inv : (a : (↑Y.toModuleCat : Type v)) → (↑X.toModuleCat : Type v))
      ((QuadraticModuleCat.Hom.toIsometry i.hom : (a : (↑X.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v)) x :
        (↑Y.toModuleCat : Type v)) =
    x

Tactic:
change (i.hom ≫ i.inv).toIsometry x = x

Premises used: CategoryTheory.CategoryStruct.comp, QuadraticModuleCat.Hom.toIsometry, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑X.toModuleCat : Type v)
⊢ (QuadraticModuleCat.Hom.toIsometry (i.hom ≫ i.inv) : (a : (↑X.toModuleCat : Type v)) → (↑X.toModuleCat : Type v)) x =
    x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑Y.toModuleCat : Type v)
change :
  (QuadraticModuleCat.Hom.toIsometry (i.inv ≫ i.hom) : (a : (↑Y.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v)) x =
    x
⊢ (QuadraticModuleCat.Hom.toIsometry i.hom : (a : (↑X.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v))
      ((QuadraticModuleCat.Hom.toIsometry i.inv : (a : (↑Y.toModuleCat : Type v)) → (↑X.toModuleCat : Type v)) x :
        (↑X.toModuleCat : Type v)) =
    x

Tactic:
change (i.inv ≫ i.hom).toIsometry x = x

Premises used: CategoryTheory.CategoryStruct.comp, QuadraticModuleCat.Hom.toIsometry, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑Y.toModuleCat : Type v)
⊢ (QuadraticModuleCat.Hom.toIsometry (i.inv ≫ i.hom) : (a : (↑Y.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v)) x =
    x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X : QuadraticModuleCat.{v, u} R
⊢ toIsometryEquiv (refl X) = QuadraticMap.IsometryEquiv.refl X.form

Tactic:
rfl

Premises used: CategoryTheory.Iso.toIsometryEquiv, QuadraticMap.IsometryEquiv.refl, LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y : QuadraticModuleCat.{v, u} R
e : X ≅ Y
⊢ e.symm.toIsometryEquiv = e.toIsometryEquiv.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, QuadraticMap.IsometryEquiv.symm, CategoryTheory.Iso.toIsometryEquiv, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
e : X ≅ Y
f : Y ≅ Z
⊢ (e ≪≫ f).toIsometryEquiv = e.toIsometryEquiv.trans f.toIsometryEquiv

Tactic:
rfl

Premises used: CategoryTheory.Iso.toIsometryEquiv, LinearEquiv.trans, QuadraticMap.IsometryEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
⊢ Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) (x + y) : M →ₗ[R] P) (0 : M →ₗ[R] P)

Tactic:
simp [hx.2, hy.2]

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
refine : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
⊢ Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    (x + y)

Tactic:
refine ⟨?_, by simp [hx.2, hy.2]⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
⊢ Eq.{u_4 + 1} (α := P) ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x))
    ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) 0)

Tactic:
have := congr_arg (· y) hx.2
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this :
  Eq.{u_4 + 1} (α := P) ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x))
    ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) 0)
⊢ (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)

Tactic:
simp only [QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar,
      LinearMap.zero_apply, sub_sub, sub_eq_zero] at this

Premises used: LinearMap.zero_apply, sub_eq_zero, QuadraticMap.polar, sub_sub, QuadraticMap.polarBilin_apply_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P) = 0
rw₁ : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q : (a : M) → P) y : P) = 0
rw₂ : HAdd.hAdd (α := P) 0 0 = 0
rw₃ rw₄ : Eq.{u_4 + 1} (α := P) 0 0
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)

Tactic:
rw [this, hx.1, hy.1, zero_add]

Premises used: zero_add, And.left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
⊢ Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
a : R
x : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
⊢ Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    (a • x)

Tactic:
simp [QuadraticMap.map_smul, hx.1, hx.2]

Premises used: QuadraticMap.map_smul, And.right, And.left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
m : M
⊢ m ∈ Q.radical ↔
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P) ∧
      ∀ (n : M), Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (m + n) : P) ((Q : (a : M) → P) n : P)

Tactic:
simp +contextual [radical, QuadraticMap.polarBilin, LinearMap.ext_iff,
    QuadraticMap.polar, sub_sub, sub_eq_zero]

Premises used: sub_eq_zero, LinearMap.ext_iff, QuadraticMap.polar, QuadraticMap.radical, sub_sub, QuadraticMap.polarBilin
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
h : ∀ (x : M'), x ∈ Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical ↔ x ∈ Q'.radical
⊢ Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical = Q'.radical

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
x : M'
⊢ x ∈ Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical ↔ x ∈ Q'.radical

Tactic:
simp [mem_radical_iff', ← e.map_app, -map_app, e.toEquiv.forall_congr_left]

Premises used: Equiv.forall_congr_left, QuadraticMap.IsometryEquiv.map_app, LinearEquiv.toEquiv, QuadraticMap.IsometryEquiv.toLinearEquiv, QuadraticMap.mem_radical_iff'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
h : Q.Equivalent Q'
obtain : ∀ (e : Q.IsometryEquiv Q'), Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical
⊢ Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical

Tactic:
obtain ⟨e⟩ := h
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
rw :
  Module.finrank.{u_1, u_2} R ↥Q.radical =
    Module.finrank.{u_1, u_3} R ↥(Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical)
rw₁ rw₂ : Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_2} R ↥Q.radical
⊢ Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical

Tactic:
rw [← e.map_radical, LinearEquiv.finrank_map_eq]

Premises used: QuadraticMap.IsometryEquiv.map_radical, LinearEquiv.finrank_map_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : (N.quotientRel : M → M → Prop) m m'
⊢ m - m' ∈ N

Tactic:
rw [Submodule.quotientRel_def] at hmm'

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ m = m' + (m - m')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
rw :
  HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m' : P)
      ((((Q.polarBilin : (a : M) → M →ₗ[R] P) (m - m') : M →ₗ[R] P) : (a : M) → P) m' : P) =
    (Q : (a : M) → P) m'
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m' : P)

Tactic:
rw [(by simp : m = m' + (m - m')), QuadraticMap.map_add Q m' (m - m'),
    (hN hmm').1, add_zero, polar_comm, ← polarBilin_apply_apply]

Premises used: HSub.hSub, QuadraticMap.polar_comm, QuadraticMap.map_add, And.left, add_zero, DFunLike.coe, QuadraticMap.polarBilin_apply_apply