awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₁ : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₂ : HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
    ((g : (a : M) → A) (a • x) : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₃ : HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₄ : HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
    HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₅ : HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₅ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₆ : a • HMul.hMul (α := A) ((f : (a : M) → A) x : A) (HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A)) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₅ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₆ :
  a • HMul.hMul (α := A) ((f : (a : M) → A) x : A) (HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A)) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₇ : a • a • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₅ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₆ :
  a • HMul.hMul (α := A) ((f : (a : M) → A) x : A) (HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A)) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₇ :
  a • a • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₈ : (a • a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a • x) : A) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₂ :
  HMul.hMul (β := A) (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((f : (a : M) → A) x : A))
      ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₃ :
  HMul.hMul (β := A) (HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A)) ((g : (a : M) → A) (a • x) : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₄ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) *
      HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) a : R) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₅ :
  HSMul.hSMul (β := A) a ((f : (a : M) → A) x : A) * HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₆ :
  a • HMul.hMul (α := A) ((f : (a : M) → A) x : A) (HSMul.hSMul (β := A) a ((g : (a : M) → A) x : A)) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₇ :
  a • a • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
rw₈ :
  (a • a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
    (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (a • x) =
    (a * a) • HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x
have rw₉ : (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) =
  (a * a) • HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
-- 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 : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
f g : M →ₗ[R] A
x y : M
⊢ HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) (x + y) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) x +
        HMul.hMul (α := (a : M) → A) (β := (a : M) → A) (⇑f : (a : M) → A) (⇑g : (a : M) → A) y)
      ((((LinearMap.compl₁₂ (LinearMap.mul R A) f g + LinearMap.compl₁₂ (LinearMap.flip (LinearMap.mul R A)) g f :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          y :
        A)
have simp : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A) +
    (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A)) =
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) y : A) +
    (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((g : (a : M) → A) y : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((g : (a : M) → A) x : A))
Tactic: simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply,
        LinearMap.compl₁₂_apply, LinearMap.mul_apply', LinearMap.flip_apply]
-- 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
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁ = Q₂
have apply : HSMul.hSMul (α := R) 2 Q₁ = HSMul.hSMul (α := R) 2 Q₂
Tactic: apply h.smul_left_cancel.mp
-- 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
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ HSMul.hSMul (α := R) 2 Q₁ = HSMul.hSMul (α := R) 2 Q₂
have rw : HSMul.hSMul (α := R) (↑2 : R) Q₁ = HSMul.hSMul (α := R) (↑2 : R) Q₂
Tactic: rw [show (2 : R) = (2 : ℕ) by rfl]
-- 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
h : IsUnit.{u_3} (M := R) 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ HSMul.hSMul (α := R) (↑2 : R) Q₁ = HSMul.hSMul (α := R) (↑2 : R) Q₂
have simp_rw : Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap
Tactic: simp_rw [Nat.cast_smul_eq_nsmul R, ← QuadraticMap.toQuadraticMap_polarBilin]
-- 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
⊢ polarBilin (f.compQuadraticMap' Q) = compr₂ Q.polarBilin f
have h : ∀ (x x_1 : M),
  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')
Tactic: ext
-- 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
⊢ 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')
  ((((compr₂ Q.polarBilin f : (a : M) → M →ₗ[R] N') x : M →ₗ[R] N') : (a : M) → N') 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')
⊢ 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') ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N) : N')
Tactic: rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
    LinearMap.compQuadraticMap_polar]