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 : Nonempty α
r : ℕ
ι : Type
_inst_1 : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
ι' : 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'
⊢ (∃ (l : Line (Option α) ι), IsMono C' l) → ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
have mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l := by
      rintro ⟨l, c, hl⟩
      refine ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => ?_⟩
      rw [Line.horizontal_apply, ← hl, ← hl']
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst_1 : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
ι' : 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'), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C' l

Tactic:
specialize hι C'
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
hι : (∃ (s : ColorFocused C'), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C' l
pos :
  ∀ (s : ColorFocused C') (sr : s.lines.card = r),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
pos₁ :
  ∀ (h : ∃ (l : Line (Option α) ι), IsMono C' l),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
rcases hι with (⟨s, sr⟩ | h)
-- 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
h : ∃ (l : Line (Option α) ι), IsMono C' l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
Or.inr (mono_of_mono h)

Premises used: Or.inr
-- 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
h : ∃ (l : Line (Option α) ι), IsMono C' l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
exact Or.inr (mono_of_mono h)

Premises used: Or.inr
-- 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
h : ∃ (l : Line (Option α) ι), IsMono C' l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
on_goal 2 => exact Or.inr (mono_of_mono h)

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
pos :
  ∀ (h : ∃ p ∈ s.lines, p.color = C' s.focus),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
neg :
  ∀ (h : ¬∃ p ∈ s.lines, p.color = C' s.focus),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
by_cases h : ∃ p ∈ s.lines, (p : AlmostMono _).color = C' s.focus

Premises used: Combinatorics.Line.ColorFocused.lines, Combinatorics.Line.ColorFocused.focus
-- 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
pos :
  ∀ (p : AlmostMono C') (p_mem : p ∈ s.lines) (hp : p.color = C' s.focus),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
obtain ⟨p, p_mem, hp⟩ := h
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
Or.inr (mono_of_mono ⟨p.line, p.color, ?_⟩)

Premises used: Combinatorics.Line.AlmostMono.line, Combinatorics.Line.AlmostMono.color, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
pos : ∀ (x : Option α), C' ((↑p.line : (x : Option α) → (i : ι) → Option α) x) = p.color
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
refine Or.inr (mono_of_mono ⟨p.line, p.color, ?_⟩)

Premises used: Combinatorics.Line.AlmostMono.line, Combinatorics.Line.AlmostMono.color, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
pos : C' ((↑p.line : (x : Option α) → (i : ι) → Option α) none) = C' s.focus
pos₁ pos₂ : C' s.focus = C' s.focus
⊢ C' ((↑p.line : (x : Option α) → (i : ι) → Option α) none) = p.color

Tactic:
rw [hp, s.is_focused p p_mem]

Premises used: Combinatorics.Line.ColorFocused.is_focused
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : 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
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
val_1 : α
⊢ C' ((↑p.line : (x : Option α) → (i : ι) → Option α) (some val_1)) = p.color

Tactic:
apply p.has_color

Premises used: Combinatorics.Line.AlmostMono.has_color
-- 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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
Or.inl ⟨⟨(s.lines.map ?_).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => ?_⟩,
            Sum.elim s.focus (l'.map some none), ?_, ?_⟩, ?_⟩

Premises used: Multiset.map, Combinatorics.Line.map, Combinatorics.Line.toFun, Option.some, Multiset.cons, Combinatorics.Line.ColorFocused.mk, Option.none, Combinatorics.Line.ColorFocused.lines, Exists.intro, Or.inl, Combinatorics.Line.ColorFocused.focus, Combinatorics.Line.AlmostMono.mk, Combinatorics.Line.vertical, Sum.elim
-- 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 : AlmostMono C' → AlmostMono C
neg₁ :
  ∀ (x : α), C ((↑(vertical s.focus (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = C' s.focus
neg₂ :
  ∀ (p : AlmostMono C),
    Membership.mem (γ := Multiset (AlmostMono C))
        ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
          Multiset.map
            (fun (p : AlmostMono C') ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines)
        p →
      (↑p.line : (x : Option α) → (i : ι ⊕ ι') → Option α) none =
        Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)
neg₃ :
  (Multiset.map (α := AlmostMono C) AlmostMono.color
      ({ 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)).Nodup
neg₄ :
  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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
refine Or.inl ⟨⟨(s.lines.map ?_).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => ?_⟩,
            Sum.elim s.focus (l'.map some none), ?_, ?_⟩, ?_⟩

Premises used: Or.inl
-- 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 :
  ∀ (p : AlmostMono C') (x : α),
    C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
⊢ AlmostMono C' → AlmostMono C

Tactic:
refine fun p => ⟨p.line.prod (l'.map some), p.color, fun x => ?_⟩
-- 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
p : AlmostMono C'
x : α
neg :
  C
      (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x))
        ((↑(map some l') : (x : Option α) → (i : ι') → Option α) (some x))) =
    p.color
neg₁ :
  C (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x)) (some ∘ (↑l' : (x : α) → (i : ι') → α) x)) =
    p.color
neg₂ :
  C (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x)) (some ∘ (↑l' : (x : α) → (i : ι') → α) x)) =
    C' ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x))
neg₃ : α
neg₄ :
  C (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x)) (some ∘ (↑l' : (x : α) → (i : ι') → α) x)) =
    (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) ((↑l' : (x : α) → (i : ι') → α) x)
      ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x))
neg₅ : α
neg₆ :
  C (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x)) (some ∘ (↑l' : (x : α) → (i : ι') → α) x)) =
    (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) ((↑l' : (x : α) → (i : ι') → α) x)
      ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x))
neg₇ : α
⊢ C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color

Tactic:
rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]

Premises used: Combinatorics.Line.prod_apply, Combinatorics.Line.AlmostMono.has_color, Combinatorics.Line.map_apply, congr_fun
-- 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 :
  ∀ (p : AlmostMono C),
    (p = { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ∨
        ∃ a ∈ s.lines, { line := a.line.prod (map some l'), color := a.color, has_color := ⋯ } = p) →
      (↑p.line : (x : Option α) → (i : ι ⊕ ι') → Option α) none =
        Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)
⊢ ∀ (p : AlmostMono C),
    Membership.mem (γ := Multiset (AlmostMono C))
        ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
          Multiset.map
            (fun (p : AlmostMono C') ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines)
        p →
      (↑p.line : (x : Option α) → (i : ι ⊕ ι') → Option α) none =
        Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)

Tactic:
simp_rw [Multiset.mem_cons, Multiset.mem_map]

Premises used: Multiset.mem_map, Multiset.mem_cons
-- 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
⊢ (↑(AlmostMono.line (C := C)
            { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ : AlmostMono C }) :
        (x : Option α) → (i : ι ⊕ ι') → Option α)
      none =
    Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)

Tactic:
simp only [vertical_apply]

Premises used: Combinatorics.Line.vertical_apply
-- 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
q : AlmostMono C'
hq : q ∈ s.lines
⊢ (↑(AlmostMono.line (C := C) { line := q.line.prod (map some l'), color := q.color, has_color := ⋯ : AlmostMono C }) :
        (x : Option α) → (i : ι ⊕ ι') → Option α)
      none =
    Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)

Tactic:
simp only [prod_apply, s.is_focused q hq]

Premises used: Combinatorics.Line.ColorFocused.is_focused, Combinatorics.Line.prod_apply
-- 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 :
  (¬∃ 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)
⊢ (Multiset.map (α := AlmostMono C) AlmostMono.color
      ({ 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)).Nodup

Tactic:
rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]

Premises used: Multiset.map_cons, Multiset.mem_map, Multiset.nodup_cons, Multiset.map_map
-- 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:
⟨h, s.distinct_colors⟩

Premises used: And.intro, Combinatorics.Line.ColorFocused.distinct_colors