awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x y : M
h :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((LinearMap.flip B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
                    B₁.toQuadraticMap :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have h₂ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
  (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
Tactic: rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x y : M
h :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((LinearMap.flip B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
                    B₁.toQuadraticMap :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have h₃ : HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
  HSMul.hSMul (α := Module.End R N) (β := N) 2 ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x y : M
h :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((LinearMap.flip B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₃ :
  HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
    HSMul.hSMul (α := Module.End R N) (β := N) 2 ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
                    B₁.toQuadraticMap :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have h₄ : HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
  HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₁ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₂ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 3 1) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 3 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₃ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1 + 1) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 3 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₃ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1 + 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₄ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1) ((Q : (a : M) → N) x : N) +
          HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 3 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₃ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1 + 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₄ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1) ((Q : (a : M) → N) x : N) +
            HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₅ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N) +
            HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N) +
          HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
⊢ ∃ (x : M), Ne.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
have rw : ¬∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
Tactic: rw [← not_forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
⊢ False
have apply : Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
  (0 : BilinMap R M N)
Tactic: apply hB₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
⊢ Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
have rw : Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) 0) 0
Tactic: rw [(QuadraticMap.ext h : Q = 0), map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
rw : Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) 0) 0
⊢ Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
have rw₁ : Eq (α := BilinMap R M N) 0 0
Tactic: rw [(QuadraticMap.ext h : Q = 0), map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
f g : M →ₗ[R] R
⊢ ((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      (linMulLin f g) =
    HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f)
have h : ∀ (x x_1 : M),
  Eq.{u_3 + 1} (α := R)
    (((((((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    (linMulLin f g) :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
    ((((HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
                  (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
Tactic: ext