awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
⊢ HSub.hSub (α := N)
      (∑ p ∈ l.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
      (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
    HSub.hSub (α := N)
      (sum (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) fun (i : Sym2 ι) (a : R) ↦
        HSMul.hSMul (β := N) a ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) i))
      ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))
have rw : HSub.hSub (α := N)
    (∑ p ∈ l.support.sym2,
      polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
        (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
    (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
  HSub.hSub (α := N)
    (∑ x ∈ l.support.sym2,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l.sym2Mul : (a : Sym2 ι) → R) x : R)
        ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) x))
    (∑ x ∈ l.support,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l * l : (a : ι) → R) x : R) (((⇑Q : (a : M) → N) ∘ g) x))
Tactic: rw [(l * l).sum_of_support_subset support_mul_subset_left _ <| by simp,
    l.sym2Mul.sum_of_support_subset support_sym2Mul_subset _ <| by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
bm : Basis ι R M
x : M
⊢ HSub.hSub (α := N) (β := N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := Sym2 M) (polarSym2 (⇑Q : (a : M) → N))
                (Sym2.map (⇑bm : (a : ι) → M))) :
            (a : Sym2 ι →₀ R) → N)
          (sym2Mul ((bm.repr : (a : M) → ι →₀ R) x) : Finsupp.{u_1, u_2} (Sym2 ι) R) :
        N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑Q : (a : M) → N) (⇑bm : (a : ι) → M)) :
            (a : ι →₀ R) → N)
          (HMul.hMul (α := ι →₀ R) (β := ι →₀ R) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)
            ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
        N) =
    (Q : (a : M) → N) x
have rw : Eq.{u_4 + 1} (α := N)
  ((Q : (a : M) → N)
      ((linearCombination R (⇑bm : (a : ι) → M) : (a : ι →₀ R) → M) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M) :
    N)
  ((Q : (a : M) → N) x : N)
Tactic: rw [← apply_linearCombination', Basis.linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
bm : Basis ι R M
x : M
rw :
  Eq.{u_4 + 1} (α := N)
    ((Q : (a : M) → N)
        ((linearCombination R (⇑bm : (a : ι) → M) : (a : ι →₀ R) → M) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M) :
      N)
    ((Q : (a : M) → N) x : N)
⊢ HSub.hSub (α := N) (β := N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := Sym2 M) (polarSym2 (⇑Q : (a : M) → N))
                (Sym2.map (⇑bm : (a : ι) → M))) :
            (a : Sym2 ι →₀ R) → N)
          (sym2Mul ((bm.repr : (a : M) → ι →₀ R) x) : Finsupp.{u_1, u_2} (Sym2 ι) R) :
        N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑Q : (a : M) → N) (⇑bm : (a : ι) → M)) :
            (a : ι →₀ R) → N)
          (HMul.hMul (α := ι →₀ R) (β := ι →₀ R) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)
            ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
        N) =
    (Q : (a : M) → N) x
have rw₁ : Eq.{u_4 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
Tactic: rw [← apply_linearCombination', Basis.linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ (Q : (a : M) → N) ((linearCombination R g : (a : ι →₀ R) → M) l : M) =
    HAdd.hAdd (α := N) (β := N) ((linearCombination R ((⇑Q : (a : M) → N) ∘ g) : (a : ι →₀ R) → N) (l * l) : N)
      (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (Sym2.mul (Sym2.map (⇑l : (a : ι) → R) p))
            (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p)) :
        N)
have simp_rw : HAdd.hAdd (α := N) (l.sum fun (i : ι) (r : R) ↦ r • HSMul.hSMul (β := N) r ((Q : (a : M) → N) (g i) : N))
    (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
      polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
        (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p)) =
  HAdd.hAdd (α := N) ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))
    (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (Sym2.mul (Sym2.map (⇑l : (a : ι) → R) p))
        (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p)))
Tactic: simp_rw [linearCombination_apply, map_finsuppSum, Q.map_smul, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ HAdd.hAdd (α := N) (l.sum fun (i : ι) (r : R) ↦ r • HSMul.hSMul (β := N) r ((Q : (a : M) → N) (g i) : N))
      (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p)) =
    HAdd.hAdd (α := N) ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))
      (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (Sym2.mul (Sym2.map (⇑l : (a : ι) → R) p))
          (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p)))
have rw : HAdd.hAdd (α := N) (l.sum fun (i : ι) (r : R) ↦ r • HSMul.hSMul (β := N) r ((Q : (a : M) → N) (g i) : N))
    (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
      polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
        (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p)) =
  HAdd.hAdd (α := N)
    (∑ x ∈ l.support,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l * l : (a : ι) → R) x : R) (((⇑Q : (a : M) → N) ∘ g) x))
    (∑ p ∈ l.support.sym2 with ¬p.IsDiag,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (Sym2.mul (Sym2.map (⇑l : (a : ι) → R) p))
        (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p)))
Tactic: rw [(l * l).sum_of_support_subset support_mul_subset_left _ <| by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ HAdd.hAdd (α := N) (β := N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑Q : (a : M) → N) (⇑bm : (a : ι) → M)) :
            (a : ι →₀ R) → N)
          (HMul.hMul (α := ι →₀ R) (β := ι →₀ R) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)
            ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
        N)
      (∑ p ∈ Finset.sym2 (support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with ¬p.IsDiag,
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
            (Sym2.mul (Sym2.map (⇑((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) p))
            (polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N) (Sym2.map (⇑bm : (a : ι) → M) p)) :
        N) =
    (Q : (a : M) → N) x
have rw : Eq.{u_4 + 1} (α := N)
  ((Q : (a : M) → N)
      ((linearCombination R (⇑bm : (a : ι) → M) : (a : ι →₀ R) → M) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M) :
    N)
  ((Q : (a : M) → N) x : N)
Tactic: rw [← apply_linearCombination, Basis.linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
rw :
  Eq.{u_4 + 1} (α := N)
    ((Q : (a : M) → N)
        ((linearCombination R (⇑bm : (a : ι) → M) : (a : ι →₀ R) → M) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M) :
      N)
    ((Q : (a : M) → N) x : N)
⊢ HAdd.hAdd (α := N) (β := N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑Q : (a : M) → N) (⇑bm : (a : ι) → M)) :
            (a : ι →₀ R) → N)
          (HMul.hMul (α := ι →₀ R) (β := ι →₀ R) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)
            ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
        N)
      (∑ p ∈ Finset.sym2 (support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with ¬p.IsDiag,
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
            (Sym2.mul (Sym2.map (⇑((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) p))
            (polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N) (Sym2.map (⇑bm : (a : ι) → M) p)) :
        N) =
    (Q : (a : M) → N) x
have rw₁ : Eq.{u_4 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
Tactic: rw [← apply_linearCombination, Basis.linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
⊢ (Q.toBilin bm).toQuadraticMap = Q
have H : ∀ (x : M), Eq.{u_4 + 1} (α := N) (((Q.toBilin bm).toQuadraticMap : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ Eq.{u_4 + 1} (α := N) (((Q.toBilin bm).toQuadraticMap : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
have H : Eq.{u_4 + 1} (α := N)
  (((Q.toBilin bm : (a : M) → M →ₗ[R] N)
          (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
            HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
              ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M)) :
        (a : M) → N)
      (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
          ((bm : (a : ι) → M) a : M)) :
    N)
  ((Q : (a : M) → N)
      (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
          ((bm : (a : ι) → M) a : M)) :
    N)
Tactic: rw [← bm.linearCombination_repr x, LinearMap.BilinMap.toQuadraticMap_apply,
      Finsupp.linearCombination_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ Eq.{u_4 + 1} (α := N)
    (((Q.toBilin bm : (a : M) → M →ₗ[R] N)
            (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
              HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M)) :
          (a : M) → N)
        (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M)) :
      N)
    ((Q : (a : M) → N)
        (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M)) :
      N)
have H : HAdd.hAdd (α := N)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1 : M) : N)))
    (∑ x_1 ∈ Finset.offDiag (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)),
      if x_1.1 = x_1.2 then
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R)
            ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1.1 : M) : N))
      else
        if x_1.1 < x_1.2 then
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R)
            (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
              ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R)
              (polar.{u_3, u_4} (M := M) ((⇑Q : (a : M) → N) : (a : M) → N) ((bm : (a : ι) → M) x_1.1 : M)
                ((bm : (a : ι) → M) x_1.2 : M)))
        else 0) =
  (Q : (a : M) → N)
    (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
        ((bm : (a : ι) → M) a : M))
Tactic: simp_rw [LinearMap.map_sum₂, map_sum, LinearMap.map_smul₂, map_smul, toBilin_apply,
    smul_ite, smul_zero, ← Finset.sum_product', ← Finset.diag_union_offDiag,
    Finset.sum_union (Finset.disjoint_diag_offDiag _), Finset.sum_diag, if_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x_1 : M
x : ι × ι
hx :
  Membership.mem (γ := Finset (ι × ι))
    (Finset.offDiag (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x_1))) x
⊢ ¬x.1 = x.2
have hx₁ : Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x_1)) x.1 ∧
  Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x_1)) x.2 ∧
    x.1 ≠ x.2
Tactic: rw [Finset.mem_offDiag] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Free R M
Q : QuadraticMap R M N
⊢ ∃ (a : BilinMap R M N), a.toQuadraticMap = Q
have obtain : ∀ (ι : Type u_3) (b : Basis ι R M), ∃ (a : BilinMap R M N), a.toQuadraticMap = Q
Tactic: obtain ⟨ι, b⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
⊢ (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm
have refine : ∀ (i j : ι),
  Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
Tactic: refine bm.ext fun i => bm.ext fun j => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
⊢ Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
have inl : ∀ (h : i < j),
  Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
Tactic: obtain h | rfl | h := lt_trichotomy i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
inl :
  ∀ (h : i < j),
    Eq.{u_4 + 1} (α := N)
      (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
          ((bm : (a : ι) → M) j : M) :
        N)
      ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
          ((bm : (a : ι) → M) j : M) :
        N)
⊢ Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
have inr : Eq.{u_4 + 1} (α := N)
  (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
      ((bm : (a : ι) → M) i : M) :
    N)
  ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
      ((bm : (a : ι) → M) i : M) :
    N)
Tactic: obtain h | rfl | h := lt_trichotomy i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
inl :
  ∀ (h : i < j),
    Eq.{u_4 + 1} (α := N)
      (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
          ((bm : (a : ι) → M) j : M) :
        N)
      ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
          ((bm : (a : ι) → M) j : M) :
        N)
inr :
  Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) i : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) i : M) :
      N)
⊢ Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
have inr₁ : ∀ (h : j < i),
  Eq.{u_4 + 1} (α := N)
    (((((Q₁ + Q₂).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((Q₁.toBilin bm + Q₂.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
Tactic: obtain h | rfl | h := lt_trichotomy i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S R
inst_8 : Module S N
inst_9 : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
⊢ (s • Q).toBilin bm = s • Q.toBilin bm
have refine : ∀ (i j : ι),
  Eq.{u_4 + 1} (α := N)
    (((((s • Q).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((s • Q.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
Tactic: refine bm.ext fun i => bm.ext fun j => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
S : Type u_5
inst_6 : CommSemiring S
inst_7 : Algebra S R
inst_8 : Module S N
inst_9 : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
⊢ Eq.{u_4 + 1} (α := N)
    (((((s • Q).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((s • Q.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
have inl : ∀ (h : i < j),
  Eq.{u_4 + 1} (α := N)
    (((((s • Q).toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
    ((((s • Q.toBilin bm : (a : M) → M →ₗ[R] N) ((bm : (a : ι) → M) i) : M →ₗ[R] N) : (a : M) → N)
        ((bm : (a : ι) → M) j : M) :
      N)
Tactic: obtain h | rfl | h := lt_trichotomy i j