awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
    (eα : (a : α) → α')
      ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
        ((eι.symm : (a : ι') → ι) i))
have inl : ∀ (val : α) (h : l.idxFun ((eι.symm : (a : ι') → ι) i) = Sum.inl val),
  (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
    (eα : (a : α) → α')
      ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
        ((eι.symm : (a : ι') → ι) i))
Tactic: cases h : l.idxFun (eι.symm i)
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
inl :
  ∀ (val : α) (h : l.idxFun ((eι.symm : (a : ι') → ι) i) = Sum.inl val),
    (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
      (eα : (a : α) → α')
        ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
          ((eι.symm : (a : ι') → ι) i))
⊢ (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
    (eα : (a : α) → α')
      ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
        ((eι.symm : (a : ι') → ι) i))
have inr : ∀ (val : η) (h : l.idxFun ((eι.symm : (a : ι') → ι) i) = Sum.inr val),
  (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
    (eα : (a : α) → α')
      ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
        ((eι.symm : (a : ι') → ι) i))
Tactic: cases h : l.idxFun (eι.symm i)
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ IsMono C (l.reindex eη eα eι) ↔
    IsMono.{u_5, u_6, u_7, u_8} (κ := κ) (fun (x : ι → α) ↦ C ((⇑eα : (a : α) → α') ∘ x ∘ (⇑eι.symm : (a : ι') → ι))) l
have simp : (∃ (c : κ),
    ∀ (x : η' → α'),
      (C fun (x_1 : ι') ↦
          (eα : (a : α) → α')
            (Sum.elim id ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
              (l.idxFun ((eι.symm : (a : ι') → ι) x_1)))) =
        c) ↔
  ∃ (c : κ),
    ∀ (x : η → α), C ((⇑eα : (a : α) → α') ∘ (↑l : (x : η → α) → (i : ι) → α) x ∘ (⇑eι.symm : (a : ι') → ι)) = c
Tactic: simp only [IsMono, funext (reindex_apply _ _ _ _ _), coe_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono.{u_9, u_10, u_11, u_8} (κ := κ) (fun (x : ι' → α') ↦ C ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eι : (a : ι) → ι')))
    (l.reindex eη eα eι)
have simp : IsMono.{u_5, u_6, u_7, u_8} (κ := κ)
  (fun (x : ι → α) ↦
    C (comp.{u_7 + 1, u_10 + 1, u_6 + 1} (β := α') (⇑eα.symm : (a : α') → α) ((⇑eα : (a : α) → α') ∘ x)))
  l
Tactic: simp [reindex_isMono, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
hlm : (↑l : (x : α) → (i : ι) → α) = (↑m : (x : α) → (i : ι) → α)
⊢ l = m
have idxFun : ∀ (i : ι) (a : α), l.idxFun i = some a ↔ m.idxFun i = some a
Tactic: ext i a
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
hlm : (↑l : (x : α) → (i : ι) → α) = (↑m : (x : α) → (i : ι) → α)
i : ι
a : α
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
have idxFun : ∀ (b : α) (hba : b ≠ a), l.idxFun i = some a ↔ m.idxFun i = some a
Tactic: obtain ⟨b, hba⟩ := exists_ne a
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (hypothesis)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
hlm : (↑l : (x : α) → (i : ι) → α) = (↑m : (x : α) → (i : ι) → α)
i : ι
a b : α
hba : b ≠ a
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
have hlm₁ : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
Tactic: simp only [funext_iff] at hlm ⊢
Cleared hypotheses: hlm
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
have idxFun : ∀ (h : l.idxFun i = some a), m.idxFun i = some a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
idxFun : ∀ (h : l.idxFun i = some a), m.idxFun i = some a
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
have idxFun₁ : ∀ (h : m.idxFun i = some a), l.idxFun i = some a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
h : l.idxFun i = some a
⊢ m.idxFun i = some a
have idxFun : ∀ (hi : m.idxFun i = none), none = some a
Tactic: cases hi : idxFun m i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
h : l.idxFun i = some a
idxFun : ∀ (hi : m.idxFun i = none), none = some a
⊢ m.idxFun i = some a
have idxFun₁ : ∀ (val : α) (hi : m.idxFun i = some val), some val = some a
Tactic: cases hi : idxFun m i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
h : m.idxFun i = some a
⊢ l.idxFun i = some a
have idxFun : ∀ (hi : l.idxFun i = none), none = some a
Tactic: cases hi : idxFun l i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1
h : m.idxFun i = some a
idxFun : ∀ (hi : l.idxFun i = none), none = some a
⊢ l.idxFun i = some a
have idxFun₁ : ∀ (val : α) (hi : l.idxFun i = some val), some val = some a
Tactic: cases hi : idxFun l i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a = (↑l : (x : α) → (i : ι) → α) (a ())
have h : ∀ (i : ι), (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
have h : ∀ (h : l.idxFun i = none),
  (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
Tactic: cases h : l.idxFun i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
h :
  ∀ (h : l.idxFun i = none),
    (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
have h₁ : ∀ (val : α) (h : l.idxFun i = some val),
  (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
Tactic: cases h : l.idxFun i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l
have simp : (∃ (c : κ), ∀ (x : Unit → α), C ((↑l : (x : α) → (i : ι) → α) (x ())) = c) ↔
  ∃ (c : κ), ∀ (x : α), C ((↑l : (x : α) → (i : ι) → α) x) = c
Tactic: simp only [Subspace.IsMono, toSubspaceUnit_apply, IsMono]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2
have none : ∀ (h : l.idxFun ie.1 = none),
  (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2
Tactic: cases h : l.idxFun ie.1
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
none :
  ∀ (h : l.idxFun ie.1 = Option.none),
    (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2
⊢ (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2
have some : ∀ (val : η → α) (h : l.idxFun ie.1 = some val),
  (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2
Tactic: cases h : l.idxFun ie.1
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
η : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
l : Line α_1 ι_1
i : ι_1
a x : α_1
α : Type u_5
ι : Type u_6
κ : Type u_7
C : (ι → Option α) → κ
⊢ Inhabited (ColorFocused C)
have refine : ∀ (h : AlmostMono C),
  Membership.mem (γ := Multiset (AlmostMono C)) 0 h →
    (↑h.line : (x : Option α) → (i : ι) → Option α) none = fun (x : ι) ↦ none
Tactic: refine ⟨⟨0, fun _ => none, fun h => ?_, Multiset.nodup_zero⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x)
have h : ∀ (i : ι ⊕ ι'), (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) i
have h : ∀ (val : ι),
  (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inl val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
h :
  ∀ (val : ι),
    (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
      Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inl val)
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) i
have h₁ : ∀ (val : ι'),
  (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inr val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v
have h : ∀ (i : ι ⊕ ι'), (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v i
have h : ∀ (val : ι),
  (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inl val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
h :
  ∀ (val : ι),
    (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
      Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inl val)
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v i
have h₁ : ∀ (val : ι'),
  (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inr val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x)
have h : ∀ (i : ι ⊕ ι'),
  (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x i =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x i =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) i
have h : ∀ (val : ι),
  (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inl val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
h :
  ∀ (val : ι),
    (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
      Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inl val)
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x i =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) i
have h₁ : ∀ (val : ι'),
  (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inr val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α : Type u_5
ι : Type u_6
inst : Nonempty ι
x : α
⊢ (↑(diagonal α ι) : (x : α) → (i : ι) → α) x = fun (x_1 : ι) ↦ x
have h : ∀ (x_1 : ι), (↑(diagonal α ι) : (x : α) → (i : ι) → α) x x_1 = x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α α' : Type u
e : α ≃ α'
κ : Type (max v u)
h_1 : Finite κ
ι : Type
x_1 : Fintype ι
h : ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
C : (ι → α') → κ
l : Line α ι
c : κ
lc : ∀ (x : α), (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x) = c
x : α
⊢ C ((↑(map (⇑e : (a : α) → α') l) : (x : α') → (i : ι) → α') ((e : (a : α) → α') x)) = c
have rw : C ((↑(map (⇑e : (a : α) → α') l) : (x : α') → (i : ι) → α') ((e : (a : α) → α') x)) =
  (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x)
Tactic: rw [← lc x, Line.map_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
α α' : Type u
e : α ≃ α'
κ : Type (max v u)
h_1 : Finite κ
ι : Type
x_1 : Fintype ι
h : ∀ (C : (ι → α) → κ), ∃ (l : Line α ι), IsMono C l
C : (ι → α') → κ
l : Line α ι
c : κ
lc : ∀ (x : α), (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x) = c
x : α
rw :
  C ((↑(map (⇑e : (a : α) → α') l) : (x : α') → (i : ι) → α') ((e : (a : α) → α') x)) =
    (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x)
⊢ C ((↑(map (⇑e : (a : α) → α') l) : (x : α') → (i : ι) → α') ((e : (a : α) → α') x)) = c
have rw₁ : C ((⇑e : (a : α) → α') ∘ (↑l : (x : α) → (i : ι) → α) x) =
  (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x)
Tactic: rw [← lc x, Line.map_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
κ : Type (max v u)
inst : Finite κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
have pos : ∀ (h : Nonempty κ),
  ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
Tactic: by_cases h : Nonempty κ
-- Lean 4 proof step from Mathlib.Combinatorics.HalesJewett (goal)
Goal:
κ : Type (max v u)
inst : Finite κ
pos :
  ∀ (h : Nonempty κ),
    ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
have neg : ∀ (h : ¬Nonempty κ),
  ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
Tactic: by_cases h : Nonempty κ
-- 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 κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have intro : ∀ (val : Fintype κ), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
Tactic: cases nonempty_fintype κ
-- 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 κ
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have pos : ∀ (h : Nonempty α), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
Tactic: by_cases h : Nonempty α
-- 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 κ
pos :
  ∀ (h : Nonempty α), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have by_cases : ∀ (h : ¬Nonempty α), ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
Tactic: by_cases h : Nonempty α
-- 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 refine : ∀ (C : (Unit → Option α) → κ) (x : Option α),
  C ((↑(diagonal (Option α) Unit) : (x : Option α) → (i : Unit) → Option α) x) = C fun (x : Unit) ↦ none
Tactic: refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
-- 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) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have 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
Tactic: obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
-- 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
⊢ ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ (l : Line (Option α) ι), IsMono C l
have refine : ∀ (C : (ι → Option α) → κ), ¬∃ (s : ColorFocused C), s.lines.card = Fintype.card κ + 1
Tactic: refine ⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩
-- 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
⊢ False
have apply : (Fintype.card κ).succ ≤ Fintype.card κ
Tactic: apply Nat.not_succ_le_self (Fintype.card κ)
-- 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
⊢ (Fintype.card κ).succ ≤ Fintype.card κ
have rw : #{ val := Multiset.map AlmostMono.color s.lines, nodup := sorry : Finset κ } ≤ Fintype.card κ
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 α
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)
⊢ (Fintype.card κ).succ ≤ Fintype.card κ
have rw₂ : (Multiset.map AlmostMono.color s.lines).Nodup
Tactic: rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]