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_1 :
  (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)
contra : ¬GT.gt (α := ℚ) (↑(a ri) : ℚ) 0
⊢ a ri = 0

Tactic:
simpa using contra
-- 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_1 :
  (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)
contra : ¬GT.gt (α := ℚ) (↑(a ri) : ℚ) 0
⊢ a ri = 0

Tactic:
replace contra : a ri = 0 := by simpa using contra
-- 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_1 :
  (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)
contra : a ri = 0
⊢ False

Tactic:
simp [contra, P.ne_zero j] at this

Premises used: RootPairing.ne_zero
-- 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
suffices : (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:
suffices P.root j = (a ri : ℚ) • P.root i by
      refine ⟨a ri, ?_, this⟩
      by_contra contra
      replace contra : a ri = 0 := by simpa using contra
      simp [contra, P.ne_zero j] at 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
x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)
hx : x ≠ ri
⊢ u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ) = 0

Tactic:
simpa [hx] using congr($huv x)
-- 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
x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)
hx : x ≠ ri
⊢ u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ) = 0

Tactic:
replace huv : u * ↑(a x) + v * ↑(b x) = 0 := by simpa [hx] using congr($huv x)
-- 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) ⋯
x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)
hx : x ≠ ri
huv : u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ) = 0
this : u * (↑(a x) : ℚ) = 0
⊢ a x = 0

Tactic:
simpa [hu.ne'] using this

Premises used: LT.lt.ne'
-- 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) ⋯
x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)
hx : x ≠ ri
huv : u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ) = 0
suffices : u * (↑(a x) : ℚ) = 0
⊢ a x = 0

Tactic:
suffices u * (a x) = 0 by simpa [hu.ne'] using 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) ⋯
x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)
hx : x ≠ ri
huv : u * (↑(a x) : ℚ) + v * (↑(b x) : ℚ) = 0
⊢ 0 ≤ u * (↑(a x) : ℚ)

Tactic:
positivity