awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x x_1 : M
h :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
h₁ :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((f : (a : N) → N') ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N) : N')
⊢ Eq.{u_8 + 1} (α := N')
    ((((polarBilin (f.compQuadraticMap' Q) : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
have h₂ : Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
  ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
Tactic: rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
    LinearMap.compQuadraticMap_polar]
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
N' : Type u_8
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x x_1 : M
h :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
h₁ :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((f : (a : N) → N') ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N) : N')
h₂ :
  Eq.{u_8 + 1} (α := N') (polar (⇑(f.compQuadraticMap' Q) : (a : M) → N') x x_1 : N')
    ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
⊢ Eq.{u_8 + 1} (α := N')
    ((((polarBilin (f.compQuadraticMap' Q) : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
    ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') x_1 : N')
have h₃ : Eq.{u_8 + 1} (α := N') ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
  ((f : (a : N) → N') (polar (⇑Q : (a : M) → N) x x_1) : N')
Tactic: rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
    LinearMap.compQuadraticMap_polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
        1 *
      2 =
    1
have h : ∀ (m : M),
  Eq (α := M)
    ((HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) sorry)
              1 *
            2 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
⊢ Eq (α := M)
    ((HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
              1 *
            2 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul (α := ℕ) 2 m) =
  m
Tactic: dsimp [Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 m) =
    m
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2 m) =
  m
Tactic: rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2 m) =
    m
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 m) =
    m
have h₁ : m = m
Tactic: rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
⊢ 2 *
      HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
        1 =
    1
have h : ∀ (m : M),
  Eq (α := M)
    ((2 *
            HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) sorry)
              1 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
⊢ Eq (α := M)
    ((2 *
            HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(Submonoid.center R)) (β := Module.End R M)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.center R) x)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) ⋯)
              1 :
          (a : M) → M)
        m :
      M)
    ((1 : (a : M) → M) m : M)
have h : HSMul.hSMul (α := ℕ) 2
    (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
  m
Tactic: dsimp [Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2
    (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
  m
Tactic: rw [← ofNat_smul_eq_nsmul R, smul_invOf_smul (2 : R) m]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
m : M
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) m) =
    m
have h₁ : m = m
Tactic: rw [← ofNat_smul_eq_nsmul R, smul_invOf_smul (2 : R) m]
-- 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
⊢ HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
      (((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) =
    Q.polarBilin
have h : ∀ (x x_1 : M),
  Eq.{u_5 + 1} (α := N)
    ((((HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
                  (((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_1 :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
Tactic: ext
-- 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 x_1 : M
⊢ Eq.{u_5 + 1} (α := N)
    ((((HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
                  (((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_1 :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
have h : HSMul.hSMul (α := ℕ) (β := N) 2
    ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N) =
  polar (⇑Q : (a : M) → N) x x_1
Tactic: dsimp
-- 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 x_1 : M
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h : Eq (α := N)
  ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
        (a : N) → N)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x_1 : N)) :
    N)
  (polar (⇑Q : (a : M) → N) x x_1 : N)
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]
-- 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 x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h₁ : Eq (α := N)
  ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
        (a : N) → N)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x_1 : N)) :
    N)
  (polar (⇑Q : (a : M) → N) x x_1 : N)
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]
-- 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 x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₁ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h₂ : Eq (α := N)
  ((HMul.hMul (α := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) : (a : N) → N)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x_1 : N)) :
    N)
  (polar (⇑Q : (a : M) → N) x x_1 : N)
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]
-- 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 x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₁ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₂ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h₃ : Eq (α := N)
  ((1 : (a : N) → N)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x_1 : N)) :
    N)
  (polar (⇑Q : (a : M) → N) x x_1 : N)
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]
-- 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 x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₁ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₂ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₃ :
  Eq (α := N)
    ((1 : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h₄ : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
    ((Q : (a : M) → N) x_1 : N) =
  polar (⇑Q : (a : M) → N) x x_1
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]
-- 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 x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₁ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₂ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₃ :
  Eq (α := N)
    ((1 : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₄ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x_1 : N) =
    polar (⇑Q : (a : M) → N) x x_1
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
have h₅ : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
    ((Q : (a : M) → N) x_1 : N) =
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
    ((Q : (a : M) → N) x_1 : N)
Tactic: rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]