awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.HalesJewett
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 : ι'
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:
simp [h, reindex, coe_apply]

Premises used: Combinatorics.Subspace.reindex, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
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 : ι'
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:
simp [h, reindex, coe_apply]

Premises used: Combinatorics.Subspace.reindex, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
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 : (ι' → α') → κ
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
⊢ 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

Tactic:
simp only [IsMono, funext (reindex_apply _ _ _ _ _), coe_apply]

Premises used: Combinatorics.Subspace.IsMono, funext, Combinatorics.Subspace.coe_apply, Combinatorics.Subspace.reindex_apply
-- Module: Mathlib.Combinatorics.HalesJewett
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 : (ι' → α') → κ
c : κ
⊢ ∀ (a : η' → α'),
    (C fun (x : ι') ↦
          (eα : (a : α) → α')
            (Sum.elim id ((⇑eα.symm : (a : α') → α) ∘ a ∘ (⇑eη : (a : η) → η'))
              (l.idxFun ((eι.symm : (a : ι') → ι) x)))) =
        c ↔
      C
          ((⇑eα : (a : α) → α') ∘
            (↑l : (x : η → α) → (i : ι) → α) (((eη.arrowCongr eα).symm : (a : η' → α') → η → α) a) ∘
              (⇑eι.symm : (a : ι') → ι)) =
        c

Tactic:
aesop
-- Module: Mathlib.Combinatorics.HalesJewett
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 : (ι' → α') → κ
⊢ (∃ (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:
exact exists_congr fun c ↦ (eη.arrowCongr eα).symm.forall_congr <| by aesop

Premises used: Equiv.arrowCongr, exists_congr, Equiv.forall_congr, Equiv.symm
-- Module: Mathlib.Combinatorics.HalesJewett
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
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
⊢ IsMono.{u_9, u_10, u_11, u_8} (κ := κ) (fun (x : ι' → α') ↦ C ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eι : (a : ι) → ι')))
    (l.reindex eη eα eι)

Tactic:
simp [reindex_isMono, Function.comp_assoc]

Premises used: Combinatorics.Subspace.reindex_isMono, Function.comp_assoc
-- Module: Mathlib.Combinatorics.HalesJewett
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_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:
simpa [← Function.comp_assoc]

Premises used: Function.comp_assoc
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
x : α
i : ι
⊢ (↑l : (x : α) → (i : ι) → α) x i = (l.idxFun i).getD x

Tactic:
rfl

Premises used: Combinatorics.Line.toFun, rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
hlm : (↑l : (x : α) → (i : ι) → α) = (↑m : (x : α) → (i : ι) → α)
idxFun : ∀ (i : ι) (a : α), l.idxFun i = some a ↔ m.idxFun i = some a
⊢ l = m

Tactic:
ext i a
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
inst : Nontrivial α
l m : Line α ι
hlm : (↑l : (x : α) → (i : ι) → α) = (↑m : (x : α) → (i : ι) → α)
i : ι
a : α
idxFun : ∀ (b : α) (hba : b ≠ a), l.idxFun i = some a ↔ m.idxFun i = some a
⊢ l.idxFun i = some a ↔ m.idxFun i = some a

Tactic:
obtain ⟨b, hba⟩ := exists_ne a

Premises used: exists_ne
-- Module: Mathlib.Combinatorics.HalesJewett
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
⊢ ∀ (x : α) (x_1 : ι), (↑l : (x : α) → (i : ι) → α) x x_1 = (↑m : (x : α) → (i : ι) → α) x x_1

Tactic:
simp only [funext_iff] at hlm ⊢

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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.HalesJewett
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
idxFun₁ : ∀ (h : m.idxFun i = some a), l.idxFun i = some a
⊢ l.idxFun i = some a ↔ m.idxFun i = some a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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
idxFun₁ : ∀ (val : α) (hi : m.idxFun i = some val), some val = some a
⊢ m.idxFun i = some a

Tactic:
cases hi : idxFun m i

Premises used: Combinatorics.Line.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
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
hi : m.idxFun i = none
⊢ none = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.HalesJewett
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
val : α
hi : m.idxFun i = some val
⊢ some val = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.HalesJewett
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
idxFun₁ : ∀ (val : α) (hi : l.idxFun i = some val), some val = some a
⊢ l.idxFun i = some a

Tactic:
cases hi : idxFun l i

Premises used: Combinatorics.Line.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
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
hi : l.idxFun i = none
⊢ none = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.HalesJewett
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
val : α
hi : l.idxFun i = some val
⊢ some val = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l_1 : Line α ι
i_1 : ι
a x : α
l : Line α ι
x_1 : Unit
i : ι
hi : l.idxFun i = none
⊢ (l.idxFun i).elim (Sum.inr ()) Sum.inl = Sum.inr x_1

Tactic:
simp [hi]
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
h : ∀ (i : ι), (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a = (↑l : (x : α) → (i : ι) → α) (a ())

Tactic:
ext i
-- Module: Mathlib.Combinatorics.HalesJewett
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
h₁ :
  ∀ (val : α) (h : l.idxFun i = some val),
    (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i

Tactic:
cases h : l.idxFun i

Premises used: Combinatorics.Line.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
h : l.idxFun i = none
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i

Tactic:
simp [toSubspaceUnit, h, Subspace.coe_apply]

Premises used: Combinatorics.Line.toSubspaceUnit, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
val : α
h : l.idxFun i = some val
⊢ (↑l.toSubspaceUnit : (x : Unit → α) → (i : ι) → α) a i = (↑l : (x : α) → (i : ι) → α) (a ()) i

Tactic:
simp [toSubspaceUnit, h, Subspace.coe_apply]

Premises used: Combinatorics.Line.toSubspaceUnit, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
simp :
  (∃ (c : κ), ∀ (x : Unit → α), C ((↑l : (x : α) → (i : ι) → α) (x ())) = c) ↔
    ∃ (c : κ), ∀ (x : α), C ((↑l : (x : α) → (i : ι) → α) x) = c
⊢ Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l

Tactic:
simp only [Subspace.IsMono, toSubspaceUnit_apply, IsMono]

Premises used: Combinatorics.Subspace.IsMono, Combinatorics.Line.toSubspaceUnit_apply, Combinatorics.Line.IsMono
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ (∃ (c : κ), ∀ (x : Unit → α), C ((↑l : (x : α) → (i : ι) → α) (x ())) = c) ↔
    ∃ (c : κ), ∀ (x : α), C ((↑l : (x : α) → (i : ι) → α) x) = c

Tactic:
exists_congr fun c ↦ ⟨fun h a ↦ h fun _ ↦ a, fun h a ↦ h _⟩

Premises used: Unit.unit, exists_congr, Iff.intro
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ (∃ (c : κ), ∀ (x : Unit → α), C ((↑l : (x : α) → (i : ι) → α) (x ())) = c) ↔
    ∃ (c : κ), ∀ (x : α), C ((↑l : (x : α) → (i : ι) → α) x) = c

Tactic:
exact exists_congr fun c ↦ ⟨fun h a ↦ h fun _ ↦ a, fun h a ↦ h _⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l_1 : Line α ι
i_1 : ι
a x : α
l : Line (η → α) ι
e : η
i : ι
hi : l.idxFun i = none
⊢ Eq (α := α ⊕ η) ((l.idxFun (i, e).1).elim (Sum.inr (i, e).2) fun (f : η → α) ↦ Sum.inl (f (i, e).2)) (Sum.inr e)

Tactic:
simp [hi]
-- Module: Mathlib.Combinatorics.HalesJewett
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
some :
  ∀ (val : η → α) (h : l.idxFun ie.1 = Option.some val),
    (↑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

Tactic:
cases h : l.idxFun ie.1

Premises used: Prod.fst, Combinatorics.Line.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
h : l.idxFun ie.1 = none
⊢ (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2

Tactic:
simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Premises used: Combinatorics.Line.toSubspace, Combinatorics.Line.coe_apply, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
val : η → α
h : l.idxFun ie.1 = some val
⊢ (↑l.toSubspace : (x : η → α) → (i : ι × η) → α) a ie = (↑l : (x : η → α) → (i : ι) → η → α) a ie.1 ie.2

Tactic:
simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Premises used: Combinatorics.Line.toSubspace, Combinatorics.Line.coe_apply, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line (η → α) ι
C : (ι × η → α) → κ
⊢ Subspace.IsMono C l.toSubspace ↔
    IsMono (κ := κ)
      (fun (x : ι → η → α) ↦
        C fun (x_1 : ι × η) ↦
          match (motive := ι × η → α) x_1 with
          | (i, e) => x i e)
      l

Tactic:
simp [Subspace.IsMono, IsMono, funext (toSubspace_apply _ _)]

Premises used: Combinatorics.Subspace.IsMono, funext, Combinatorics.Line.IsMono, Combinatorics.Line.toSubspace_apply
-- Module: Mathlib.Combinatorics.HalesJewett
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 α) → κ
refine :
  ∀ (h : AlmostMono C),
    Membership.mem (γ := Multiset (AlmostMono C)) 0 h →
      (↑h.line : (x : Option α) → (i : ι) → Option α) none = fun (x : ι) ↦ none
⊢ Inhabited (ColorFocused C)

Tactic:
refine ⟨⟨0, fun _ => none, fun h => ?_, Multiset.nodup_zero⟩⟩
-- Module: Mathlib.Combinatorics.HalesJewett
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 α) → κ
h : AlmostMono C
⊢ Membership.mem (γ := Multiset (AlmostMono C)) 0 h →
    (↑h.line : (x : Option α) → (i : ι) → Option α) none = fun (x : ι) ↦ none

Tactic:
simp only [Multiset.notMem_zero, IsEmpty.forall_iff]

Premises used: Multiset.notMem_zero, IsEmpty.forall_iff
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ : Type u_4
l_1 : Line α_1 ι_1
i : ι_1
a x : α_1
α : Type u_5
α' : Type u_6
ι : Type u_7
f : α → α'
l : Line α ι
⊢ Option.map f (l.idxFun (⋯.choose (p := fun (i : ι) ↦ l.idxFun i = none))) = none

Tactic:
simp only [l.proper.choose_spec, Option.map_none]

Premises used: Exists.choose_spec, Combinatorics.Line.proper, Option.map_none
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
x : α
⊢ (↑l : (x : α) → (i : ι) → α) x = fun (i : ι) ↦ (l.idxFun i).getD x

Tactic:
rfl

Premises used: Combinatorics.Line.toFun, rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
l : Line α ι
x : α
i : ι
h : l.idxFun i = none
⊢ (↑l : (x : α) → (i : ι) → α) x i = x

Tactic:
simp only [Option.getD_none, h, l.apply_def]

Premises used: Combinatorics.Line.apply_def, Option.getD_none
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_2
ι : Type u_3
l : Line α ι
i : ι
a x : α
h : l.idxFun i = some a
⊢ (↑l : (x : α) → (i : ι) → α) x i = a

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
α' : Type u_6
ι : Type u_7
f : α → α'
l : Line α ι
x : α
⊢ (↑(map f l) : (x : α') → (i : ι) → α') (f x) = f ∘ (↑l : (x : α) → (i : ι) → α) x

Tactic:
simp only [Line.apply_def, Line.map, Option.getD_map, comp_def]

Premises used: Combinatorics.Line.map, Function.comp_def, Option.getD_map, Combinatorics.Line.apply_def
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
h : ∀ (i : ι ⊕ ι'), (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) i
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x)

Tactic:
funext i
-- Module: Mathlib.Combinatorics.HalesJewett
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)
h₁ :
  ∀ (val : ι'),
    (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
      Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inr val)
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) i

Tactic:
cases i
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val : ι
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val : ι'
⊢ (↑(vertical v l) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim v ((↑l : (x : α) → (i : ι') → α) x) (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
h : ∀ (i : ι ⊕ ι'), (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v i
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v

Tactic:
funext i
-- Module: Mathlib.Combinatorics.HalesJewett
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)
h₁ :
  ∀ (val : ι'),
    (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
      Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inr val)
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x i = Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v i

Tactic:
cases i
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val : ι
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val : ι'
⊢ (↑(l.horizontal v) : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) v (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
h :
  ∀ (i : ι ⊕ ι'),
    (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x i =
      Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) i
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x)

Tactic:
funext i
-- Module: Mathlib.Combinatorics.HalesJewett
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)
h₁ :
  ∀ (val : ι'),
    (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
      Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inr val)
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x i =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) i

Tactic:
cases i
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val : ι
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inl val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val : ι'
⊢ (↑(l.prod l') : (x : α) → (i : ι ⊕ ι') → α) x (Sum.inr val) =
    Sum.elim ((↑l : (x : α) → (i : ι) → α) x) ((↑l' : (x : α) → (i : ι') → α) x) (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
inst : Nonempty ι
x : α
h : ∀ (x_1 : ι), (↑(diagonal α ι) : (x : α) → (i : ι) → α) x x_1 = x
⊢ (↑(diagonal α ι) : (x : α) → (i : ι) → α) x = fun (x_1 : ι) ↦ x

Tactic:
ext
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
α : Type u_5
ι : Type u_6
inst : Nonempty ι
x : α
x_1 : ι
⊢ (↑(diagonal α ι) : (x : α) → (i : ι) → α) x x_1 = x

Tactic:
simp [diagonal]

Premises used: Combinatorics.Line.diagonal
-- Module: Mathlib.Combinatorics.HalesJewett
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)
rw₁ rw₂ :
  C ((⇑e : (a : α) → α') ∘ (↑l : (x : α) → (i : ι) → α) x) =
    (fun (v : ι → α) ↦ C ((⇑e : (a : α) → α') ∘ v)) ((↑l : (x : α) → (i : ι) → α) x)
⊢ C ((↑(map (⇑e : (a : α) → α') l) : (x : α') → (i : ι) → α') ((e : (a : α) → α') x)) = c

Tactic:
rw [← lc x, Line.map_apply]

Premises used: Combinatorics.Line.map_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
κ : Type (max v u)
_ :
  ∀ [Finite κ],
    ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l
⊢ ∀ [Finite κ],
    ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ (l : Line PEmpty.{u + 1} ι), IsMono C l

Tactic:
_
-- Module: Mathlib.Combinatorics.HalesJewett
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
neg :
  ∀ (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

Tactic:
by_cases h : Nonempty κ

Premises used: Nonempty