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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
i : ι
obtain :
  ∀ (q : ℚ) (hq₀ : 0 < q)
    (hq :
      (↑q : R) =
        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)),
    Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
⊢ Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)

Tactic:
obtain ⟨q, hq₀, hq⟩ := aux 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
i : ι
q : ℚ
hq₀ : 0 < q
hq :
  (↑q : R) =
    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)
⊢ Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)

Tactic:
simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀.ne', hf₀ i]

Premises used: RootPairing.coroot_eq_polarizationEquiv_apply_root, LT.lt.ne', Rat.cast_smul_eq_qsmul
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
⊢ ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)

Tactic:
have hg₀ (i : ι) : g (P.coroot i) ≠ 0 := by
    obtain ⟨q, hq₀, hq⟩ := aux i
    simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀.ne', hf₀ 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
i : ι
obtain :
  ∀ (q : ℚ) (hq₀ : 0 < q)
    (hq :
      (↑q : R) =
        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)),
    LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
⊢ LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)

Tactic:
obtain ⟨q, hq₀, hq⟩ := aux 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
i : ι
q : ℚ
hq₀ : 0 < q
hq :
  (↑q : R) =
    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)
⊢ LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)

Tactic:
simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀]

Premises used: RootPairing.coroot_eq_polarizationEquiv_apply_root, Rat.cast_smul_eq_qsmul
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
⊢ ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)

Tactic:
have hg (i : ι) : 0 < g (P.coroot i) ↔ 0 < f (P.root i) := by
    obtain ⟨q, hq₀, hq⟩ := aux i
    simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀]
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
hg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
rw :
  Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
      (AddSubmonoid.closure
        (image.{u_1, u_4} (α := ι) (⇑P.coroot : (a : ι) → N) (baseOf (⇑P.coroot : (a : ι) → N) (↑g : N →+ ℚ))))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
      (AddSubmonoid.closure
        (image.{u_1, u_4} (α := ι) (⇑P.coroot : (a : ι) → N) (baseOf (⇑P.coroot : (a : ι) → N) (↑g : N →+ ℚ))))
      (-(P.coroot : (a : ι) → N) i : N)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)

Tactic:
rw [hf, P.baseOf_root_eq_baseOf_coroot f hf₀ g hg₀ (fun i ↦ (hg i).symm)]

Premises used: AddMonoidHomClass.toAddMonoidHom, Iff.symm, RootPairing.baseOf_root_eq_baseOf_coroot
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          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)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
hg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) (-i) : N) (-(P.coroot : (a : ι) → N) i : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
⊢ LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) (↑(⋯.toFinset (s := s)) : Set ι)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
have :
  ∀ (this : Fintype ι),
    LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) (↑(⋯.toFinset (s := s)) : Set ι)
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) (↑(⋯.toFinset (s := s)) : Set ι)

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
this : Fintype ι
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) (↑(⋯.toFinset (s := s)) : Set ι)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑(⋯.toFinset (s := s)) : Set ι)))
      ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑(⋯.toFinset (s := s)) : Set ι)))
      (-(P.root : (a : ι) → M) i : M)

Tactic:
simpa using hsp 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
      (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' (↑(⋯.toFinset (s := s)) : Set ι)))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
      (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' (↑(⋯.toFinset (s := s)) : Set ι)))
      (-(P.coroot : (a : ι) → N) i : N)

Tactic:
simpa using coroot_mem_or_neg_mem_closure_of_root P s hli hsp i

Premises used: RootPairing.coroot_mem_or_neg_mem_closure_of_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
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
⊢ ∀ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
simp [P.ne_zero]

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
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) (-i) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simp