awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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'

Tactic:
simp [(hN hmm').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
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (a b : M), a ≈ b → Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) a : P) ((Q : (a : M) → P) b : P)

Tactic:
lift_aux hN

Premises used: _private.0.QuadraticMap.lift_aux
-- 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
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (a b : M), a ≈ b → Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) a : P) ((Q : (a : M) → P) b : P)

Tactic:
exact lift_aux hN

Premises used: _private.0.QuadraticMap.lift_aux
-- 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
N : Submodule R M
hN : N ≤ Q.radical
refine :
  ∃ (B : LinearMap.BilinMap.{u_1, u_2, u_4} R (M ⧸ N) P),
    ∀ (x y : M ⧸ N),
      Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
        HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
          ((((B : (a : M ⧸ N) → M ⧸ N →ₗ[R] P) x : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                (a : M ⧸ N) → P)
              y :
            P)
⊢ QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P

Tactic:
refine QuadraticMap.mk (Quotient.lift Q <| by exact lift_aux hN)
    (fun a m ↦ m.inductionOn (Q.map_smul a)) ?_
-- 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
N : Submodule R M
hN : N ≤ Q.radical
h :
  ∀ (x y : M ⧸ N),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
      HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  x :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            y :
          P)
w : ∀ (n : M) (hn : n ∈ N), n ∈ (LinearMap.flip Q.polarBilin).ker
⊢ ∃ (B : LinearMap.BilinMap.{u_1, u_2, u_4} R (M ⧸ N) P),
    ∀ (x y : M ⧸ N),
      Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
        HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
          ((((B : (a : M ⧸ N) → M ⧸ N →ₗ[R] P) x : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                (a : M ⧸ N) → P)
              y :
            P)

Tactic:
use Q.polarBilin.liftQ₂ N N (fun n hn ↦ (hN hn).2) (fun n hn ↦ ?_)

Premises used: And.right, LinearMap.liftQ₂, 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
N : Submodule R M
hN : N ≤ Q.radical
h :
  ∀ (a a_1 : M),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (HAdd.hAdd (α := M ⧸ N) (Submodule.Quotient.mk a) (Submodule.Quotient.mk a_1)) =
      HAdd.hAdd (β := P)
        (Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a) +
          Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a_1))
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  (Submodule.Quotient.mk a) :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            (Submodule.Quotient.mk a_1) :
          P)
⊢ ∀ (x y : M ⧸ N),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
      HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  x :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            y :
          P)

Tactic:
simp only [Submodule.Quotient.forall]

Premises used: Submodule.Quotient.forall
-- 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
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (a a_1 : M),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (HAdd.hAdd (α := M ⧸ N) (Submodule.Quotient.mk a) (Submodule.Quotient.mk a_1)) =
      HAdd.hAdd (β := P)
        (Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a) +
          Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a_1))
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  (Submodule.Quotient.mk a) :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            (Submodule.Quotient.mk a_1) :
          P)

Tactic:
QuadraticMap.map_add Q

Premises used: QuadraticMap.map_add, QuadraticMap.polar, DFunLike.coe
-- 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
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (a a_1 : M),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (HAdd.hAdd (α := M ⧸ N) (Submodule.Quotient.mk a) (Submodule.Quotient.mk a_1)) =
      HAdd.hAdd (β := P)
        (Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a) +
          Quotient.lift (⇑Q : (a : M) → P) ⋯ (Submodule.Quotient.mk a_1))
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  (Submodule.Quotient.mk a) :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            (Submodule.Quotient.mk a_1) :
          P)

Tactic:
exact QuadraticMap.map_add Q

Premises used: QuadraticMap.map_add, DFunLike.coe
-- 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
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
w : Eq (α := M →ₗ[R] P) ((LinearMap.flip Q.polarBilin : (a : M) → M →ₗ[R] P) n : M →ₗ[R] P) (0 : M →ₗ[R] P)
w₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := P) ((((LinearMap.flip Q.polarBilin : (a : M) → M →ₗ[R] P) n : M →ₗ[R] P) : (a : M) → P) x : P)
      ((0 : (a : M) → P) x : P)
w₂ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := P) ((((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) : (a : M) → P) n : P)
      ((0 : (a : M) → P) x : P)
w₃ : ∀ (x : M), Eq.{u_4 + 1} (α := P) (polar (⇑Q : (a : M) → P) x n : P) ((0 : (a : M) → P) x : P)
w₄ : ∀ (x : M), Eq.{u_4 + 1} (α := P) (polar (⇑Q : (a : M) → P) n x : P) ((0 : (a : M) → P) x : P)
w₅ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := P) ((((Q.polarBilin : (a : M) → M →ₗ[R] P) n : M →ₗ[R] P) : (a : M) → P) x : P)
      ((0 : (a : M) → P) x : P)
w₆ : ∀ (x : M), True
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker

Tactic:
simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply,
      polarBilin_apply_apply, polar_comm, ← polarBilin_apply_apply, (hN hn).2, forall_true_iff]

Premises used: QuadraticMap.polar_comm, LinearMap.ext_iff, LinearMap.flip_apply, LinearMap.mem_ker, And.right, forall_true_iff, QuadraticMap.polarBilin_apply_apply
-- 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
⊢ Eq.{u_4 + 1} (α := P) ((Q.lift N hN : (a : M ⧸ N) → P) (Submodule.Quotient.mk m) : P) ((Q : (a : M) → P) m : P)

Tactic:
rfl

Premises used: rfl
-- 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
mp : N ≤ Q.radical → ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q
mpr : (∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q) → N ≤ Q.radical
⊢ N ≤ Q.radical ↔ ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q

Tactic:
constructor
-- 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
⊢ N ≤ Q.radical → ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q

Tactic:
fun hN ↦ ⟨Q.lift N hN, rfl⟩

Premises used: QuadraticMap.lift, Exists.intro, rfl
-- 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
⊢ N ≤ Q.radical → ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q

Tactic:
exact fun hN ↦ ⟨Q.lift N hN, rfl⟩
-- 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
N : Submodule R M
Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P
m : M
hm : m ∈ N
⊢ m ∈ (Q'.comp N.mkQ).radical

Tactic:
simp [radical, (Submodule.Quotient.mk_eq_zero _).mpr hm, LinearMap.ext_iff, polar]

Premises used: Iff.mpr, LinearMap.ext_iff, QuadraticMap.polar, QuadraticMap.radical, Submodule.Quotient.mk_eq_zero
-- 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 → m ∈ LinearMap.ker Q.polarBilin

Tactic:
simp +contextual [mem_radical_iff', LinearMap.ext_iff, QuadraticMap.polar]

Premises used: LinearMap.ext_iff, QuadraticMap.polar, QuadraticMap.mem_radical_iff'
-- 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
inst_5 : Invertible (α := R) 2
h : ∀ (m : M), m ∈ Q.radical ↔ m ∈ LinearMap.ker Q.polarBilin
⊢ Q.radical = LinearMap.ker Q.polarBilin

Tactic:
ext m
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  (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)) ↔
    ∀ (x : M),
      HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) x : P) =
        0
⊢ m ∈ Q.radical ↔ m ∈ LinearMap.ker Q.polarBilin

Tactic:
simp only [mem_radical_iff', LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar]

Premises used: LinearMap.zero_apply, LinearMap.ext_iff, QuadraticMap.polar, LinearMap.mem_ker, QuadraticMap.mem_radical_iff', QuadraticMap.polarBilin_apply_apply
-- 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
inst_5 : Invertible (α := R) 2
m : M
⊢ (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)) →
    ∀ (x : M),
      HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) x : P) =
        0

Tactic:
simp +contextual
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  ∀
    (h :
      ∀ (x : M),
        HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) x : P) =
          0),
    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)
⊢ (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)) ↔
    ∀ (x : M),
      HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) x : P) =
        0

Tactic:
refine ⟨by simp +contextual, fun h ↦ ?_⟩
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  ∀ (x : M),
    HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
        ((Q : (a : M) → P) x : P) =
      0
this : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ 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:
grind
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  ∀ (x : M),
    HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
        ((Q : (a : M) → P) x : P) =
      0
h₁ : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ 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:
suffices Q m = 0 by grind
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  ∀ (x : M),
    HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + x) : P) ((Q : (a : M) → P) m : P))
        ((Q : (a : M) → P) x : P) =
      0
⊢ HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + m) : P) ((Q : (a : M) → P) m : P))
      ((Q : (a : M) → P) m : P) =
    0

Tactic:
specialize h m
-- 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
inst_5 : Invertible (α := R) 2
m : M
h :
  HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + m) : P) ((Q : (a : M) → P) m : P))
      ((Q : (a : M) → P) m : P) =
    0
h₁ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 m) : P)
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₂ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (β := P) (HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₃ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₄ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₅ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
            (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P)) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₆ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
          (HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P)) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₇ :
  ∀
    (h :
      HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₈ :
  ∀
    (h :
      HSub.hSub (β := P) (HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₉ h₁₀ h₁₁ h₁₂ :
  ∀ (h : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)

Tactic:
rwa [← two_smul R, QuadraticMap.map_smul, sub_sub, ← two_smul R, mul_smul, ← smul_sub,
    (isUnit_of_invertible 2).smul_eq_zero, two_smul, add_sub_cancel_right] at h

Premises used: isUnit_of_invertible, QuadraticMap.map_smul, two_smul, IsUnit.smul_eq_zero, sub_sub, smul_sub, add_sub_cancel_right, OfNat.ofNat, SemigroupAction.mul_smul
-- 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
inst_5 : Invertible (α := R) 2
rw :
  LinearMap.ker Q.polarBilin =
    LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
      ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)
⊢ Q.radical =
    LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
      ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)

Tactic:
rw [radical_eq_ker_polarBilin]

Premises used: QuadraticMap.radical_eq_ker_polarBilin
-- 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
inst_5 : Invertible (α := R) 2
h :
  ∀ (m : M),
    m ∈ LinearMap.ker Q.polarBilin ↔
      Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
          ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q))
        m
⊢ LinearMap.ker Q.polarBilin =
    LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
      ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)

Tactic:
ext m
-- 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
inst_5 : Invertible (α := R) 2
m : M
⊢ m ∈ LinearMap.ker Q.polarBilin ↔
    Membership.mem (γ := Submodule R M)
      (LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
        ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q))
      m

Tactic:
simp [LinearMap.ext_iff, QuadraticMap.polar, -smul_eq_mul, invOf_smul_eq_iff]

Premises used: LinearMap.ext_iff, QuadraticMap.polar, invOf_smul_eq_iff, smul_eq_mul
-- 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
inst_5 : Invertible (α := R) 2
⊢ Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q) ↔ Q.radical = ⊥

Tactic:
⟨Nondegenerate.radical_eq_bot, fun h ↦ ⟨h, ?_⟩⟩

Premises used: QuadraticMap.Nondegenerate.radical_eq_bot, QuadraticMap.Nondegenerate.mk, Iff.intro
-- 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
inst_5 : Invertible (α := R) 2
refine : ∀ (h : Q.radical = ⊥), Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1
⊢ Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q) ↔ Q.radical = ⊥

Tactic:
refine ⟨Nondegenerate.radical_eq_bot, fun h ↦ ⟨h, ?_⟩⟩
-- 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
inst_5 : Invertible (α := R) 2
h : Q.radical = ⊥
rw : Module.rank R ↥⊥ ≤ 1
⊢ Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1

Tactic:
rw [← QuadraticMap.radical_eq_ker_polarBilin, h]

Premises used: QuadraticMap.radical_eq_ker_polarBilin
-- 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
inst_5 : Invertible (α := R) 2
h : Q.radical = ⊥
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
inst_5 : Invertible (α := R) 2
h : Q.radical = ⊥
h_1 : Nontrivial R
⊢ Module.rank R ↥⊥ ≤ 1

Tactic:
simp only [rank_subsingleton', zero_le]

Premises used: zero_le, rank_subsingleton'