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 : InvolutiveNeg ι := P.indexNeg
have :
  ∀ (this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)),
    LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)
⊢ LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)

Tactic:
have : Fintype (baseOf P.root f) := Fintype.ofFinite _
-- 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 : ι)
change : LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
⊢ LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)

Tactic:
change LinearIndependent R ((P.rootSpan ℚ).subtype ∘ v)

Premises used: Rat, Function.comp, RootPairing.rootSpan, LinearIndependent, Submodule.subtype, DFunLike.coe
-- 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_2 : 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 : ι)
this : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (LinearMap.ker (Submodule.subtype (P.rootSpan ℚ))) ⊥

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_2 : 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 : ι)
this : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
rw :
  LE.le (α := Submodule ℚ M) (map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤)
    (span ℚ
      (comp (β := ↥(P.rootSpan ℚ)) (⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M)
          (P.rootSpanMem ℚ) ''
        univ))
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤

Tactic:
rw [this, eq_top_iff, ← (P.rootSpan ℚ).subtype.map_le_map_iff' (by simp), map_span,
        ← image_univ, ← image_comp]

Premises used: Set.image_univ, eq_top_iff, LinearMap.map_le_map_iff', Set.image_comp, Submodule.map_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
this_2 : 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 : ι)
this : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
⊢ LE.le (α := Submodule ℚ M) (map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤)
    (span ℚ
      (comp (β := ↥(P.rootSpan ℚ)) (⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M)
          (P.rootSpanMem ℚ) ''
        univ))

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 : ι)
suffices : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤

Tactic:
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
-- 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 : ι)
x : ↥(P.rootSpan ℚ)
i : x ∈ range v
⊢ Membership.mem (γ := Set ↥(P.rootSpan ℚ)) (range (P.rootSpanMem ℚ)) x

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
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 : ι)
apply : range (P.rootSpanMem ℚ) ⊆ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))

Tactic:
apply le_antisymm (span_mono fun x i ↦ by aesop) (span_le.mpr ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.span_mono, Submodule.span_le
-- 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_2 : 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 : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
rw :
  Membership.mem (α := M) (γ := Submodule ℚ M)
    (span ℚ ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ))
    ((Submodule.subtype (P.rootSpan ℚ) : (a : ↥(P.rootSpan ℚ)) → M) (P.rootSpanMem ℚ i) : M)
⊢ P.rootSpanMem ℚ i ∈ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))

Tactic:
rw [← (injective_subtype (P.rootSpan ℚ)).mem_set_image, ← map_coe, SetLike.mem_coe, map_span,
        ← image_univ, ← image_comp]

Premises used: Set.image_univ, Rat, Submodule.injective_subtype, RootPairing.rootSpan, SetLike.mem_coe, Set.image_comp, Submodule.map_span, Submodule.map_coe, Function.Injective.mem_set_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_2 : 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 : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)

Tactic:
this
-- 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_2 : 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 : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
h :
  Eq (α := Set M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ)
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f))
⊢ Membership.mem (α := M) (γ := Submodule ℚ M)
    (span ℚ ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ))
    ((Submodule.subtype (P.rootSpan ℚ) : (a : ↥(P.rootSpan ℚ)) → M) (P.rootSpanMem ℚ i) : M)

Tactic:
convert! this
-- 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_2 : 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 : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ Eq (α := Set M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ)
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f))

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
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 : ι)
i : ι
suffices :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ P.rootSpanMem ℚ i ∈ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))

Tactic:
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
-- 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 : ι)
i : ι
⊢ ∀ (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
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 : ι)
i : ι
⊢ ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)

Tactic:
simpa
-- 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 : ι)
i : ι
rw :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (↑(AddSubgroup.closure (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) : Set M))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)

Tactic:
rw [← span_span_of_tower ℤ, ← Submodule.coe_toAddSubgroup, span_int_eq_addSubgroupClosure,
      AddSubgroup.closure_image_isAddIndecomposable_baseOf P.root (by simp) f (by simpa)]

Premises used: Submodule.span_span_of_tower, Int, AddSubgroup.closure_image_isAddIndecomposable_baseOf, Submodule.span_int_eq_addSubgroupClosure, RootPairing.root, DFunLike.coe, Submodule.coe_toAddSubgroup
-- 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 : ι)
i : ι
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑(P.rootSpanMem ℚ 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
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 : ι)
i : ι
⊢ Membership.mem (γ := Submodule ℚ M)
    (span ℚ (↑(AddSubgroup.closure (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) : Set M))
    (↑(P.rootSpanMem ℚ i) : M)

Tactic:
exact subset_span <| AddSubgroup.subset_closure <| by simp

Premises used: Submodule.subset_span, AddSubgroup.subset_closure
-- 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 : ι)
⊢ 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
-- 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)) ⊤
⊢ LinearIndependent ℚ v

Tactic:
replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf