awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
κ : Type (max v u)
inst : Finite κ
h : Nonempty κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l

Tactic:
⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩

Premises used: Inhabited.default, Combinatorics.Line.toFun, inferInstance, Unit, PEmpty.rec, Exists.intro, Classical.arbitrary, Eq
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
κ : Type (max v u)
inst : Finite κ
h : Nonempty κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l

Tactic:
refine ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
κ : Type (max v u)
inst : Finite κ
h : ¬Nonempty κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l

Tactic:
⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩

Premises used: False.elim, inferInstance, PEmpty, Nonempty.intro, Empty, Exists.intro, Empty.rec
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
κ : Type (max v u)
inst : Finite κ
h : ¬Nonempty κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l

Tactic:
exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
_ :
  ∀ [Fintype α],
    (∀ (κ : Type (max v u)) [Finite κ],
        ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l) →
      ∀ (κ : Type (max v u)) [Finite κ],
        ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∀ [Fintype α],
    (∀ (κ : Type (max v u)) [Finite κ],
        ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l) →
      ∀ (κ : Type (max v u)) [Finite κ],
        ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
_
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u
inst : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
κ : Type (max v u)
_ : ∀ [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∀ [Finite κ], ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
_
-- Module: Mathlib.Combinatorics.HalesJewett
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 κ
intro :
  ∀ (val : Fintype κ), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
cases nonempty_fintype κ

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.HalesJewett
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 κ
pos :
  ∀ (h : Nonempty α), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
by_cases :
  ∀ (h : ¬Nonempty α), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
by_cases h : Nonempty α

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

Tactic:
⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩

Premises used: Combinatorics.Line.diagonal, inferInstance, Option.none, Unit, Exists.intro, Option
-- Module: Mathlib.Combinatorics.HalesJewett
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 α
refine :
  ∀ (C : (Unit → Option α) → κ) (x : Option α),
    C ((↑(diagonal (Option α) Unit) : (x : Option α) → (i : Unit) → Option α) x) = C fun (x : Unit) ↦ none
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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 α
C : (Unit → Option α) → κ
⊢ C ((↑(diagonal (Option α) Unit) : (x : Option α) → (i : Unit) → Option α) none) = C fun (x : Unit) ↦ none

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
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 α
C : (Unit → Option α) → κ
a : α
⊢ C ((↑(diagonal (Option α) Unit) : (x : Option α) → (i : Unit) → Option α) (some a)) = C fun (x : Unit) ↦ none

Tactic:
(h ⟨a⟩).elim

Premises used: False.elim, Nonempty.intro
-- Module: Mathlib.Combinatorics.HalesJewett
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 α
C : (Unit → Option α) → κ
a : α
⊢ C ((↑(diagonal (Option α) Unit) : (x : Option α) → (i : Unit) → Option α) (some a)) = C fun (x : Unit) ↦ none

Tactic:
exact (h ⟨a⟩).elim

Premises used: False.elim, Nonempty.intro
-- Module: Mathlib.Combinatorics.HalesJewett
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

Tactic:
case neg =>
      refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
      rintro (_ | ⟨a⟩)
      · rfl
      · exact (h ⟨a⟩).elim
-- Module: Mathlib.Combinatorics.HalesJewett
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
obtain :
  ∀ (ι : Type) (_inst : Fintype ι)
    (hι :
      ∀ (C : (ι → Option α) → κ),
        (∃ (s : ColorFocused C), s.lines.card = Fintype.card κ + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l),
    ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)

Premises used: Fintype.card, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩

Premises used: Or.resolve_left, Exists.intro
-- Module: Mathlib.Combinatorics.HalesJewett
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
refine : ∀ (C : (ι → Option α) → κ), ¬∃ (s : ColorFocused C), s.lines.card = Fintype.card κ + 1
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
refine ⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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
apply : (Fintype.card κ).succ ≤ Fintype.card κ
⊢ False

Tactic:
apply Nat.not_succ_le_self (Fintype.card κ)

Premises used: Fintype.card, Nat.not_succ_le_self
-- Module: Mathlib.Combinatorics.HalesJewett
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
f : AlmostMono C → κ
⊢ (Fintype.card κ).succ ≤ Fintype.card κ

Tactic:
rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]

Premises used: Nat.add_one, Finset.card_mk, Multiset.card_map
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ #{ val := Multiset.map AlmostMono.color s.lines, nodup := ⋯ : Finset κ } ≤ Fintype.card κ

Tactic:
Finset.card_le_univ ⟨_, s.distinct_colors⟩

Premises used: Finset.card_le_univ, Finset.mk, Combinatorics.Line.ColorFocused.distinct_colors
-- Module: Mathlib.Combinatorics.HalesJewett
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 α
pos :
  ∀ (r : ℕ),
    ∃ (ι : Type) (x : Fintype ι),
      ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r) ∨ ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (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⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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 α) → κ), (∃ (s : ColorFocused C), s.lines.card = 0) ∨ ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
⟨Empty, inferInstance, fun C => Or.inl ⟨default, Multiset.card_zero⟩⟩

Premises used: Inhabited.default, inferInstance, Multiset.card_zero, Empty, Exists.intro, Or.inl
-- Module: Mathlib.Combinatorics.HalesJewett
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 α) → κ), (∃ (s : ColorFocused C), s.lines.card = 0) ∨ ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
exact ⟨Empty, inferInstance, fun C => Or.inl ⟨default, Multiset.card_zero⟩⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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
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
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
obtain ⟨ι, _inst, hι⟩ := ihr
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ ∃ (ι_1 : Type) (x : Fintype ι_1), ∀ (C : (ι_1 → α) → (ι → Option α) → κ), ∃ (l : Line α ι_1), IsMono C l

Tactic:
specialize ihα ((ι → Option α) → κ)
-- Module: Mathlib.Combinatorics.HalesJewett
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
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
⊢ ∃ (ι : Type) (x : Fintype ι),
    ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) ι), IsMono C l

Tactic:
obtain ⟨ι', _inst, hι'⟩ := ihα
-- 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 ι'
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:
⟨ι ⊕ ι', inferInstance, ?_⟩

Premises used: inferInstance, Sum, Exists.intro
-- 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 ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ (l : Line α ι'), IsMono C l
pos :
  ∀ (C : (ι ⊕ ι' → Option α) → κ),
    (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (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:
refine ⟨ι ⊕ ι', inferInstance, ?_⟩
-- 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 ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ (l : Line α ι'), IsMono C l
C : (ι ⊕ ι' → Option α) → κ
⊢ ∃ (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'))

Premises used: Option.some, Function.comp, Sum.elim
-- 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 α) → κ
hι' :
  ∃ (l : Line α ι'),
    IsMono (κ := (ι → Option α) → κ) (fun (v' : ι' → α) (v : ι → Option α) ↦ C (Sum.elim v (some ∘ v'))) l
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
⊢ (∃ (s : ColorFocused C), s.lines.card = r + 1) ∨ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
obtain ⟨l', C', hl'⟩ := 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 ι
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

Tactic:
⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => ?_⟩

Premises used: Combinatorics.Line.toFun, Option.some, Function.comp, Exists.intro, Classical.arbitrary, Combinatorics.Line.horizontal
-- 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 α) ι
c : κ
hl : ∀ (x : Option α), C' ((↑l : (x : Option α) → (i : ι) → Option α) x) = c
refine :
  ∀ (x : Option α),
    C
        ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
            (x : Option α) → (i : ι ⊕ ι') → Option α)
          x) =
      c
⊢ ∃ (l : Line (Option α) (ι ⊕ ι')), IsMono C l

Tactic:
refine ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => ?_⟩
-- 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 α) ι
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)
rw₄ : α
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)
rw₇ : α
rw₈ : Option α
⊢ C
      ((↑(l.horizontal (some ∘ (↑l' : (x : α) → (i : ι') → α) (Classical.arbitrary α))) :
          (x : Option α) → (i : ι ⊕ ι') → Option α)
        x) =
    c

Tactic:
rw [Line.horizontal_apply, ← hl, ← hl']

Premises used: Combinatorics.Line.horizontal_apply