-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
obtain :
  ∀ (ι : Type) (_inst : Fintype ι) (hι : ∀ (C : (ι → ↥S) → κ), ∃ (l : Line (↥S) ι), Line.IsMono C l),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₁ :
  ∀ (ι : Type) (_inst : Fintype ι)
    (hι : ∃ (l : Line (↥S) ι), Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ) (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) l),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₂ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
obtain₃ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}), ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
refine_1 :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}), ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
refine_2 :
  (ι : Type) →
    (_inst : Fintype ι) →
      (l : Line (↥S) ι) →
        (c : κ) →
          (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c) →
            let s : Finset ι := {i : ι | l.idxFun i = none};
            (hs : s = {i : ι | l.idxFun i = none}) → (i : ι) → ↥S → M
refine_3 :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}),
      ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) = c
refine_2₁ :
  (ι : Type) →
    (_inst : Fintype ι) →
      (l : Line (↥S) ι) →
        (c : κ) →
          (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c) →
            let s : Finset ι := {i : ι | l.idxFun i = none};
            (hs : s = {i : ι | l.idxFun i = none}) → (i : ι) → ↥S → M
refine_3₁ refine_3₂ refine_3₃ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}) (x : M) (xs : x ∈ S),
      C (#s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) = c
refine_3₄ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ)
    (hl : ∀ (x : ↥S), (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) ((↑l : (x : ↥S) → (i : ι) → ↥S) x) = c),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}) (x : M) (xs : x ∈ S),
      C (#s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) =
        (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M)))
          ((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs))
refine_3₅ refine_3₆ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}) (x : M) (xs : x ∈ S),
      C (#s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) =
        (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M)))
          ((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs))
refine_3₇ :
  ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ),
    let s : Finset ι := {i : ι | l.idxFun i = none};
    ∀ (hs : s = {i : ι | l.idxFun i = none}) (x : M) (xs : x ∈ S),
      #s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0 =
        ∑ i : ι, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have refine_3₈ : ∀ (ι : Type) (_inst : Fintype ι) (l : Line (↥S) ι) (c : κ),
  let s : Finset ι := {i : ι | l.idxFun i = none};
  ∀ (hs : s = {i : ι | l.idxFun i = none}) (x : M) (xs : x ∈ S),
    #s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0 =
      HAdd.hAdd (α := M)
        (∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
        (∑ i ∈ sᶜ, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
Tactic: classical
  obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
  specialize hι fun v => C <| ∑ i, v i
  obtain ⟨l, c, hl⟩ := hι
  set s : Finset ι := {i | l.idxFun i = none} with hs
  refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
  · rw [hs, Finset.mem_filter]
    exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
  · exact fun m => m
  intro x xs
  rw [← hl ⟨x, xs⟩]
  clear hl; congr
  rw [← Finset.sum_add_sum_compl s]
  congr 1
  · rw [← Finset.sum_const]
    apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.mem_filter] at hi
    rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
  · apply Finset.sum_congr rfl
    intro i hi
    rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
    obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
    simp [← hy, Option.map_some, Option.getD]