awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
Tactic: have h_span : span ℚ (range v) = ⊤ := by
    suffices span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ)) by
      rw [this, eq_top_iff, ← (P.rootSpan ℚ).subtype.map_le_map_iff' (by simp), map_span,
        ← image_univ, ← image_comp]
      simp
    apply le_antisymm (span_mono fun x i ↦ by aesop) (span_le.mpr ?_)
    rintro - ⟨i, rfl⟩
    suffices (P.rootSpanMem ℚ i : M) ∈ span ℚ (P.root '' baseOf P.root f) by
      rw [← (injective_subtype (P.rootSpan ℚ)).mem_set_image, ← map_coe, SetLike.mem_coe, map_span,
        ← image_univ, ← image_comp]
      convert! this
      aesop
    rw [← span_span_of_tower ℤ, ← Submodule.coe_toAddSubgroup, span_int_eq_addSubgroupClosure,
      AddSubgroup.closure_image_isAddIndecomposable_baseOf P.root (by simp) f (by simpa)]
    exact subset_span <| AddSubgroup.subset_closure <| by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
⊢ Basis.{u_1, 0, u_3} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) ℚ ↥(P.rootSpan ℚ)
have this₁ : LinearIndependent ℚ v
Tactic: replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
this : LinearIndependent ℚ v
⊢ LE.le (α := Submodule ℚ ↥(P.rootSpan ℚ)) ⊤ (span ℚ (range v))
have rw : LE.le.{u_3} (α := Submodule ℚ ↥(P.rootSpan ℚ)) ⊤ ⊤
Tactic: rw [h_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
b : Basis.{u_1, 0, u_3} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) ℚ ↥(P.rootSpan ℚ) :=
  have this : LinearIndependent ℚ v := ⋯;
  Basis.mk this ⋯
⊢ Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
have rw : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{0, u_3} ℚ ↥(P.rootSpan ℚ)
Tactic: rw [← RootPairing.finrank_rootSpanIn ℚ P, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
b : Basis.{u_1, 0, u_3} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) ℚ ↥(P.rootSpan ℚ) :=
  have this : LinearIndependent ℚ v := ⋯;
  Basis.mk this ⋯
rw : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{0, u_3} ℚ ↥(P.rootSpan ℚ)
⊢ Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
have rw₁ : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
  Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
Tactic: rw [← RootPairing.finrank_rootSpanIn ℚ P, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
Tactic: have h_card : Nat.card (baseOf P.root f) = finrank R M := by
    let b : Basis (baseOf P.root f) ℚ (P.rootSpan ℚ) := by
      replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf
      exact Basis.mk this (by rw [h_span])
    rw [← RootPairing.finrank_rootSpanIn ℚ P, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
⊢ Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
have rw : Eq (α := Submodule R M) (span R (↑(map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤) : Set M)) ⊤
Tactic: rw [range_comp, ← span_span_of_tower ℚ, span_image, h_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_span : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have h_span₁ : Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
Tactic: replace h_span : span R (range <| (P.rootSpan ℚ).subtype ∘ v) = ⊤ := by
    rw [range_comp, ← span_span_of_tower ℚ, span_image, h_span]
    simp
Cleared hypotheses: h_span
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
  Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
rw :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw₁ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
  finrank.{u_2, u_3} R ↥(span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)))
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
rw :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
rw₁ :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    finrank.{u_2, u_3} R ↥(span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)))
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw₂ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{u_2, u_3} R ↥⊤
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
rw :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
rw₁ :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    finrank.{u_2, u_3} R ↥(span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)))
rw₂ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{u_2, u_3} R ↥⊤
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw₃ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
rw :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
rw₁ :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    finrank.{u_2, u_3} R ↥(span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)))
rw₂ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{u_2, u_3} R ↥⊤
rw₃ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw₄ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
  Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
h_card : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
h_span :
  Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤
rw :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Set.finrank R (M := M) (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))
rw₁ :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    finrank.{u_2, u_3} R ↥(span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)))
rw₂ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank.{u_2, u_3} R ↥⊤
rw₃ : Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M
rw₄ :
  Fintype.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
    Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
⊢ LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
have rw₅ : Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) =
  Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
Tactic: rw [linearIndependent_iff_card_eq_finrank_span, Set.finrank, h_span, finrank_top, ← h_card,
    Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
have hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
Tactic: have hf' (i : ι) : f (P.root i) ≠ 0 := AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure
      P.root f s (by aesop) i (P.ne_zero i) (by simp) (hsp i)