awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
rw rw₁ : LE.le.{u_3} (α := Submodule ℚ ↥(P.rootSpan ℚ)) ⊤ ⊤
⊢ LE.le (α := Submodule ℚ ↥(P.rootSpan ℚ)) ⊤ (span ℚ (range v))

Tactic:
rw [h_span]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
⊢ Basis.{u_1, 0, u_3} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) ℚ ↥(P.rootSpan ℚ)

Tactic:
exact Basis.mk this (by rw [h_span])

Premises used: Module.Basis.mk
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 ℚ)
rw₁ 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)
⊢ Nat.card.{u_1} (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1) = finrank R M

Tactic:
rw [← RootPairing.finrank_rootSpanIn ℚ P, finrank_eq_nat_card_basis b]

Premises used: Rat, Module.finrank_eq_nat_card_basis, RootPairing.finrank_rootSpanIn
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)) ⊤
⊢ 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]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
rw : Eq (α := Submodule R M) (span R (↑(map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤) : Set M)) ⊤
⊢ Eq (α := Submodule R M) (span R (range ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v))) ⊤

Tactic:
rw [range_comp, ← span_span_of_tower ℚ, span_image, h_span]

Premises used: Set.range_comp, Submodule.span_span_of_tower, Rat, Submodule.span_image
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 (↑(map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤) : Set M)) ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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))) ⊤

Tactic:
replace h_span : span R (range <| (P.rootSpan ℚ).subtype ∘ v) = ⊤ := by
    rw [range_comp, ← span_span_of_tower ℚ, span_image, h_span]
    simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
rw₅ 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)
⊢ LinearIndependent R (M := M) ((⇑(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]

Premises used: Set.finrank, finrank_top, Fintype.card_eq_nat_card, linearIndependent_iff_card_eq_finrank_span
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
i : ι
⊢ ∀ i ∈ s, LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) (-i) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
⊢ ∀ (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)
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) (-i) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
⊢ ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        (-(P.root : (a : ι) → M) i : M)

Tactic:
have aux (i : ι) := mem_or_neg_mem_closure_baseOf P.root f i (hf' i) (by simp)
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        (-(P.root : (a : ι) → M) i : M)
rw : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = finrank R M
rw₁ rw₂ : finrank R M = finrank R M
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard

Tactic:
rw [P.ncard_eq_finrank_of_linearIndepOn_of hli hsp, P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux]

Premises used: RootPairing.linearIndepOn_root_baseOf, RootPairing.ncard_eq_finrank_of_linearIndepOn_of
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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

Tactic:
have h_card : (baseOf P.root f).ncard = s.ncard := by
    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)
    have aux (i : ι) := mem_or_neg_mem_closure_baseOf P.root f i (hf' i) (by simp)
    rw [P.ncard_eq_finrank_of_linearIndepOn_of hli hsp, P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
this : s ⊆ baseOf (⇑P.root : (a : ι) → M) f
rw rw₁ : s.ncard ≤ s.ncard
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) ≤ s.ncard

Tactic:
rw [h_card]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
suffices : s ⊆ baseOf (⇑P.root : (a : ι) → M) f
⊢ s = baseOf (⇑P.root : (a : ι) → M) f

Tactic:
suffices s ⊆ baseOf P.root f from eq_of_subset_of_ncard_le this (by rw [h_card])
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
inl :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
inr :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)

Tactic:
rcases hsp i with hi | hi