awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg₁ : ∀ (x : α), C ((↑(vertical s.focus (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = C' s.focus
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), ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg₂ : ∀ (p : AlmostMono C),
  Membership.mem (γ := Multiset (AlmostMono C))
      ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := sorry } ::ₘ
        Multiset.map (fun (p : AlmostMono C') ↦ { line := p.line.prod (map some l'), color := p.color, has_color := sorry })
          s.lines)
      p →
    (↑p.line : (x : Option α) → (i : ι ⊕ ι') → Option α) none =
      Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none)
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), ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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)
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg₃ : (Multiset.map (α := AlmostMono C) AlmostMono.color
    ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := sorry : AlmostMono C } ::ₘ
      Multiset.map
        (fun (p : AlmostMono C') ↦
          { line := p.line.prod (map some l'), color := p.color, has_color := sorry : AlmostMono C })
        s.lines)).Nodup
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), ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg₄ : Multiset.card (α := AlmostMono C)
    (ColorFocused.lines
      {
        lines :=
          { line := vertical s.focus (map some l'), color := C' s.focus, has_color := sorry : AlmostMono C } ::ₘ
            Multiset.map
              (fun (p : AlmostMono C') ↦
                { line := p.line.prod (map some l'), color := p.color, has_color := sorry : AlmostMono C })
              s.lines,
        focus := Sum.elim s.focus ((↑(map some l') : (x : Option α) → (i : ι') → Option α) none), is_focused := sorry,
        distinct_colors := sorry : ColorFocused C }) =
  r + 1
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), ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 C' → AlmostMono C
have neg : ∀ (p : AlmostMono C') (x : α),
  C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
Tactic: refine fun p => ⟨p.line.prod (l'.map some), p.color, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 : α
⊢ C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
have neg : C
    (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x))
      ((↑(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)]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
have neg₁ : C (Sum.elim ((↑p.line : (x : Option α) → (i : ι) → Option α) (some x)) (some ∘ (↑l' : (x : α) → (i : ι') → α) x)) =
  p.color
Tactic: rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
have 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))
Tactic: rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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₃ : α
⊢ C ((↑(p.line.prod (map some l')) : (x : Option α) → (i : ι ⊕ ι') → Option α) (some x)) = p.color
have 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))
Tactic: rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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),
    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)
have neg : ∀ (p : AlmostMono C),
  (p = { line := vertical s.focus (map some l'), color := C' s.focus, has_color := sorry } ∨
      ∃ a ∈ s.lines, { line := a.line.prod (map some l'), color := a.color, has_color := sorry } = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (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
have 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 := sorry }) a =
        AlmostMono.color (C := C)
          { line := vertical s.focus (map some l'), color := C' s.focus, has_color := sorry : 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 := sorry })
      s.lines)
Tactic: rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ 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
have neg : Multiset.card (α := AlmostMono C)
      (Multiset.map
        (fun (p : AlmostMono C') ↦
          { line := p.line.prod (map some l'), color := p.color, has_color := sorry : AlmostMono C })
        s.lines) +
    1 =
  r + 1
Tactic: rw [Multiset.card_cons, Multiset.card_map, sr]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ 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
have neg₁ : s.lines.card + 1 = r + 1
Tactic: rw [Multiset.card_cons, Multiset.card_map, sr]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ 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
have neg₂ : r + 1 = r + 1
Tactic: rw [Multiset.card_cons, Multiset.card_map, sr]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 : α
⊢ C ((↑l : (x : α) → (i : ι) → α) x) = c.down
have rw : C ((↑l : (x : α) → (i : ι) → α) x) = ULift.down.{u, v} ((ULift.up ∘ C) ((↑l : (x : α) → (i : ι) → α) x))
Tactic: rw [← hc x, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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))
⊢ C ((↑l : (x : α) → (i : ι) → α) x) = c.down
have rw₁ : C ((↑l : (x : α) → (i : ι) → α) x) = ULift.down.{u, v} { down := C ((↑l : (x : α) → (i : ι) → α) x) }
Tactic: rw [← hc x, Function.comp_apply]
-- 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: obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
-- 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 ι
hι : ∀ (C : (ι → ↥S) → κ), ∃ (l : Line (↥S) ι), Line.IsMono C l
⊢ ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c
have hι₁ : ∃ (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
Cleared hypotheses: hι
-- 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 ι
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
have 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
Tactic: obtain ⟨l, c, hl⟩ := hι
Cleared hypotheses: hι
-- 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 : κ
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
have hs : 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