awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this_2 : IsReflexive R N
this : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
rw :
  finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))) =
    finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))) =
    finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this_2 : IsReflexive R N
this : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ finrank.{u_2, u_3} R
      ↥(Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))) =
    finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
apply LinearEquiv.finrank_map_eq

Premises used: LinearEquiv.finrank_map_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
suffices : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
suffices finrank R (LinearMap.ker P.RootForm) = finrank R (P.corootSpan R).dualAnnihilator by
    refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm
    rw [this]
    apply LinearEquiv.finrank_map_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) = finrank R N

Tactic:
have aux0 := Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R)
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux0 : finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) = finrank R N
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R M

Tactic:
have aux1 := Submodule.finrank_add_eq_of_isCompl P.isCompl_rootSpan_ker_rootForm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux0 : finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) = finrank R N
aux1 : finrank.{u_2, u_3} R ↥(P.rootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R M
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R N

Tactic:
rw [← P.finrank_corootSpan_eq', P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq] at aux1

Premises used: RootPairing.finrank_corootSpan_eq', RootPairing.toLinearMap, Subspace.dual_finrank_eq, LinearEquiv.finrank_eq, LinearMap.toPerfPair
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
aux0 : finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R)) = finrank R N
aux1 : finrank.{u_2, u_4} R ↥(P.corootSpan R) + finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R N
⊢ finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ LinearMap.ker P.CorootForm =
    Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))

Tactic:
P.flip.ker_rootForm_eq_dualAnnihilator

Premises used: RootPairing.flip, RootPairing.CorootForm, RootPairing.ker_rootForm_eq_dualAnnihilator
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ IsCompl (P.rootSpan R)
    (Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)))

Tactic:
simpa only [ker_rootForm_eq_dualAnnihilator] using P.isCompl_rootSpan_ker_rootForm

Premises used: RootPairing.isCompl_rootSpan_ker_rootForm, RootPairing.ker_rootForm_eq_dualAnnihilator
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ IsCompl (P.corootSpan R)
    (Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R)))

Tactic:
simpa only [ker_corootForm_eq_dualAnnihilator] using P.isCompl_corootSpan_ker_corootForm

Premises used: RootPairing.isCompl_corootSpan_ker_corootForm, RootPairing.ker_corootForm_eq_dualAnnihilator
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ LinearMap.Nondegenerate (M₁ := ↥(P.rootSpan R)) (P.RootForm.restrict (P.rootSpan R))

Tactic:
P.rootForm_symmetric.nondegenerate_restrict_of_isCompl_ker P.isCompl_rootSpan_ker_rootForm

Premises used: RootPairing.isCompl_rootSpan_ker_rootForm, LinearMap.BilinForm.restrict, LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker, RootPairing.rootForm_symmetric
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
rw : P.RootForm.orthogonal (P.rootSpan R) = P.RootForm.orthogonal ⊤
⊢ P.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm

Tactic:
rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]

Premises used: LinearMap.IsSymm.isRefl, LinearMap.BilinForm.orthogonal_top_eq_ker, RootPairing.rootForm_symmetric
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x : M
⊢ x ∈ P.RootForm.orthogonal ⊤ → x ∈ P.RootForm.orthogonal (P.rootSpan R)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
refine : P.RootForm.orthogonal (P.rootSpan R) ≤ P.RootForm.orthogonal ⊤
⊢ P.RootForm.orthogonal (P.rootSpan R) = P.RootForm.orthogonal ⊤

Tactic:
refine le_antisymm ?_ (by intro; simp_all)

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x : M
hx : x ∈ P.RootForm.orthogonal (P.rootSpan R)
y : M
⊢ ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
simp only [LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.IsOrtho] at hx ⊢

Premises used: LinearMap.BilinForm.IsOrtho, LinearMap.BilinForm.mem_orthogonal_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x y : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
rw : Membership.mem (γ := Submodule R M) ⊤ y
⊢ ∃ (u : M), Membership.mem (γ := Submodule R M) (P.rootSpan R) u ∧ ∃ v ∈ LinearMap.ker P.RootForm, u + v = y

Tactic:
rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]

Premises used: IsCompl.sup_eq_top, RootPairing.isCompl_rootSpan_ker_rootForm, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x y : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) ⊤ y

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x y : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) ⊤ y

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x y : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
obtain :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (P.rootSpan R) u) (v : M) (hv : v ∈ LinearMap.ker P.RootForm),
    LinearMap.IsOrtho P.RootForm (u + v) x
⊢ LinearMap.IsOrtho P.RootForm y x

Tactic:
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan R) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
    rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top

Premises used: RootPairing.RootForm, LinearMap.ker, RootPairing.rootSpan, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
u : M
hu : Membership.mem (γ := Submodule R M) (P.rootSpan R) u
v : M
hv : v ∈ LinearMap.ker P.RootForm
⊢ Eq (α := M →ₗ[R] R) ((P.RootForm : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
simp only [LinearMap.mem_ker] at hv

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
x : M
hx :
  ∀ (n : M),
    Membership.mem (γ := Submodule R M) (P.rootSpan R) n →
      Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
u : M
hu : Membership.mem (γ := Submodule R M) (P.rootSpan R) u
v : M
hv : Eq (α := M →ₗ[R] R) ((P.RootForm : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ LinearMap.IsOrtho P.RootForm (u + v) x

Tactic:
simp [LinearMap.IsOrtho, hx _ hu, hv]

Premises used: LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
⊢ P.CorootForm.orthogonal (P.corootSpan R) = LinearMap.ker P.CorootForm

Tactic:
P.flip.orthogonal_rootSpan_eq

Premises used: RootPairing.flip, RootPairing.CorootForm, RootPairing.orthogonal_rootSpan_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤ ↔ Eq (α := Submodule R N) (P.corootSpan R) ⊤

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
refine_1 : ∀ (h : Eq (α := Submodule R M) (P.rootSpan R) ⊤), Eq (α := Submodule R N) (P.corootSpan R) ⊤
refine_2 : ∀ (h : Eq (α := Submodule R N) (P.corootSpan R) ⊤), Eq (α := Submodule R M) (P.rootSpan R) ⊤
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤ ↔ Eq (α := Submodule R N) (P.corootSpan R) ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
h : Eq (α := Submodule R M) (P.rootSpan R) ⊤
refine_1 : finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
⊢ Eq (α := Submodule R N) (P.corootSpan R) ⊤

Tactic:
apply Submodule.eq_top_of_finrank_eq

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
h : Eq (α := Submodule R N) (P.corootSpan R) ⊤
refine_2 : finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤

Tactic:
apply Submodule.eq_top_of_finrank_eq

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
h : Eq (α := Submodule R M) (P.rootSpan R) ⊤
refine_1 : finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R N
refine_1₁ : finrank.{u_2, u_3} R ↥⊤ = finrank R N
refine_1₂ : finrank R M = finrank R N
refine_1₃ : finrank R (Dual R N) = finrank R N
refine_1₄ refine_1₅ : finrank R N = finrank R N
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N

Tactic:
rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]

Premises used: RootPairing.finrank_corootSpan_eq', RootPairing.toLinearMap, Subspace.dual_finrank_eq, LinearEquiv.finrank_eq, finrank_top, LinearMap.toPerfPair
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
this_1 : IsReflexive R M
this : IsReflexive R N
h : Eq (α := Submodule R N) (P.corootSpan R) ⊤
refine_2 : finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R M
refine_2₁ : finrank.{u_2, u_4} R ↥⊤ = finrank R M
refine_2₂ : finrank R N = finrank R M
refine_2₃ : finrank R N = finrank R (Dual R N)
refine_2₄ refine_2₅ : finrank R N = finrank R N
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M

Tactic:
rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]

Premises used: RootPairing.finrank_corootSpan_eq', RootPairing.toLinearMap, Subspace.dual_finrank_eq, LinearEquiv.finrank_eq, finrank_top, LinearMap.toPerfPair
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
simp :
  (↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := ⋯) (re₂₁ := ⋯)
          ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) ⋯ ⋯) P.flip.toPerfPair.symm) :
      M →ₗ[R] N) =
    P.Polarization
⊢ (↑P.PolarizationEquiv : M →ₗ[R] N) = P.Polarization

Tactic:
simp only [PolarizationEquiv, LinearMap.BilinForm.toDual, RootPairing.toInvariantForm_form,
    ← P.flip_comp_polarization_eq_rootForm, RootPairing.flip_toLinearMap]

Premises used: RootPairing.flip_comp_polarization_eq_rootForm, RootPairing.PolarizationEquiv, LinearMap.BilinForm.toDual, RootPairing.flip_toLinearMap, RootPairing.toInvariantForm_form
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
h :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := N)
      (((↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := ⋯) (re₂₁ := ⋯)
                  ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) ⋯ ⋯) P.flip.toPerfPair.symm) :
              M →ₗ[R] N) :
            (a : M) → N)
          m :
        N)
      ((P.Polarization : (a : M) → N) m : N)
⊢ (↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := ⋯) (re₂₁ := ⋯)
          ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) ⋯ ⋯) P.flip.toPerfPair.symm) :
      M →ₗ[R] N) =
    P.Polarization

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
m : M
e : N ≃ₗ[R] Dual R M := P.flip.toPerfPair
h :
  Eq.{u_4 + 1} (α := N)
    ((e.symm : (a : Dual R M) → N) ((e : (a : N) → Dual R M) ((P.Polarization : (a : M) → N) m) : Dual R M) : N)
    ((P.Polarization : (a : M) → N) m : N)
⊢ Eq.{u_4 + 1} (α := N)
    (((↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := ⋯) (re₂₁ := ⋯)
                ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) ⋯ ⋯) P.flip.toPerfPair.symm) :
            M →ₗ[R] N) :
          (a : M) → N)
        m :
      N)
    ((P.Polarization : (a : M) → N) m : N)

Tactic:
change e.symm (e _) = _

Premises used: LinearEquiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
m : M
e : N ≃ₗ[R] Dual R M := P.flip.toPerfPair
⊢ Eq.{u_4 + 1} (α := N)
    ((e.symm : (a : Dual R M) → N) ((e : (a : N) → Dual R M) ((P.Polarization : (a : M) → N) m) : Dual R M) : N)
    ((P.Polarization : (a : M) → N) m : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
m : M
⊢ Eq.{u_4 + 1} (α := N) ((P.PolarizationEquiv : (a : M) → N) m : N) ((P.Polarization : (a : M) → N) m : N)

Tactic:
congr($P.polarizationEquiv_toLinearMap m)

Premises used: congrArg, id, RootPairing.polarizationEquiv_toLinearMap, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
i : ι
⊢ Ne.{u_2 + 1} (α := 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)
    (0 : R)

Tactic:
have h₀ := IsAnisotropic.rootForm_root_ne_zero (P := P) i