-- 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
hg : P.coroot i = (linearCombination R fun k => P.coroot ↑k) g
⊢ ↑(f ⟨i, h⟩) * t = 1

Tactic:
rw [hg] at hf

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 → ℤ
g : ↑b.support →₀ R := single ⟨i, h⟩ 1
hf :
  (linearCombination R fun k => P.coroot ↑k) g =
    (linearCombination R fun k => P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↑b.support).symm fun x => ↑(f x))
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
ht : t • P.root i ∈ range ⇑P.root
⊢ ∃ z, ↑z * t = 1

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
ht : t • P.root i ∈ range ⇑P.root
this : Fintype ι
⊢ ∃ z, ↑z * 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
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

Tactic:
simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
  coroot_eq_smul_coroot_iff.mpr hj]

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
ht : t • P.root i ∈ range ⇑P.root
⊢ ∃ z, ↑z * t = 1

Tactic:
classical
have : Fintype ι := Fintype.ofFinite ι
obtain ⟨j, hj⟩ := ht
obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by
  have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
  rw [image_eq_range, mem_span_range_iff_exists_fun] at this
  refine this.imp fun f hf ↦ ?_
  simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
    coroot_eq_smul_coroot_iff.mpr hj]
use f ⟨i, h⟩
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 R R,
    Fintype.linearCombination_apply, hf]
  simp_rw [mul_smul, ← Finset.smul_sum]
let g : b.support →₀ R := single ⟨i, h⟩ 1
have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
rw [hg] at hf
have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linInd_coroot
simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm

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
⊢ ∃ f, P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i

Tactic:
have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j

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 : P.coroot j ∈ span ℤ (⇑P.coroot '' b.support)
⊢ ∃ f, P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i

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))
⊢ ↑(f ⟨i, h⟩) * t = 1

Tactic:
let g : b.support →₀ R := single ⟨i, h⟩ 1

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
⊢ ↑(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
this : P.coroot j ∈ span ℤ (⇑P.coroot '' b.support)
⊢ ∃ f, P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i

Tactic:
rw [image_eq_range, mem_span_range_iff_exists_fun] at this

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, P.coroot i = ∑ i : ↑b.support, (t * ↑(f i)) • P.coroot ↑i