awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h_1 : Nonempty α
r : ℕ
ι : Type
_inst_1 : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' :
  ∀ (x : α), (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) ((↑l' : (x : α) → (i : ι') → α) x) = C'
mono_of_mono : (∃ (l : Line (Option α) ι), IsMono C' l) → ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
⊢ (¬∃ a ∈ s.lines,
        comp (β := AlmostMono C) AlmostMono.color
            (fun (p : AlmostMono C') ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) a =
          AlmostMono.color (C := C)
            { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ : AlmostMono C }) ∧
    Multiset.Nodup (α := κ)
      (Multiset.map
        (comp (β := AlmostMono C) AlmostMono.color fun (p : AlmostMono C') ↦
          { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ })
        s.lines)

Tactic:
exact ⟨h, s.distinct_colors⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h_1 : Nonempty α
r : ℕ
ι : Type
_inst_1 : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' :
  ∀ (x : α), (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) ((↑l' : (x : α) → (i : ι') → α) x) = C'
mono_of_mono : (∃ (l : Line (Option α) ι), IsMono C' l) → ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
neg :
  Multiset.card (α := AlmostMono C)
        (Multiset.map
          (fun (p : AlmostMono C') ↦
            { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ : AlmostMono C })
          s.lines) +
      1 =
    r + 1
neg₁ : s.lines.card + 1 = r + 1
neg₂ neg₃ : r + 1 = r + 1
⊢ Multiset.card (α := AlmostMono C)
      (ColorFocused.lines
        {
          lines :=
            { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ : AlmostMono C } ::ₘ
              Multiset.map
                (fun (p : AlmostMono C') ↦
                  { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ : AlmostMono C })
                s.lines,
          focus := Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none), is_focused := ⋯,
          distinct_colors := ⋯ : ColorFocused C }) =
    r + 1

Tactic:
rw [Multiset.card_cons, Multiset.card_map, sr]

Premises used: Multiset.card_cons, Multiset.card_map
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Finite α
κ : Type v
inst_1 : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ (l : Line α ι), IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift.{u, v} κ
hc : ∀ (x : α), (ULift.up ∘ C) ((↑l : (x : α) → (i : ι) → α) x) = c
x : α
rw : C ((↑l : (x : α) → (i : ι) → α) x) = ULift.down.{u, v} ((ULift.up ∘ C) ((↑l : (x : α) → (i : ι) → α) x))
rw₁ rw₂ : C ((↑l : (x : α) → (i : ι) → α) x) = ULift.down.{u, v} { down := C ((↑l : (x : α) → (i : ι) → α) x) }
⊢ C ((↑l : (x : α) → (i : ι) → α) x) = c.down

Tactic:
rw [← hc x, Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Combinatorics.HalesJewett
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

Tactic:
obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ

Premises used: Combinatorics.Line.exists_mono_in_high_dimension, Membership.mem, Subtype
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → ↥S) → κ), ∃ (l : Line (↥S) ι), Line.IsMono C l
⊢ ∃ (l : Line (↥S) ι), Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ) (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) l

Tactic:
specialize hι fun v => C <| ∑ i, v i

Premises used: Finset.univ, Subtype.val, Finset.sum
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
M : Type u_5
κ : Type u_6
inst : AddCommMonoid M
S : Finset M
inst_1 : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∃ (l : Line (↥S) ι), Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ) (fun (v : ι → ↥S) ↦ C (∑ i : ι, (↑(v i) : M))) l
obtain :
  ∀ (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

Tactic:
obtain ⟨l, c, hl⟩ := hι
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ let s : Finset ι := {i : ι | l.idxFun i = none};
  s = {i : ι | l.idxFun i = none}

Tactic:
set s : Finset ι := {i | l.idxFun i = none} with hs

Premises used: Finset, Option.none
-- Module: Mathlib.Combinatorics.HalesJewett
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

Tactic:
⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩

Premises used: Iff.mpr, Compl.compl, Option.getD, Combinatorics.Line.proper, Combinatorics.Line.idxFun, Option.map, And.intro, Exists.intro, Finset.card, Finset.card_pos, Exists.choose, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Combinatorics.HalesJewett
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
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
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c

Tactic:
refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0,
    c, ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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 :
  Membership.mem (γ := Finset ι) Finset.univ (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) ∧
    l.idxFun (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) = none
⊢ ⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none) ∈ s

Tactic:
rw [hs, Finset.mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.HalesJewett
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}
⊢ Membership.mem (γ := Finset ι) Finset.univ (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) ∧
    l.idxFun (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) = none

Tactic:
⟨Finset.mem_univ _, l.proper.choose_spec⟩

Premises used: Finset.mem_univ, Exists.choose_spec, Combinatorics.Line.proper, And.intro
-- Module: Mathlib.Combinatorics.HalesJewett
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}
⊢ Membership.mem (γ := Finset ι) Finset.univ (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) ∧
    l.idxFun (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none)) = none

Tactic:
exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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}
i : ι
⊢ ↥S → M

Tactic:
exact fun m => m
-- Module: Mathlib.Combinatorics.HalesJewett
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
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))
⊢ C (#s • x + ∑ i ∈ sᶜ, Option.getD (Option.map (fun (m : ↥S) ↦ (↑m : M)) (l.idxFun i)) 0) = c

Tactic:
rw [← hl ⟨x, xs⟩]

Premises used: Subtype.mk
-- Module: Mathlib.Combinatorics.HalesJewett
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ᶜ, 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)
⊢ 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:
congr
-- Module: Mathlib.Combinatorics.HalesJewett
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ᶜ, 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))
⊢ #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:
rw [← Finset.sum_add_sum_compl s]

Premises used: Finset.sum_add_sum_compl
-- Module: Mathlib.Combinatorics.HalesJewett
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)
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))
⊢ #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:
congr 1
-- Module: Mathlib.Combinatorics.HalesJewett
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 :
  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))
⊢ #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]

Premises used: Finset.sum_const
-- Module: Mathlib.Combinatorics.HalesJewett
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 : ∀ x_1 ∈ s, x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) x_1) : M)
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ Membership.mem (γ := Finset ι) Finset.univ i ∧ l.idxFun i = none

Tactic:
rw [hs, Finset.mem_filter] at hi

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.HalesJewett
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)
refine_3₁ refine_3₂ : x = x
⊢ x = (↑((↑l : (x : ↥S) → (i : ι) → ↥S) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xs) i) : M)

Tactic:
rw [l.apply_none _ _ hi.right, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Combinatorics.Line.apply_none, And.right
-- Module: Mathlib.Combinatorics.HalesJewett
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 :
  ∀ 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)
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.HalesJewett
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ᶜ
⊢ Membership.mem (γ := Finset ι) Finset.univ i ∧ ¬l.idxFun i = none

Tactic:
rw [hs, Finset.compl_filter, Finset.mem_filter] at hi

Premises used: Finset.compl_filter, Finset.mem_filter
-- Module: Mathlib.Combinatorics.HalesJewett
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 :
  ∀ (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)
⊢ 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

Premises used: Option.ne_none_iff_exists, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.HalesJewett
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
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:
simp [← hy, Option.map_some, Option.getD]

Premises used: Option.getD, Option.map_some
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
intro : ∀ (val : Fintype η), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l

Tactic:
cases nonempty_fintype η

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
intro :
  ∀ (ι : Type) (w : Fintype ι)
    (hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l),
    ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l

Tactic:
obtain ⟨ι, _, hι⟩ := Line.exists_mono_in_high_dimension (Shrink.{0} η → α) κ

Premises used: Combinatorics.Line.exists_mono_in_high_dimension
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l

Tactic:
⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩

Premises used: inferInstance, Exists.intro, Shrink, Prod
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
intro : ∀ (C : (ι × Shrink.{0, u_7} η → α) → κ), ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l

Tactic:
refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
intro :
  ∀ (l : Line (Shrink.{0, u_7} η → α) ι)
    (hl :
      Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
        (fun (x : ι → Shrink.{0, u_7} η → α) ↦
          C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
            match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
            | (i, e) => x i e)
        l),
    ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l
⊢ ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l

Tactic:
obtain ⟨l, hl⟩ := hι fun x ↦ C fun (i, e) ↦ x i e

Premises used: _private.0.Combinatorics.Subspace.exists_mono_in_high_dimension.match_1
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
    (fun (x : ι → Shrink.{0, u_7} η → α) ↦
      C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
        match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
        | (i, e) => x i e)
    l
⊢ ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l

Tactic:
⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩

Premises used: Combinatorics.Line.toSubspace, Combinatorics.Subspace.reindex, Exists.intro, Equiv.symm, equivShrink, Equiv.refl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
    (fun (x : ι → Shrink.{0, u_7} η → α) ↦
      C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
        match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
        | (i, e) => x i e)
    l
intro : IsMono C (l.toSubspace.reindex (Equiv.symm (equivShrink η)) (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))
⊢ ∃ (l : Subspace η α (ι × Shrink.{0, u_7} η)), IsMono C l

Tactic:
refine ⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
κ : Type u_6
η : Type u_7
inst : Finite α
inst_1 : Finite κ
inst_2 : Finite η
val : Fintype η
ι : Type
w : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ (l : Line (Shrink.{0, u_7} η → α) ι), Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono.{u_5, 0, u_6 + 1} (κ := κ)
    (fun (x : ι → Shrink.{0, u_7} η → α) ↦
      C fun (x_1 : ι × Shrink.{0, u_7} η) ↦
        match (motive := ι × Shrink.{0, u_7} η → α) x_1 with
        | (i, e) => x i e)
    l
⊢ IsMono.{u_7, u_5, 0, u_6} (κ := κ)
    (fun (x : ι × Shrink.{0, u_7} η → α) ↦
      C
        ((⇑(Equiv.refl α).symm : (a : α) → α) ∘
          x ∘ (⇑(Equiv.refl (ι × Shrink.{0, u_7} η)) : (a : ι × Shrink.{0, u_7} η) → ι × Shrink.{0, u_7} η)))
    (l.toSubspace.reindex (Equiv.symm (equivShrink η)) (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))

Tactic:
hl.toSubspace.reindex

Premises used: Combinatorics.Subspace.IsMono.reindex, Combinatorics.Line.IsMono.toSubspace