awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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 : IsReflexive R M
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))
have this₁ : IsReflexive R N
Tactic: have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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))
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))
have refine : 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: refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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.{u_2, u_3} R ↥(LinearMap.ker P.RootForm)
have 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))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ LinearMap.ker P.RootForm =
    Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R))
have suffices : finrank.{u_2, u_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have aux0 : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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 ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have aux1 : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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_3} R ↥(LinearMap.ker P.RootForm) = finrank R ↥(Submodule.dualAnnihilator (P.corootSpan R))
have aux1₁ : 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
Cleared hypotheses: aux1
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm
have rw : P.RootForm.orthogonal (P.rootSpan R) = P.RootForm.orthogonal ⊤
Tactic: rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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.RootForm.orthogonal (P.rootSpan R) = P.RootForm.orthogonal ⊤
have refine : P.RootForm.orthogonal (P.rootSpan R) ≤ P.RootForm.orthogonal ⊤
Tactic: refine le_antisymm ?_ (by intro; simp_all)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
⊢ LinearMap.IsOrtho P.RootForm y x
have 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)
Tactic: simp only [LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.IsOrtho] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
⊢ ∃ (u : M), Membership.mem (γ := Submodule R M) (P.rootSpan R) u ∧ ∃ v ∈ LinearMap.ker P.RootForm, u + v = y
have rw : Membership.mem (γ := Submodule R M) ⊤ y
Tactic: rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
⊢ LinearMap.IsOrtho P.RootForm y x
have 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
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
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
⊢ LinearMap.IsOrtho P.RootForm (u + v) x
have hv₁ : 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
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤ ↔ Eq (α := Submodule R N) (P.corootSpan R) ⊤
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
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 : IsReflexive R M
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤ ↔ Eq (α := Submodule R N) (P.corootSpan R) ⊤
have this₁ : IsReflexive R N
Tactic: have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
have refine_1 : ∀ (h : Eq (α := Submodule R M) (P.rootSpan R) ⊤), Eq (α := Submodule R N) (P.corootSpan R) ⊤
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤ ↔ Eq (α := Submodule R N) (P.corootSpan R) ⊤
have refine_2 : ∀ (h : Eq (α := Submodule R N) (P.corootSpan R) ⊤), Eq (α := Submodule R M) (P.rootSpan R) ⊤
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
⊢ Eq (α := Submodule R N) (P.corootSpan R) ⊤
have refine_1 : finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
Tactic: apply Submodule.eq_top_of_finrank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
⊢ Eq (α := Submodule R M) (P.rootSpan R) ⊤
have refine_2 : finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
Tactic: apply Submodule.eq_top_of_finrank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
have refine_1 : finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R N
Tactic: rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
have refine_1₁ : finrank.{u_2, u_3} R ↥⊤ = finrank R N
Tactic: rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
have refine_1₂ : finrank R M = finrank R N
Tactic: rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
have refine_1₃ : finrank R (Dual R N) = finrank R N
Tactic: rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R N
have refine_1₄ : finrank R N = finrank R N
Tactic: rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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) ⊤
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
have refine_2 : finrank.{u_2, u_4} R ↥(P.corootSpan R) = finrank R M
Tactic: rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
have refine_2₁ : finrank.{u_2, u_4} R ↥⊤ = finrank R M
Tactic: rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
have refine_2₂ : finrank R N = finrank R M
Tactic: rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
have refine_2₃ : finrank R N = finrank R (Dual R N)
Tactic: rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
⊢ finrank.{u_2, u_3} R ↥(P.rootSpan R) = finrank R M
have refine_2₄ : finrank R N = finrank R N
Tactic: rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ (↑P.PolarizationEquiv : M →ₗ[R] N) = P.Polarization
have simp : (↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := sorry) (re₂₁ := sorry)
        ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) sorry sorry) P.flip.toPerfPair.symm) :
    M →ₗ[R] N) =
  P.Polarization
Tactic: simp only [PolarizationEquiv, LinearMap.BilinForm.toDual, RootPairing.toInvariantForm_form,
    ← P.flip_comp_polarization_eq_rootForm, RootPairing.flip_toLinearMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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
⊢ (↑(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
have h : ∀ (m : M),
  Eq.{u_4 + 1} (α := N)
    (((↑(LinearEquiv.trans (σ₁₂ := RingHom.id R) (σ₂₁ := RingHom.id R) (re₁₂ := sorry) (re₂₁ := sorry)
                ((P.flip ∘ₗ P.Polarization).linearEquivOfInjective (K := R) sorry sorry) P.flip.toPerfPair.symm) :
            M →ₗ[R] N) :
          (a : M) → N)
        m :
      N)
    ((P.Polarization : (a : M) → N) m : N)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
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)
    (((↑(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)
have 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)
Tactic: change e.symm (e _) = _