-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma eq_one_or_neg_one_of_mem_support_of_smul_mem_aux [Finite ι]
    [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N]
    (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) :
    ∃ z : ℤ, z * t = 1

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this : Fintype ι
j : ι
hj : P.root j = t • P.root i
f : ↑b.support → ℤ
hf :
  P.coroot i =
    (linearCombination R fun k => P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↑b.support).symm fun x => ↑(f x))
g : ↑b.support →₀ R := single ⟨i, h⟩ 1
⊢ ↑(f ⟨i, h⟩) * t = 1

Tactic:
have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this : Fintype ι
j : ι
hj : P.root j = t • P.root i
f : ↑b.support → ℤ
hf :
  P.coroot i =
    (linearCombination R fun k => P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↑b.support).symm fun x => ↑(f x))
g : ↑b.support →₀ R := single ⟨i, h⟩ 1
hg : P.coroot i = (linearCombination R fun k => P.coroot ↑k) g
⊢ ↑(f ⟨i, h⟩) * t = 1

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this : Fintype ι
j : ι
hj : P.root j = t • P.root i
f : ↑b.support → ℤ
hf : P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i
⊢ P.coroot i =
    (linearCombination R fun k => P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↑b.support).symm fun x => ↑(f x))

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

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this : Fintype ι
j : ι
hj : P.root j = t • P.root i
f : ↑b.support → ℤ
hf : P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i
⊢ ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i = t • ∑ i : ↑b.support, ↑(f i) • P.coroot ↑i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this : Fintype ι
j : ι
hj : P.root j = t • P.root i
f : ↑b.support → ℤ
hf :
  P.coroot i =
    (linearCombination R fun k => P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↑b.support).symm fun x => ↑(f x))
g : ↑b.support →₀ R := single ⟨i, h⟩ 1
⊢ P.coroot i = (linearCombination R fun k => P.coroot ↑k) g

Tactic:
simp [g]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this✝ : Fintype ι
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i : ↑b.support, c i • P.coroot ↑i = P.coroot j
⊢ ∃ f, P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i

Tactic:
refine this.imp fun f hf ↦ ?_

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝² : Finite ι
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
this✝ : Fintype ι
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i : ↑b.support, c i • P.coroot ↑i = P.coroot j
f : ↑b.support → ℤ
hf : ∑ i : ↑b.support, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i