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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  Eq.{u_3 + 1} (α := M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), (u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ)) • (↑x : M))
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
      HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
        (↑x : M))
aux :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
        HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
          (↑x : M) :
      M)
rw : LinearIndepOn.{u_1, 0, u_3} ℚ (M := M) (⇑P.root : (a : ι) → M) s
⊢ LinearIndepOn.{u_3, 0, u_3} (ι := M) ℚ id ((⇑P.root : (a : ι) → M) '' s)

Tactic:
rw [← linearIndepOn_iff_image P.root.injective.injOn]

Premises used: Function.Injective.injOn, RootPairing.root, Function.Embedding.injective, linearIndepOn_iff_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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  Eq.{u_3 + 1} (α := M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), (u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ)) • (↑x : M))
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
      HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
        (↑x : M))
aux :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
        HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
          (↑x : M) :
      M)
⊢ LinearIndepOn.{u_1, 0, u_3} ℚ (M := M) (⇑P.root : (a : ι) → M) s

Tactic:
(linearIndepOn_root_baseOf P f hf).restrict_scalars' ℚ

Premises used: Rat, LinearIndependent.restrict_scalars', RootPairing.linearIndepOn_root_baseOf, LinearIndepOn
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  Eq.{u_3 + 1} (α := M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), (u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ)) • (↑x : M))
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
      HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
        (↑x : M))
aux :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
        HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
          (↑x : M) :
      M)
⊢ LinearIndepOn.{u_1, 0, u_3} ℚ (M := M) (⇑P.root : (a : ι) → M) s

Tactic:
exact (linearIndepOn_root_baseOf P f hf).restrict_scalars' ℚ

Premises used: Rat, LinearIndependent.restrict_scalars', RootPairing.linearIndepOn_root_baseOf
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  Eq.{u_3 + 1} (α := M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), (u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ)) • (↑x : M))
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
      HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
        (↑x : M))
aux :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
        HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
          (↑x : M) :
      M)
⊢ LinearIndepOn.{u_3, 0, u_3} (ι := M) ℚ id ((⇑P.root : (a : ι) → M) '' s)

Tactic:
have hli : LinearIndepOn ℚ id (P.root '' s) := by
      rw [← linearIndepOn_iff_image P.root.injective.injOn]
      exact (linearIndepOn_root_baseOf P f hf).restrict_scalars' ℚ
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  Eq.{u_3 + 1} (α := M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), (u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ)) • (↑x : M))
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
      HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
        (↑x : M))
aux :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3),
        HSMul.hSMul (α := ℚ) (Pi.single (M := fun (x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1 x : ℚ)
          (↑x : M) :
      M)
hli : LinearIndepOn.{u_3, 0, u_3} (ι := M) ℚ id ((⇑P.root : (a : ι) → M) '' s)
⊢ LinearIndependent.{u_3, 0, u_3} (ι := { x : M // Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x }) ℚ
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x))

Tactic:
rw [← linearIndependent_subtype_iff] at hli

Premises used: linearIndependent_subtype_iff
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
this : (P.root : (a : ι) → M) j = HSMul.hSMul (α := ℚ) (β := M) (↑(a ri) : ℚ) ((P.root : (a : ι) → M) i : M)
⊢ ∃ q > 0, (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)

Tactic:
⟨a ri, ?_, this⟩

Premises used: Nat.cast, And.intro, Exists.intro
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
this : (P.root : (a : ι) → M) j = HSMul.hSMul (α := ℚ) (β := M) (↑(a ri) : ℚ) ((P.root : (a : ι) → M) i : M)
refine : GT.gt (α := ℚ) (↑(a ri) : ℚ) 0
⊢ ∃ q > 0, (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)

Tactic:
refine ⟨a ri, ?_, 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
this : (P.root : (a : ι) → M) j = HSMul.hSMul (α := ℚ) (β := M) (↑(a ri) : ℚ) ((P.root : (a : ι) → M) i : M)
by_contra : ∀ (contra : ¬GT.gt (α := ℚ) (↑(a ri) : ℚ) 0), False
⊢ GT.gt (α := ℚ) (↑(a ri) : ℚ) 0

Tactic:
by_contra contra