awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
⊢ HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw₁ : HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
      R) =
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
    (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
Tactic: rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
rw₁ :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
⊢ HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw₂ : HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
      R) =
  HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
      R)
Tactic: rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (hypothesis)
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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
⊢ HSMul.hSMul (α := ℕ) 4
      (HPow.hPow (α := R) (β := ℕ)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        2) =
    P.coxeterWeight i j •
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
have hji : HSMul.hSMul (α := ℕ) (β := R) 2
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R) =
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
    (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
Tactic: have hji : 2 • (P.RootForm (P.root i)) (P.root j) =
      P.toLinearMap (P.root i) (2 • P.Polarization (P.root j)) := by
    rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
hji :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
⊢ HSMul.hSMul (α := ℕ) 4
      (HPow.hPow (α := R) (β := ℕ)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        2) =
    P.coxeterWeight i j •
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
have rw : HMul.hMul (α := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      (P.pairing j i) *
    HMul.hMul (α := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      (P.pairing i j) =
  P.pairing i j * P.pairing j i *
    HMul.hMul (α := R) (β := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
Tactic: rw [sq, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul, hij, ← rootForm_self_smul_coroot,
    smul_mul_assoc 2, ← mul_smul_comm, hji, ← rootForm_self_smul_coroot, map_smul, ← pairing,
    map_smul, ← pairing, smul_eq_mul, smul_eq_mul, smul_eq_mul, coxeterWeight]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i : ι
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      (∏ a : ι,
        (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) a) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) a : M))
      ((P.coroot : (a : ι) → N) i : N) ∈
    LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
have obtain : ∀ (c : R)
  (hc :
    ∏ i : ι,
        (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) =
      HMul.hMul (α := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        c),
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      (∏ a : ι,
        (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) a) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) a : M))
      ((P.coroot : (a : ι) → N) i : N) ∈
    LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
Tactic: obtain ⟨c, hc⟩ := Finset.dvd_prod_of_mem (fun a ↦ P.RootForm (P.root a) (P.root a))
    (Finset.mem_univ i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i : ι
c : R
hc :
  ∏ i : ι,
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) =
    HMul.hMul (α := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      c
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      (∏ a : ι,
        (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) a) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) a : M))
      ((P.coroot : (a : ι) → N) i : N) ∈
    LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
have rw : c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) ∈
  LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
Tactic: rw [hc, mul_comm, mul_smul, rootForm_self_smul_coroot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i : ι
c : R
hc :
  ∏ i : ι,
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) =
    HMul.hMul (α := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      c
⊢ ∃ (y : ↥(P.rootSpan R)),
    (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) y =
      c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have h : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N)
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (P.rootSpan R) x)
      (c • HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) i : M)) sorry) =
  c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: use ⟨c • 2 • P.root i, by aesop⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i_1 j i : ι
⊢ ∃ s > 0,
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
have refine : GT.gt.{u_5} (α := S) (∑ k : ι, HPow.hPow (β := ℕ) (P.pairingIn S i k) 2) 0
Tactic: refine ⟨∑ k, P.pairingIn S i k ^ 2, ?_, by simp [sq, rootForm_apply_apply]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
⊢ Eq (α := LinearMap.BilinForm.{u_5, u_3} S ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (RootPositiveForm.posForm (P.posRootForm S)) (P.RootFormIn S)
have h : ∀ (x x_1 : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
  Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x_1 :
      S)
    ((((P.RootFormIn S :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x_1 :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x x_1 : ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ Eq.{u_5 + 1} (α := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x_1 :
      S)
    ((((P.RootFormIn S :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              x :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        x_1 :
      S)
have h : Eq.{u_2 + 1} (α := R)
  ((algebraMap S R : (a : S) → R)
      ((((RootPositiveForm.posForm (P.posRootForm S) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                x :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          x_1 :
        S) :
    R)
  ((algebraMap S R : (a : S) → R)
      ((((P.RootFormIn S :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                x :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
                (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          x_1 :
        S) :
    R)
Tactic: apply FaithfulSMul.algebraMap_injective S R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
⊢ ∃ s ≥ 0,
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) s : R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
have refine : IsSumSq.{u_5} (R := S)
  ((((RootPositiveForm.posForm (P.posRootForm S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
              hx) :
          LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
            (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
        (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx) :
    S)
Tactic: refine ⟨(P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩, IsSumSq.nonneg ?_, by simp [posRootForm]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
⊢ IsSumSq.{u_5} (R := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
have choose : ∀ (s : (i : ι) → S)
  (hs :
    ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (s i) : R) ((P.coroot' i : (a : M) → R) x : R)),
  IsSumSq.{u_5} (R := S)
    ((((RootPositiveForm.posForm (P.posRootForm S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                x hx) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule S M) (span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) :
      S)
Tactic: choose s hs using P.coroot'_apply_apply_mem_of_mem_span S hx