awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ ∀ (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)
have h : ∀ (a a_1 : M),
  Quotient.lift (⇑Q : (a : M) → P) sorry (HAdd.hAdd (α := M ⧸ N) (Submodule.Quotient.mk a) (Submodule.Quotient.mk a_1)) =
    HAdd.hAdd (β := P)
      (Quotient.lift (⇑Q : (a : M) → P) sorry (Submodule.Quotient.mk a) +
        Quotient.lift (⇑Q : (a : M) → P) sorry (Submodule.Quotient.mk a_1))
      (((((LinearMap.liftQ₂ N N Q.polarBilin sorry sorry :
                    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: simp only [Submodule.Quotient.forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have w : Eq (α := M →ₗ[R] P) ((LinearMap.flip Q.polarBilin : (a : M) → M →ₗ[R] P) n : M →ₗ[R] P) (0 : M →ₗ[R] P)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have w₃ : ∀ (x : M), Eq.{u_4 + 1} (α := P) (polar (⇑Q : (a : M) → P) x n : P) ((0 : (a : M) → P) x : P)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have w₄ : ∀ (x : M), Eq.{u_4 + 1} (α := P) (polar (⇑Q : (a : M) → P) n x : P) ((0 : (a : M) → P) x : P)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
have w₆ : ∀ (x : M), True
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
have mp : N ≤ Q.radical → ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ N ≤ Q.radical ↔ ∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q
have mpr : (∃ (Q' : QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P), Q'.comp N.mkQ = Q) → N ≤ Q.radical
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Q.radical = LinearMap.ker Q.polarBilin
have h : ∀ (m : M), m ∈ Q.radical ↔ m ∈ LinearMap.ker Q.polarBilin
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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 ∈ Q.radical ↔ m ∈ LinearMap.ker Q.polarBilin
have 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
Tactic: simp only [mem_radical_iff', LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
have 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)
Tactic: refine ⟨by simp +contextual, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ 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)
have h₁ : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
Tactic: suffices Q m = 0 by grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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
Tactic: specialize h m
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have 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)
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
Cleared hypotheses: h