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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
hP :
  Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
    (∑ j : ι,
        HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
          ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N) :
      N)
⊢ Eq.{u_4 + 1} (α := N)
    (∑ i_1 : ι, HSMul.hSMul (β := N) (P.pairingIn S i i_1 * P.pairingIn S i i_1) ((P.coroot : (a : ι) → N) i : N))
    (∑ x : ι, P.pairingIn S i x • HSMul.hSMul (β := N) (P.pairing i x) ((P.coroot : (a : ι) → N) i : N))
have refine : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    HSMul.hSMul (β := N) (P.pairingIn S i x * P.pairingIn S i x) ((P.coroot : (a : ι) → N) i : N) =
      P.pairingIn S i x • HSMul.hSMul (β := N) (P.pairing i x) ((P.coroot : (a : ι) → N) i : N)
Tactic: refine Finset.sum_congr rfl ?_
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
hP :
  Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
    (∑ j : ι,
        HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
          ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N) :
      N)
j : ι
hj : Membership.mem (γ := Finset ι) Finset.univ j
⊢ HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j • HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)
have rw : HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
  P.pairingIn S i j •
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
      ((P.coroot : (a : ι) → N) i : N)
Tactic: rw [← P.algebraMap_pairingIn S, IsScalarTower.algebraMap_smul, ← mul_smul]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
hP :
  Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
    (∑ j : ι,
        HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
          ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N) :
      N)
j : ι
hj : Membership.mem (γ := Finset ι) Finset.univ j
rw :
  HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j •
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((P.coroot : (a : ι) → N) i : N)
⊢ HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j • HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)
have rw₁ : HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
  P.pairingIn S i j • HSMul.hSMul (β := N) (P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N)
Tactic: rw [← P.algebraMap_pairingIn S, IsScalarTower.algebraMap_smul, ← mul_smul]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
hP :
  Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
    (∑ j : ι,
        HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
          ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N) :
      N)
j : ι
hj : Membership.mem (γ := Finset ι) Finset.univ j
rw :
  HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j •
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((P.coroot : (a : ι) → N) i : N)
rw₁ :
  HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j • HSMul.hSMul (β := N) (P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N)
⊢ HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
    P.pairingIn S i j • HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)
have rw₂ : HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N) =
  HSMul.hSMul (β := N) (P.pairingIn S i j * P.pairingIn S i j) ((P.coroot : (a : ι) → N) i : N)
Tactic: rw [← P.algebraMap_pairingIn S, IsScalarTower.algebraMap_smul, ← mul_smul]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
      (∏ j : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S j) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S j))
      ((P.coroot : (a : ι) → N) i : N))
have obtain : ∀ (c : S)
  (hc :
    ∏ i : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) =
      HMul.hMul (α := S)
        ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i) :
          S)
        c),
  Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
      (∏ j : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S j) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S j))
      ((P.coroot : (a : ι) → N) i : N))
Tactic: obtain ⟨c, hc⟩ := Finset.dvd_prod_of_mem
    (fun j ↦ P.RootFormIn S (P.rootSpanMem S j) (P.rootSpanMem S j))
    (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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
⊢ Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
    (HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
      (∏ j : ι,
        (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S j) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S j))
      ((P.coroot : (a : ι) → N) i : N))
have rw : Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
  (c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N))
Tactic: rw [hc, mul_comm, mul_smul, rootFormIn_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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
⊢ ∃ (y : ↥(P.rootSpan S)),
    (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) y =
      c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
have h : (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
    (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
  c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
Tactic: use c • 2 • (P.rootSpanMem S 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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
⊢ (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
      (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
have h : HSMul.hSMul (β := N) c
    ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
        (HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) :
      N) =
  c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
Tactic: rw [map_smul, two_smul, two_smul, map_add]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
h :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
⊢ (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
      (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
have h₁ : HSMul.hSMul (β := N) c
    ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
        (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
      N) =
  c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
Tactic: rw [map_smul, two_smul, two_smul, map_add]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
h :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₁ :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
⊢ (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
      (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
have h₂ : HSMul.hSMul (β := N) c
    ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
        (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
      N) =
  c •
    HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
Tactic: rw [map_smul, two_smul, two_smul, map_add]
-- 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 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
h :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₁ :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₂ :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
        N) =
    c •
      HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
        ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
⊢ (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
      (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
have h₃ : c •
    HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N) =
  c •
    HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
Tactic: rw [map_smul, two_smul, two_smul, map_add]
-- 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 (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw : HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
    ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
          (a : ↥(P.rootSpan R)) → R)
        (P.rootSpanMem R i) :
      R)
    ((P.coroot : (a : ι) → N) i : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]
-- 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 : ι
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
              LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
            (a : ↥(P.rootSpan R)) → R)
          (P.rootSpanMem R i) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw₁ : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn R : (a : ↥(P.rootSpan R)) → N) (P.rootSpanMem R i) : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]