-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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
i : ι
simp_rw :
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
simp_rw₁ simp_rw₂ :
  ∀ (m : M)
    (hm :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
refine_1 :
  ∀ (m : M)
    (hm :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m)
    (x : M) (h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)) x),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
have refine_2 : ∀ (m : M)
  (hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m)
  (x y : M)
  (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x)
  (hy :
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y),
  (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: classical
  simp_rw [← neg_eq_iff_eq_neg]
  suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr hf'⟩
  intro m hm
  refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
  · rintro - ⟨j, hj, rfl⟩
    exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
  · intro _ _ _ _ ⟨f, hf, hf'⟩ ⟨g, hg, hg'⟩
    refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
    exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩