awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
rw :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (x + y)
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
have rw₁ : f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
  f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)
Tactic: rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
    add_right_comm (f (x + y)), add_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
rw :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (x + y)
rw₁ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
have rw₂ : f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
  f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
Tactic: rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
    add_right_comm (f (x + y)), add_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
rw :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (x + y)
rw₁ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)
rw₂ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
have rw₃ : f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x + x') + f (x' + y) + f y ↔
  f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
Tactic: rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
    add_right_comm (f (x + y)), add_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
rw :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (x + y)
rw₁ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)
rw₂ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
rw₃ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x + x') + f (x' + y) + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
have rw₄ : f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y) ↔
  f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
Tactic: rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
    add_right_comm (f (x + y)), add_left_inj]
-- 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' x y : QuadraticMap R M N
h : x.toFun = y.toFun
⊢ x = y
have mk : ∀ (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (exists_companion' :
    ∃ (B : BilinMap R M N),
      ∀ (x y : M),
        toFun (x + y) =
          HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
  (h :
    { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
      y.toFun),
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } = y
Tactic: cases x
Cleared hypotheses: x, h
-- 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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' y : QuadraticMap R M N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
exists_companion' :
  ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      toFun (x + y) =
        HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
h :
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
    y.toFun
⊢ { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } = y
have mk : ∀ (toFun_1 : M → N) (toFun_smul_1 : ∀ (a : R) (x : M), toFun_1 (a • x) = (a * a) • toFun_1 x)
  (exists_companion'_1 :
    ∃ (B : BilinMap R M N),
      ∀ (x y : M),
        toFun_1 (x + y) =
          HAdd.hAdd (β := N) (toFun_1 x + toFun_1 y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
  (h :
    { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
      { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 :
          QuadraticMap R M N }.toFun),
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } =
    { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (z + x) : N)
have obtain : ∀ (B : BilinMap R M N)
  (h :
    ∀ (x y : M),
      (Q : (a : M) → N) (x + y) =
        HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)),
  HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (z + x) : N)
Tactic: obtain ⟨B, h⟩ := Q.exists_companion
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (z + x) : N)
have rw : HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
    (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
      ((Q : (a : M) → N) z : N)) =
  HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
    ((Q : (a : M) → N) (x + z) : N)
Tactic: rw [add_comm z x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (x + z) : N)
have simp : HAdd.hAdd (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N) +
      HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)
        ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
      ((Q : (a : M) → N) z : N) =
  HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) +
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q : (a : M) → N) z : N))
        ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) z : N))
      ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)
Tactic: simp only [h, LinearMap.map_add₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ (Q : (a : M) → N) (x + x) = HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)
have rw : HSMul.hSMul (β := N) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → N) x : N) =
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (↑4 : R) ((Q : (a : M) → N) x : N)
Tactic: rw [← two_smul R x, Q.map_smul, ← Nat.cast_smul_eq_nsmul R]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) 0 : N) (0 : N)
have rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := M) 0 0) : N) (0 : N)
Tactic: rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := M) 0 0) : N) (0 : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) 0 : N) (0 : N)
have rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) 0 0) ((Q : (a : M) → N) 0 : N) = 0
Tactic: rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := M) 0 0) : N) (0 : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) 0 0) ((Q : (a : M) → N) 0 : N) = 0
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) 0 : N) (0 : N)
have rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 0 ((Q : (a : M) → N) 0 : N) = 0
Tactic: rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := M) 0 0) : N) (0 : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) 0 0) ((Q : (a : M) → N) 0 : N) = 0
rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 0 ((Q : (a : M) → N) 0 : N) = 0
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) 0 : N) (0 : N)
have rw₃ : Eq.{u_5 + 1} (α := N) 0 0
Tactic: rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x : M
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
have rw : (Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) =
  HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x : M
rw :
  (Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
have rw₁ : HSMul.hSMul (β := N)
    (HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) a : R) ((algebraMap S R : (a : S) → R) a : R))
    ((Q : (a : M) → N) x : N) =
  HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x : M
rw :
  (Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₁ :
  HSMul.hSMul (β := N)
      (HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) a : R) ((algebraMap S R : (a : S) → R) a : R))
      ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
have rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (a * a) : R) ((Q : (a : M) → N) x : N) =
  HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x : M
rw :
  (Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₁ :
  HSMul.hSMul (β := N)
      (HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) a : R) ((algebraMap S R : (a : S) → R) a : R))
      ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₂ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (a * a) : R) ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
have rw₃ : HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
Tactic: rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)
have rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
Tactic: rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)
have rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) (-1) (-1)) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
Tactic: rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) (-1) (-1)) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)
have rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (- -1) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
Tactic: rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) (-1) (-1)) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (- -1) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)
have rw₃ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 1 ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
Tactic: rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) (-1) (-1)) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (- -1) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₃ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 1 ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)
have rw₄ : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
Tactic: rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (x - y) : N) ((Q : (a : M) → N) (y - x) : N)
have rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-(y - x)) : N) ((Q : (a : M) → N) (y - x) : N)
Tactic: rw [← neg_sub, Q.map_neg]
-- 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
Q : QuadraticMap R M N
x y : M
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-(y - x)) : N) ((Q : (a : M) → N) (y - x) : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (x - y) : N) ((Q : (a : M) → N) (y - x) : N)
have rw₁ : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (y - x) : N) ((Q : (a : M) → N) (y - x) : N)
Tactic: rw [← neg_sub, Q.map_neg]
-- 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
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have obtain : ∀ (B : BilinMap R M N)
  (h :
    ∀ (x y : M),
      (Q : (a : M) → N) (x + y) =
        HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)),
  polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
Tactic: obtain ⟨B, h⟩ := Q.exists_companion