awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → κ
ι : 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
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
have refine_1 : sorry.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
Tactic: refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
-- 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 → κ
ι : 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
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
refine_1 : ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have refine_2 : (i : ι) → ↥S → M
Tactic: refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
-- 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 → κ
ι : 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
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
refine_1 : ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
refine_2 : (i : ι) → ↥S → M
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have refine_3 : ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) = c
Tactic: refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
-- 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 → κ
ι : 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
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
⊢ ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
have refine_1 : Membership.mem (γ := Finset ι) Finset.univ (sorry.choose (p := fun (i : ι) ↦ l.idxFun i = none)) ∧
  l.idxFun (sorry.choose (p := fun (i : ι) ↦ l.idxFun i = none)) = none
Tactic: rw [hs, Finset.mem_filter]
-- 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 → κ
ι : 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
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
have refine_3 : 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))
Tactic: rw [← hl ⟨x, xs⟩]
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
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))
have refine_3 : #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)
Tactic: congr
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
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)
have refine_3 : #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: rw [← Finset.sum_add_sum_compl s]
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
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))
have refine_3 : #s • x = ∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
Tactic: congr 1
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
refine_3 : #s • x = ∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
⊢ #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))
have refine_3₁ : Eq.{u_5 + 1} (α := M) (∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0)
  (∑ i ∈ sᶜ, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
Tactic: congr 1
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x = ∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have refine_3 : Eq.{u_5 + 1} (α := M) (∑ _x ∈ s, x)
  (∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
Tactic: rw [← Finset.sum_const]
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ Eq.{u_5 + 1} (α := M) (∑ _x ∈ s, x)
    (∑ i ∈ s, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
have refine_3 : ∀ x_1 ∈ s, x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) x_1) : M)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have hi₁ : Membership.mem (γ := Finset ι) Finset.univ i ∧ l.idxFun i = none
Tactic: rw [hs, Finset.mem_filter] at hi
Cleared hypotheses: hi
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i ∧ l.idxFun i = none
⊢ x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have refine_3 : x = (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) : M)
Tactic: rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i ∧ l.idxFun i = none
refine_3 : x = (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) : M)
⊢ x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have refine_3₁ : x = x
Tactic: rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ Eq.{u_5 + 1} (α := M) (∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0)
    (∑ i ∈ sᶜ, (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M))
have refine_3 : ∀ x_1 ∈ sᶜ,
  Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun x_1)) 0 =
    (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) x_1) : M)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ sᶜ
⊢ Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0 =
    (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have hi₁ : Membership.mem (γ := Finset ι) Finset.univ i ∧ ¬l.idxFun i = none
Tactic: rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
Cleared hypotheses: hi
-- 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 → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i : ι | l.idxFun i = none}
hs : s = {i : ι | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i ∧ ¬l.idxFun i = none
⊢ Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0 =
    (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
have refine_3 : ∀ (y : ↥S) (hy : some y = l.idxFun i),
  Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0 =
    (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)
Tactic: obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
-- 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 → κ
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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
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]
-- 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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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
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]
-- 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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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
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]
-- 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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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
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]
-- 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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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}), sorry.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s
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]
-- 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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have 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
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]