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
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 :
  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)))
⊢ 2 / l' i ≠ 0

Tactic:
simpa using IsAnisotropic.rootForm_root_ne_zero i

Premises used: RootPairing.IsAnisotropic.rootForm_root_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
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 :
  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)))
⊢ 2 / l' i ≠ 0

Tactic:
have aux₁ : 2 / l' i ≠ 0 := by simpa using IsAnisotropic.rootForm_root_ne_zero i
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
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_1 : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j_1
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 :
  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_1) ((P.root : (a : ι) → M) j_1 : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
aux₁ : 2 / l' i ≠ 0
j : ι
ring_nf : (l' i)⁻¹⁻¹ * (l' j)⁻¹ = HMul.hMul (α := R) (↑(l i) : R) (↑(l j) : R)⁻¹
⊢ (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)

Tactic:
ring_nf
-- 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_1 : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j_1
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 :
  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_1) ((P.root : (a : ι) → M) j_1 : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
aux₁ : 2 / l' i ≠ 0
j : ι
⊢ (l' i)⁻¹⁻¹ * (l' j)⁻¹ = HMul.hMul (α := R) (↑(l i) : R) (↑(l j) : R)⁻¹

Tactic:
simp [hll']
-- 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 :
  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)))
aux₁ : 2 / l' i ≠ 0
⊢ ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)

Tactic:
have aux₂ (j : ι) : (2 / l' i)⁻¹ * (2 / l' j) = l i / l j := by ring_nf; simp [hll']
-- 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 :
  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)))
aux₁ : 2 / l' i ≠ 0
aux₂ : ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M)

Tactic:
simp only [smul_add, smul_smul, inv_mul_cancel₀ aux₁, aux₂, one_smul] at contra

Premises used: smul_smul, one_smul, inv_mul_cancel₀, smul_add
-- 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
aux₁ : 2 / l' i ≠ 0
aux₂ : ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
contra :
  (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M)
rw :
  HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M) =
    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)
⊢ (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)

Tactic:
rw [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
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
aux₁ : 2 / l' i ≠ 0
aux₂ : ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
contra :
  (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M)
⊢ HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M) =
    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)

Tactic:
module
-- 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)
obtain :
  ∀ (u : ℚ) (hu : u > 0) (v : ℚ) (hv : v > 0)
    (huv :
      (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)),
    i = j
⊢ i = j

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ : ∃ᵉ (u > (0 : ℚ)) (v > (0 : ℚ)),
      P.root i = u • P.root j + v • P.root k := by
    let l (i : ι) := P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i)
    have hl (i : ι) : 0 < l i := by
      simpa only [l, ← posRootForm_eq] using RootPositiveForm.zero_lt_posForm_apply_root _ _
    refine ⟨l i / l j, by simp [hl], l i / l k, by simp [hl], ?_⟩
    simp only [P.coroot_eq_polarizationEquiv_apply_root, ← map_smul, ← map_add,
      P.PolarizationEquiv.injective.eq_iff] at contra
    let l' (i : ι) := P.RootForm (P.root i) (P.root i)
    have hll' (i : ι) : l i = l' i := P.algebraMap_rootFormIn ℚ _ _
    change (2 / l' i) • P.root i = (2 / l' j) • P.root j + (2 / l' k) • P.root k at contra
    replace contra := congr_arg ((2 / l' i)⁻¹ • ·) contra
    have aux₁ : 2 / l' i ≠ 0 := by simpa using IsAnisotropic.rootForm_root_ne_zero i
    have aux₂ (j : ι) : (2 / l' i)⁻¹ * (2 / l' j) = l i / l j := by ring_nf; simp [hll']
    simp only [smul_add, smul_smul, inv_mul_cancel₀ aux₁, aux₂, one_smul] at contra
    rw [contra]
    module

Premises used: 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
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
huv :
  (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)
l : ι
hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)
rwa :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) l : M)
rwa₁ :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (toAddSubmonoid (span ℕ ((⇑P.root : (a : ι) → M) '' s)))
    ((P.root : (a : ι) → M) l : M)
rwa₂ :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) l : M)
rwa₃ :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)}))
    ((P.root : (a : ι) → M) l : M)
rwa₄ : LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) l : M) : ℚ)
rwa₅ rwa₆ rwa₇ rwa₈ : 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)

Tactic:
rwa [← Submodule.mem_span_iff_of_fintype, ← mem_toAddSubmonoid, span_nat_eq_addSubmonoidClosure,
      AddSubmonoid.closure_image_isAddIndecomposable_baseOf,
      AddSubmonoid.mem_closure_image_pos_iff P.root f _ (P.ne_zero _), hfg]

Premises used: RootPairing.ne_zero, AddSubmonoid.closure_image_isAddIndecomposable_baseOf, Submodule.mem_span_iff_of_fintype, AddSubmonoid.mem_closure_image_pos_iff, Submodule.mem_toAddSubmonoid, RootPairing.root, Submodule.span_nat_eq_addSubmonoidClosure, DFunLike.coe