awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), LinearMap.ker (P.coroot' i)) x
y : M
⊢ Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((0 : (a : M) → R) y : R)

Tactic:
simp_all [coroot', rootForm_apply_apply]

Premises used: RootPairing.coroot', RootPairing.rootForm_apply_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
⊢ Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R)) ≤
    LinearMap.ker P.CorootForm

Tactic:
P.flip.corootSpan_dualAnnihilator_le_ker_rootForm

Premises used: Set.Mem, RootPairing.flip, setOf, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_12 : Fintype ι
x : ↥(P.rootSpan S)
⊢ Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N)
    (∑ i : ι,
        HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
          ((P.coroot : (a : ι) → N) i : N) :
      N)

Tactic:
simp [PolarizationIn]

Premises used: RootPairing.PolarizationIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : ↥(P.rootSpan S)
simp :
  Eq.{u_4 + 1} (α := N)
    (∑ x_1 : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S x_1 : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) x_1 : N))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N))
⊢ Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N)
    ((P.Polarization : (a : M) → N) (↑x : M) : N)

Tactic:
simp only [PolarizationIn, LinearMap.coe_sum, LinearMap.coe_comp, Finset.sum_apply, comp_apply,
    LinearMap.toSpanSingleton_apply, Polarization_apply]

Premises used: RootPairing.Polarization_apply, Finset.sum_apply, RootPairing.PolarizationIn, LinearMap.coe_sum, LinearMap.toSpanSingleton_apply, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : ↥(P.rootSpan S)
⊢ Eq.{u_4 + 1} (α := N)
    (∑ x_1 : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S x_1 : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) x_1 : N))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N))

Tactic:
Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : ↥(P.rootSpan S)
refine :
  ∀ (i : ι) (hi : Membership.mem (γ := Finset ι) Finset.univ i),
    HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) i : N) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N)
⊢ Eq.{u_4 + 1} (α := N)
    (∑ x_1 : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S x_1 : (a : ↥(P.rootSpan S)) → S) x : S)
        ((P.coroot : (a : ι) → N) x_1 : N))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N))

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : ↥(P.rootSpan S)
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((algebraMap S R : (a : S) → R) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) : R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N)
rw₁ rw₂ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N)
⊢ HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N)

Tactic:
rw [algebra_compatible_smul R (P.coroot'In S i x) (P.coroot i), algebraMap_coroot'In_apply]

Premises used: algebra_compatible_smul, RootPairing.algebraMap_coroot'In_apply, RootPairing.coroot, DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
h :
  ∀ (x : N),
    x ∈ Submodule.map P.Polarization (P.rootSpan R) ↔
      Membership.mem (γ := Submodule R N) (LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R)) x
⊢ Submodule.map P.Polarization (P.rootSpan R) = LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : N
⊢ x ∈ Submodule.map P.Polarization (P.rootSpan R) ↔
    Membership.mem (γ := Submodule R N) (LinearMap.range (M := ↥(P.rootSpan R)) (P.PolarizationIn R)) x

Tactic:
simp [PolarizationIn_eq]

Premises used: RootPairing.PolarizationIn_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Module S N
inst_10 : IsScalarTower S R N
inst_11 : P.IsValuedIn S
inst_12 : Fintype ι
x : ↥(P.corootSpan S)
⊢ Eq.{u_3 + 1} (α := M) ((P.CoPolarizationIn S : (a : ↥(P.corootSpan S)) → M) x : M)
    (∑ i : ι,
        HSMul.hSMul.{u_5, u_3, u_3} (α := S) (β := M) ((P.root'In S i : (a : ↥(P.corootSpan S)) → S) x : S)
          ((P.root : (a : ι) → M) i : M) :
      M)

Tactic:
P.flip.PolarizationIn_apply S x

Premises used: RootPairing.flip, RootPairing.PolarizationIn_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x : ↥(P.corootSpan S)
⊢ Eq.{u_3 + 1} (α := M) ((P.CoPolarizationIn S : (a : ↥(P.corootSpan S)) → M) x : M)
    ((P.CoPolarization : (a : N) → M) (↑x : N) : M)

Tactic:
P.flip.PolarizationIn_eq S x

Premises used: RootPairing.flip, RootPairing.PolarizationIn_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_11 : Fintype ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) x :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            y :
          S) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
simp [RootFormIn, rootForm_apply_apply]

Premises used: RootPairing.rootForm_apply_apply, RootPairing.RootFormIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x y : ↥(P.rootSpan S)
rw :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑y : M) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) (↑x : M) : N) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑y : M) : N →ₗ[R] R) : (a : N) → R)
        ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N) :
      R)
    ((algebraMap S R : (a : S) → R)
        ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) x :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            y :
          S) :
      R)

Tactic:
rw [PolarizationIn_eq, algebraMap_rootFormIn]

Premises used: RootPairing.PolarizationIn_eq, RootPairing.algebraMap_rootFormIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑y : M) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) (↑x : M) : N) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
toLinearMap_apply_apply_Polarization P x y

Premises used: RootPairing.toLinearMap_apply_apply_Polarization, Subtype.val
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 ι
x y : ↥(P.rootSpan S)
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑y : M) : N →ₗ[R] R) : (a : N) → R)
        ((P.Polarization : (a : M) → N) (↑x : M) : N) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R)

Tactic:
exact toLinearMap_apply_apply_Polarization P x y

Premises used: RootPairing.toLinearMap_apply_apply_Polarization, Subtype.val
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_12 : Fintype ι
x : N
hx : Membership.mem (γ := Submodule S N) (LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) x
obtain :
  ∀ (y : ↥(P.rootSpan S)) (hy : (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) y = x),
    Membership.mem (γ := Submodule S N) (P.corootSpan S) x
⊢ Membership.mem (γ := Submodule S N) (P.corootSpan S) x

Tactic:
obtain ⟨y, hy⟩ := hx
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_12 : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy : (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) y = x
⊢ ∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)
        ((P.coroot : (a : ι) → N) i : N) =
    x

Tactic:
rw [PolarizationIn_apply] at hy

Premises used: RootPairing.PolarizationIn_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_12 : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy :
  ∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)
        ((P.coroot : (a : ι) → N) i : N) =
    x
⊢ Membership.mem (γ := Submodule S N) (P.corootSpan S) x

Tactic:
(Submodule.mem_span_range_iff_exists_fun S).mpr
    (Exists.intro (fun i ↦ (P.coroot'In S i) y) hy)

Premises used: Iff.mpr, Set.Mem, Submodule.mem_span_range_iff_exists_fun, Exists.intro, DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : P.IsValuedIn S
inst_12 : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy :
  ∑ i : ι,
      HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) y : S)
        ((P.coroot : (a : ι) → N) i : N) =
    x
⊢ Membership.mem (γ := Submodule S N) (P.corootSpan S) x

Tactic:
exact (Submodule.mem_span_range_iff_exists_fun S).mpr
    (Exists.intro (fun i ↦ (P.coroot'In S i) y) hy)

Premises used: Iff.mpr, Submodule.mem_span_range_iff_exists_fun, Exists.intro, DFunLike.coe, RootPairing.coroot'In
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : ι
simp_rw :
  Eq.{u_4 + 1} (α := N) (∑ x : ι, HSMul.hSMul (β := N) (P.pairingIn S i x) ((P.coroot : (a : ι) → N) x : N))
    (∑ j : ι,
      HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
        ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N))
⊢ 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)

Tactic:
simp_rw [PolarizationIn_apply, coroot'In_rootSpanMem_eq_pairingIn]

Premises used: RootPairing.coroot'In_rootSpanMem_eq_pairingIn, RootPairing.PolarizationIn_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : ι
⊢ Eq.{u_4 + 1} (α := N) (∑ x : ι, HSMul.hSMul (β := N) (P.pairingIn S i x) ((P.coroot : (a : ι) → N) x : N))
    (∑ j : ι,
      HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
        ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N))

Tactic:
(Fintype.sum_equiv (P.reflectionPerm i)
          (fun j ↦ P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j))
          (fun j ↦ P.pairingIn S i j • P.coroot j) (congrFun rfl)).symm

Premises used: RootPairing.pairingIn, congrFun, RootPairing.reflectionPerm, HSMul.hSMul, RootPairing.coroot, Fintype.sum_equiv, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : ι
⊢ Eq.{u_4 + 1} (α := N) (∑ x : ι, HSMul.hSMul (β := N) (P.pairingIn S i x) ((P.coroot : (a : ι) → N) x : N))
    (∑ j : ι,
      HSMul.hSMul (β := N) (P.pairingIn S i ((P.reflectionPerm i : (a : ι) → ι) j))
        ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N))

Tactic:
exact (Fintype.sum_equiv (P.reflectionPerm i)
          (fun j ↦ P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j))
          (fun j ↦ P.pairingIn S i j • P.coroot j) (congrFun rfl)).symm

Premises used: RootPairing.pairingIn, congrFun, RootPairing.reflectionPerm, HSMul.hSMul, RootPairing.coroot, Fintype.sum_equiv, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : ι
⊢ 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)

Tactic:
have hP : P.PolarizationIn S (P.rootSpanMem S i) =
      ∑ j : ι, P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j) := by
    simp_rw [PolarizationIn_apply, coroot'In_rootSpanMem_eq_pairingIn]
    exact (Fintype.sum_equiv (P.reflectionPerm i)
          (fun j ↦ P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j))
          (fun j ↦ P.pairingIn S i j • P.coroot j) (congrFun rfl)).symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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)
rw :
  HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
      ((((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)
      ((P.coroot : (a : ι) → N) i : N) =
    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)
⊢ HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N)
      ((((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)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)

Tactic:
rw [two_nsmul]

Premises used: two_nsmul