awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u
inst : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
key :
  ∀ (r : ℕ),
    ∃ (ι : Type) (x : Fintype ι),
      ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
ι : Type
_inst : Fintype ι
hι :
  ∀ (C : (ι → Option α) → κ),
    (∃ (s : ColorFocused C), s.lines.card = Fintype.card κ + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
rw : #{ val := Multiset.map AlmostMono.color s.lines, nodup := ⋯ : Finset κ } ≤ Fintype.card κ
rw₁ : Type (max u v)
rw₂ : (Multiset.map AlmostMono.color s.lines).Nodup
⊢ (Fintype.card κ).succ ≤ Fintype.card κ
have f : AlmostMono C → κ
Tactic: rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u
inst : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have pos : ∀ (r : ℕ),
  ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
Tactic: suffices key :
      ∀ r : ℕ,
        ∃ (ι : Type) (_ : Fintype ι),
          ∀ C : (ι → Option α) → κ,
            (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l by
      -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors
      -- so we must be in the second case, where there is a monochromatic line.
      obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
      refine ⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩
      rintro ⟨s, sr⟩
      apply Nat.not_succ_le_self (Fintype.card κ)
      rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
      exact Finset.card_le_univ ⟨_, s.distinct_colors⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u
inst : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
r : ℕ
ihr :
  ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
have pos : ∀ (ι : Type) (_inst : Fintype ι)
  (hι : ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l),
  ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
Tactic: obtain ⟨ι, _inst, hι⟩ := ihr
Cleared hypotheses: ihr
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
Goal:
α : Type u
inst : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
have ihα₁ : ∃ (ι_1 : Type) (x : Fintype ι_1), ∀ (C : (ι_1 → α) → (ι → Option α) → κ), ∃ (l : Line α ι_1), IsMono C l
Tactic: specialize ihα ((ι → Option α) → κ)
Cleared hypotheses: ihα
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u
inst : Fintype α
κ : Type (max v u)
inst_1 : Finite κ
val : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
ihα : ∃ (ι_1 : Type) (x : Fintype ι_1), ∀ (C : (ι_1 → α) → (ι → Option α) → κ), ∃ (l : Line α ι_1), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
have pos : ∀ (ι' : Type) (_inst : Fintype ι') (hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ (l : Line α ι'), IsMono C l),
  ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
Tactic: obtain ⟨ι', _inst, hι'⟩ := ihα
Cleared hypotheses: ihα
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ (l : Line α ι'), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l
have pos : ∀ (C : (ι ⊕ ι' → Option α) → κ),
  (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
Tactic: refine ⟨ι ⊕ ι', inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
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 ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ (l : Line α ι'), IsMono C l
C : (ι ⊕ ι' → Option α) → κ
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have hι'₁ : ∃ (l : Line α ι'),
  IsMono (κ := (ι → Option α) → κ) (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) l
Tactic: specialize hι' fun v' v => C (Sum.elim v (some ∘ v'))
Cleared hypotheses: hι'
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 α) → κ
hι' :
  ∃ (l : Line α ι'),
    IsMono (κ := (ι → Option α) → κ) (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) l
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have pos : ∀ (l' : Line α ι') (C' : (ι → Option α) → κ)
  (hl' :
    ∀ (x : α),
      (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) ((↑l' : (x : α) → (i : ι') → α) x) = C'),
  (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
Tactic: obtain ⟨l', C', hl'⟩ := hι'
Cleared hypotheses: hι'
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
⊢ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have refine : ∀ (x : Option α),
  C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c
Tactic: refine ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, 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 : 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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
x : Option α
⊢ C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c
have rw : C
    (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
      (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
  c
Tactic: rw [Line.horizontal_apply, ← hl, ← hl']
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
x : Option α
rw :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    c
⊢ C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c
have rw₁ : C
    (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
      (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
  C' ((↑l : (x : Option α) → (i : ι) → Option α) x)
Tactic: rw [Line.horizontal_apply, ← hl, ← hl']
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
x : Option α
rw :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    c
rw₁ :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    C' ((↑l : (x : Option α) → (i : ι) → Option α) x)
rw₂ : Option α
⊢ C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c
have rw₃ : C
    (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
      (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
  (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v')))
    ((↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α)) ((↑l : (x : Option α) → (i : ι) → Option α) x)
Tactic: rw [Line.horizontal_apply, ← hl, ← hl']
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
x : Option α
rw :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    c
rw₁ :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    C' ((↑l : (x : Option α) → (i : ι) → Option α) x)
rw₂ : Option α
rw₃ :
  C
      (Sum.elim ((↑l : (x : Option α) → (i : ι) → Option α) x)
        (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) =
    (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v')))
      ((↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α)) ((↑l : (x : Option α) → (i : ι) → Option α) x)
⊢ C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c
have rw₄ : α
Tactic: rw [Line.horizontal_apply, ← hl, ← hl']
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
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'
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have mono_of_mono : (∃ (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']
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
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 + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have hι₁ : (∃ (s : ColorFocused C'), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C' l
Tactic: specialize hι C'
Cleared hypotheses: hι
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have pos : ∀ (s : ColorFocused C') (sr : s.lines.card = r),
  (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
Tactic: rcases hι with (⟨s, sr⟩ | h)
Cleared hypotheses: hι
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have pos₁ : ∀ (h : ∃ (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)
Cleared hypotheses: hι
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have pos : ∀ (h : ∃ p ∈ s.lines, p.color = C' s.focus),
  (∃ (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
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg : ∀ (h : ¬∃ p ∈ s.lines, p.color = C' s.focus),
  (∃ (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
-- 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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have 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
Tactic: obtain ⟨p, p_mem, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
have pos : ∀ (x : Option α), C' ((↑p.line : (x : Option α) → (i : ι) → Option α) x) = p.color
Tactic: refine Or.inr (mono_of_mono ⟨p.line, p.color, ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ C' ((↑p.line : (x : Option α) → (i : ι) → Option α) none) = p.color
have pos : C' ((↑p.line : (x : Option α) → (i : ι) → Option α) none) = C' s.focus
Tactic: rw [hp, s.is_focused p p_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
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
⊢ C' ((↑p.line : (x : Option α) → (i : ι) → Option α) none) = p.color
have pos₁ : C' s.focus = C' s.focus
Tactic: rw [hp, s.is_focused p p_mem]
-- 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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l
have neg : AlmostMono C' → AlmostMono C
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), ?_, ?_⟩, ?_⟩