awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
rw :
  ∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) =
    HSMul.hSMul (β := N) t
      (∑ i : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)

Tactic:
rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]

Premises used: Fintype.linearCombination_apply, Finsupp.linearCombination_eq_fintype_linearCombination_apply, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
simp_rw :
  ∑ x : ↥b.support,
      t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) =
    HSMul.hSMul (β := N) t
      (∑ i : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))
⊢ ∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) =
    HSMul.hSMul (β := N) t
      (∑ i : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))

Tactic:
simp_rw [mul_smul, ← Finset.smul_sum]

Premises used: Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)

Tactic:
replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
      (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
    simp_rw [mul_smul, ← Finset.smul_sum]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)

Tactic:
simp [g]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)

Tactic:
have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
⊢ Eq.{u_4 + 1} (α := N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)

Tactic:
rw [hg] at hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
hf₁ :
  Eq.{u_4 + 1} (α := N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)

Tactic:
rw [hg] at hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hf :
  Eq.{u_4 + 1} (α := N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
⊢ Injective (α := Finsupp.{u_1, u_2} (↥b.support) R) (β := N)
    (⇑(linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι)) : (a : ↥b.support →₀ R) → N)

Tactic:
have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hf :
  Eq.{u_4 + 1} (α := N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
this :
  Injective (α := Finsupp.{u_1, u_2} (↥b.support) R) (β := N)
    (⇑(linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι)) : (a : ↥b.support →₀ R) → N)
⊢ (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1

Tactic:
simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm

Premises used: DFunLike.congr_fun, Finsupp.linearEquivFunOnFinite, mul_comm, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
obtain : ∀ (z : ℤ) (hz : (↑z : R) * t = 1), t = 1 ∨ t = -1
⊢ t = 1 ∨ t = -1

Tactic:
obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht

Premises used: RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
z : ℤ
hz : (↑z : R) * t = 1
obtain :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))

Tactic:
obtain ⟨j, hj⟩ := ht
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))

Tactic:
simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hz, one_smul] using mem_range_self j

Premises used: Set.mem_range_self, Iff.mpr, RootPairing.coroot_eq_smul_coroot_iff, smul_smul, one_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
z : ℤ
hz : (↑z : R) * t = 1
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))

Tactic:
replace ht : (z : R) • P.coroot i ∈ range P.coroot := by
    obtain ⟨j, hj⟩ := ht
    simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hz, one_smul] using mem_range_self j
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
obtain : ∀ (w : ℤ) (hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1), t = 1 ∨ t = -1
⊢ t = 1 ∨ t = -1

Tactic:
obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h _ ht

Premises used: RootPairing.Base.flip, RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
⊢ HMul.hMul (α := R) (↑z : R) (↑w : R) = 1

Tactic:
simpa [mul_mul_mul_comm _ t, mul_comm t, mul_comm _ (z : R), hz] using congr_arg₂ (· * ·) hz hw

Premises used: Int.cast, HMul.hMul, mul_mul_mul_comm, mul_comm, congr_arg₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
⊢ HMul.hMul (α := R) (↑z : R) (↑w : R) = 1

Tactic:
have : (z : R) * w = 1 := by
    simpa [mul_mul_mul_comm _ t, mul_comm t, mul_comm _ (z : R), hz] using congr_arg₂ (· * ·) hz hw
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this_1 : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
this : z = 1 ∨ z = -1
inl :
  ∀ (hz : (↑1 : R) * t = 1)
    (ht :
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N)))
    (hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1) (this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1), t = 1 ∨ t = -1
inr :
  ∀ (hz : (↑(-1) : R) * t = 1)
    (ht :
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(-1) : R) ((P.coroot : (a : ι) → N) i : N)))
    (hw : HMul.hMul (α := R) (↑w : R) (↑(-1) : R) = 1) (this : HMul.hMul (α := R) (↑(-1) : R) (↑w : R) = 1),
    t = 1 ∨ t = -1
⊢ t = 1 ∨ t = -1

Tactic:
rcases this with rfl | rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑1 : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1
this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1
inl : t = 1
⊢ t = 1 ∨ t = -1

Tactic:
left
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑1 : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1
this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1
⊢ t = 1

Tactic:
simpa using hz
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑(-1) : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(-1) : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑(-1) : R) = 1
this : HMul.hMul (α := R) (↑(-1) : R) (↑w : R) = 1
inr : t = -1
⊢ t = 1 ∨ t = -1

Tactic:
right
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑(-1) : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(-1) : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑(-1) : R) = 1
this : HMul.hMul (α := R) (↑(-1) : R) (↑w : R) = 1
⊢ t = -1

Tactic:
simpa [neg_eq_iff_eq_neg] using hz

Premises used: neg_eq_iff_eq_neg