awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
inst_9 : P.IsRootSystem
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ Eq.{u_6 + 1} (α := Submodule R M₂)
    (span R (range.{u_6, u_5 + 1} (ι := ι₂) (⇑(RootPairing.map (P := P) e f g).root : (a : ι₂) → M₂))) ⊤

Tactic:
simp [RootPairing.map, Embedding.coe_trans, range_comp]

Premises used: Set.range_comp, Function.Embedding.coe_trans, RootPairing.map
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
inst_9 : P.IsRootSystem
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ Eq.{u_7 + 1} (α := Submodule R N₂)
    (span R (range.{u_7, u_5 + 1} (ι := ι₂) (⇑(RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂))) ⊤

Tactic:
simp [Embedding.coe_trans, range_comp, RootPairing.map]

Premises used: Set.range_comp, Function.Embedding.coe_trans, RootPairing.map
-- 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
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) x : N)
    (∑ i : ι,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) x : R)
          ((P.coroot : (a : ι) → N) i : N) :
      N)

Tactic:
simp [Polarization]

Premises used: RootPairing.Polarization
-- 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
⊢ Eq.{u_3 + 1} (α := M) ((P.CoPolarization : (a : N) → M) x : M)
    (∑ i : ι,
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.root' i : (a : N) → R) x : R) ((P.root : (a : ι) → M) i : M) :
      M)

Tactic:
P.flip.Polarization_apply x

Premises used: RootPairing.Polarization_apply, RootPairing.flip
-- 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 ι
⊢ P.CoPolarization = P.flip.Polarization

Tactic:
rfl

Premises used: RootPairing.CoPolarization, 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
inst_5 : Fintype ι
x y : M
⊢ Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.coroot' i : (a : M) → R) x : R) ((P.coroot' i : (a : M) → R) y : R) : R)

Tactic:
simp [RootForm]

Premises used: RootPairing.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
inst_5 : Fintype ι
x y : N
⊢ Eq.{u_2 + 1} (α := R) ((((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)
    (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.root' i : (a : N) → R) x : R) ((P.root' i : (a : N) → R) y : R) : R)

Tactic:
P.flip.rootForm_apply_apply x y

Premises used: RootPairing.flip, 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 ι
x y : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((P.Polarization : (a : M) → N) x : N) : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
simp [RootForm]

Premises used: RootPairing.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
inst_5 : Fintype ι
x : N
h :
  ∀ (y : N),
    Eq.{u_2 + 1} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)
⊢ Eq (α := N →ₗ[R] R) ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R)
    ((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R)

Tactic:
ext y
-- 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 y : N
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
    ((((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
P.flip.toLinearMap_apply_apply_Polarization x y

Premises used: RootPairing.toLinearMap_apply_apply_Polarization, RootPairing.flip
-- 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 y : N
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
    ((((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
exact P.flip.toLinearMap_apply_apply_Polarization x y

Premises used: RootPairing.toLinearMap_apply_apply_Polarization, RootPairing.flip
-- 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 x_1 : M),
    Eq.{u_2 + 1} (α := R)
      ((((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)
⊢ P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm

Tactic:
ext
-- 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 x_1 : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)

Tactic:
simp [rootForm_apply_apply, RootPairing.flip]

Premises used: RootPairing.flip, 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 ι
⊢ P.toLinearMap ∘ₗ P.CoPolarization = P.CorootForm

Tactic:
P.flip.flip_comp_polarization_eq_rootForm

Premises used: RootPairing.flip_comp_polarization_eq_rootForm, RootPairing.flip, RootPairing.CoPolarization, LinearMap.mk₂'ₛₗ, RootPairing.CorootForm, LinearMap.flip
-- 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 ι
m : M
rw :
  Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
    Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
    Eq (α := M →ₗ[R] R) ((P.RootForm : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
rw [← flip_comp_polarization_eq_rootForm]

Premises used: RootPairing.flip_comp_polarization_eq_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
inst_5 : Fintype ι
m : M
h : Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N)
⊢ Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
simp [h]
-- 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 ι
m : M
refine :
  Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R) →
    Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
    Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
refine ⟨fun h ↦ by simp [h], ?_⟩
-- 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 ι
m : M
h :
  Eq (α := Dual R M) ((P.flip.toPerfPair : (a : N) → Dual R M) ((P.Polarization : (a : M) → N) m) : Dual R M)
    (0 : Dual R M)
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N)

Tactic:
simpa only [EmbeddingLike.map_eq_zero_iff] using h

Premises used: EmbeddingLike.map_eq_zero_iff
-- 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 ι
n : N
⊢ Eq.{u_3 + 1} (α := M) ((P.CoPolarization : (a : N) → M) n : M) (0 : M) ↔
    Eq (α := N →ₗ[R] R) ((P.CorootForm : (a : N) → N →ₗ[R] R) n : N →ₗ[R] R) (0 : N →ₗ[R] R)

Tactic:
P.flip.polarization_apply_eq_zero_iff n

Premises used: RootPairing.flip, RootPairing.polarization_apply_eq_zero_iff
-- 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 : M), x ∈ P.Polarization.ker ↔ x ∈ LinearMap.ker P.RootForm
⊢ P.Polarization.ker = LinearMap.ker P.RootForm

Tactic:
ext
-- 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
⊢ x ∈ P.Polarization.ker ↔ x ∈ LinearMap.ker P.RootForm

Tactic:
simp only [LinearMap.mem_ker, P.polarization_apply_eq_zero_iff]

Premises used: LinearMap.mem_ker, RootPairing.polarization_apply_eq_zero_iff
-- 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 ι
⊢ P.CoPolarization.ker = LinearMap.ker P.CorootForm

Tactic:
P.flip.ker_polarization_eq_ker_rootForm

Premises used: RootPairing.flip, RootPairing.CoPolarization, RootPairing.CorootForm, RootPairing.ker_polarization_eq_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
inst_5 : Fintype ι
⊢ LinearMap.IsSymm P.RootForm

Tactic:
simp [LinearMap.isSymm_def, mul_comm, rootForm_apply_apply]

Premises used: LinearMap.isSymm_def, RootPairing.rootForm_apply_apply, mul_comm
-- 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 ι
i : ι
x y : M
simp :
  Eq.{u_2 + 1} (α := R)
    (∑ x_1 : ι,
      HMul.hMul (α := R) (β := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) x : R)
        ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) y : R))
    (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.coroot' i : (a : M) → R) x : R) ((P.coroot' i : (a : M) → R) y : R))
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.reflection i : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((P.reflection i : (a : M) → M) y : M) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
simp only [rootForm_apply_apply, coroot'_reflection]

Premises used: RootPairing.rootForm_apply_apply, RootPairing.coroot'_reflection
-- 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 ι
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x_1 : ι,
      HMul.hMul (α := R) (β := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) x : R)
        ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) y : R))
    (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.coroot' i : (a : M) → R) x : R) ((P.coroot' i : (a : M) → R) y : R))

Tactic:
Fintype.sum_equiv (P.reflectionPerm i)
    (fun j ↦ (P.coroot' (P.reflectionPerm i j) x) * (P.coroot' (P.reflectionPerm i j) y))
    (fun j ↦ P.coroot' j x * P.coroot' j y) (congrFun rfl)

Premises used: HMul.hMul, RootPairing.coroot', congrFun, RootPairing.reflectionPerm, Fintype.sum_equiv, 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
inst_5 : Fintype ι
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x_1 : ι,
      HMul.hMul (α := R) (β := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) x : R)
        ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) y : R))
    (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.coroot' i : (a : M) → R) x : R) ((P.coroot' i : (a : M) → R) y : R))

Tactic:
exact Fintype.sum_equiv (P.reflectionPerm i)
    (fun j ↦ (P.coroot' (P.reflectionPerm i j) x) * (P.coroot' (P.reflectionPerm i j) y))
    (fun j ↦ P.coroot' j x * P.coroot' j y) (congrFun rfl)

Premises used: HMul.hMul, RootPairing.coroot', congrFun, RootPairing.reflectionPerm, Fintype.sum_equiv, 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
inst_5 : Fintype ι
x : M
⊢ IsSumSq.{u_2} (R := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
P.rootForm_apply_apply x x ▸ IsSumSq.sum_mul_self Finset.univ _

Premises used: Finset.univ, Eq.rec, IsSumSq.sum_mul_self, RootPairing.rootForm_apply_apply, Eq.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
inst_5 : Fintype ι
j : ι
⊢ Eq.{u_2 + 1} (α := 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)
    (∑ i : ι, P.pairing j i * P.pairing j i : R)

Tactic:
simp [rootForm_apply_apply]

Premises used: 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 ι
y : N
hy : y ∈ LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
obtain :
  ∀ (x : ↥(P.rootSpan R)) (hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y),
    Membership.mem (γ := Submodule R N) (P.corootSpan R) y
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R) y

Tactic:
obtain ⟨x, hx⟩ := hy
-- 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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
rw :
  Membership.mem (γ := Submodule R N) (P.corootSpan R)
    (∑ 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))
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R) y

Tactic:
rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]

Premises used: RootPairing.Polarization_apply, LinearMap.domRestrict_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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R)
    (∑ 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:
(Submodule.mem_span_range_iff_exists_fun R).mpr ?_

Premises used: Iff.mpr, Set.Mem, Submodule.mem_span_range_iff_exists_fun
-- 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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
refine :
  ∃ (c : ι → R),
    Eq.{u_4 + 1} (α := N) (∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : 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))
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R)
    (∑ 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 (Submodule.mem_span_range_iff_exists_fun R).mpr ?_

Premises used: Iff.mpr, Submodule.mem_span_range_iff_exists_fun
-- 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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
h :
  Eq.{u_4 + 1} (α := N)
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
        ((fun (i : ι) ↦
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑x : M) : N →ₗ[R] R) : (a : N) → R)
                ((P.coroot : (a : ι) → N) i : N) :
              R))
          i)
        ((P.coroot : (a : ι) → N) i : 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))
⊢ ∃ (c : ι → R),
    Eq.{u_4 + 1} (α := N) (∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : 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:
use fun i => P.toLinearMap x (P.coroot i)

Premises used: RootPairing.toLinearMap, RootPairing.coroot, Subtype.val, DFunLike.coe
-- 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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
⊢ Eq.{u_4 + 1} (α := N)
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
        ((fun (i : ι) ↦
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑x : M) : N →ₗ[R] R) : (a : N) → R)
                ((P.coroot : (a : ι) → N) i : N) :
              R))
          i)
        ((P.coroot : (a : ι) → N) i : 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:
simp
-- 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 ι
rw : ⨅ (i : ι), LinearMap.ker (P.coroot' i) ≤ LinearMap.ker P.RootForm
⊢ Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)) ≤
    LinearMap.ker P.RootForm

Tactic:
rw [P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot']

Premises used: RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'
-- 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
h :
  ∀ (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)
⊢ x ∈ LinearMap.ker P.RootForm

Tactic:
ext y