-- 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
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 :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), (↑z : R) * t = 1
obtain₁ :
  ∀ (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)),
    ∃ (z : ℤ), (↑z : R) * t = 1
h₁ :
  ∀ (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)),
    (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
h₂ h₃ :
  ∀ (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)),
    (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
h₄ :
  ∀ (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)),
    let 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)),
      (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
h₅ :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
    (f : ↥b.support → ℤ),
    let 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)),
      (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
h₆ :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
    (f : ↥b.support → ℤ),
    let 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
⊢ ∃ (z : ℤ), (↑z : R) * t = 1

Tactic:
classical
  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 only [Finset.coe_sort_coe] at 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,
      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.linearIndepOn_coroot
  simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm

Premises used: Finsupp.linearEquivFunOnFinite, mul_comm, RootPairing.coroot, DFunLike.coe