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
refine :
  ∀ (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)),
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)
⊢ Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)

Tactic:
refine fun i hi ↦ ⟨by obtain ⟨hi, -⟩ := hi; aesop, fun j hj k hk 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 :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
this : i = j
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)

Tactic:
grind
-- 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)
suffices : i = j
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)

Tactic:
suffices i = j by grind
-- 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_1 : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i_1
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_1 =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
i : ι
⊢ 0 < l i

Tactic:
simpa only [l, ← posRootForm_eq] using RootPositiveForm.zero_lt_posForm_apply_root _ _

Premises used: Set.mem_range_self, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, RootPairing.posRootForm_eq, Submodule.subset_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
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)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
⊢ ∀ (i : ι), 0 < l i

Tactic:
have hl (i : ι) : 0 < l i := by
      simpa only [l, ← posRootForm_eq] using RootPositiveForm.zero_lt_posForm_apply_root _ _
-- 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)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ l i / l j > 0

Tactic:
simp [hl]
-- 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)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ l i / l k > 0

Tactic:
simp [hl]
-- 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)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
refine :
  (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
⊢ ∃ u > 0,
    ∃ v > 0,
      (P.root : (a : ι) → M) i =
        HSMul.hSMul (β := M) u ((P.root : (a : ι) → M) j : M) + HSMul.hSMul (β := M) v ((P.root : (a : ι) → M) k : M)

Tactic:
refine ⟨l i / l j, by simp [hl], l i / l k, by simp [hl], ?_⟩
-- 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)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R))
        ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R))
        ((P.root : (a : ι) → M) k : M)

Tactic:
simp only [P.coroot_eq_polarizationEquiv_apply_root, ← map_smul, ← map_add,
      P.PolarizationEquiv.injective.eq_iff] at contra

Premises used: RootPairing.coroot_eq_polarizationEquiv_apply_root, RootPairing.PolarizationEquiv, Function.Injective.eq_iff, map_add, LinearEquiv.injective, map_smul
-- 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
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
contra :
  HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R))
        ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R))
        ((P.root : (a : ι) → M) k : M)
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
⊢ ∀ (i : ι), (↑(l i) : R) = l' i

Tactic:
have hll' (i : ι) : l i = l' i := P.algebraMap_rootFormIn ℚ _ _
-- 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
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
contra :
  HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R))
        ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R))
        ((P.root : (a : ι) → M) k : M)
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
⊢ HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)

Tactic:
change (2 / l' i) • P.root i = (2 / l' j) • P.root j + (2 / l' k) • P.root k at contra

Premises used: HDiv.hDiv, RootPairing.root, OfNat.ofNat, 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
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
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)
⊢ Eq.{u_3 + 1} (α := M)
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
      (HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))

Tactic:
replace contra := congr_arg ((2 / l' i)⁻¹ • ·) contra