[GOAL]
α : Type ?u.3173
ι : Type ?u.3179
κ : Type ?u.3180
C : (ι → Option α) → κ
⊢ Inhabited (ColorFocused C)
[PROOFSTEP]
refine' ⟨⟨0, fun _ => none, fun h => _, Multiset.nodup_zero⟩⟩
[GOAL]
α : Type ?u.3173
ι : Type ?u.3179
κ : Type ?u.3180
C : (ι → Option α) → κ
h : AlmostMono C
⊢ h ∈ 0 → (fun x i => Option.getD (idxFun h.line i) x) none = fun x => none
[PROOFSTEP]
simp only [Multiset.not_mem_zero, IsEmpty.forall_iff]
[GOAL]
α : Type ?u.3673
α' : Type ?u.3677
ι : Type ?u.3674
f : α → α'
l : Line α ι
⊢ (fun i => Option.map f (idxFun l i)) (Exists.choose (_ : ∃ i, idxFun l i = none)) = none
[PROOFSTEP]
simp only [l.proper.choose_spec, Option.map_none']
[GOAL]
α : Type u_1
ι : Type u_2
l : Line α ι
x : α
i : ι
h : idxFun l i = none
⊢ (fun x i => Option.getD (idxFun l i) x) x i = x
[PROOFSTEP]
simp only [Option.getD_none, h, l.apply]
[GOAL]
α : Type u_1
ι : Type u_2
l : Line α ι
x : α
i : ι
h : idxFun l i ≠ none
⊢ some ((fun x i => Option.getD (idxFun l i) x) x i) = idxFun l i
[PROOFSTEP]
rw [l.apply, Option.getD_of_ne_none h]
[GOAL]
α : Type u_1
α' : Type u_2
ι : Type u_3
f : α → α'
l : Line α ι
x : α
⊢ (fun x i => Option.getD (idxFun (map f l) i) x) (f x) = f ∘ (fun x i => Option.getD (idxFun l i) x) x
[PROOFSTEP]
simp only [Line.apply, Line.map, Option.getD_map]
[GOAL]
α : Type u_1
α' : Type u_2
ι : Type u_3
f : α → α'
l : Line α ι
x : α
⊢ (fun i => f (Option.getD (idxFun l i) x)) = f ∘ fun i => Option.getD (idxFun l i) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x = Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x)
[PROOFSTEP]
funext i
[GOAL]
case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x i = Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x) i
[PROOFSTEP]
cases i
[GOAL]
case h.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
val✝ : ι
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x (Sum.inl val✝) =
    Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
v : ι → α
l : Line α ι'
x : α
val✝ : ι'
⊢ (fun x i => Option.getD (idxFun (vertical v l) i) x) x (Sum.inr val✝) =
    Sum.elim v ((fun x i => Option.getD (idxFun l i) x) x) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
v : ι' → α
x : α
⊢ (fun x i => Option.getD (idxFun (horizontal l v) i) x) x = Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) v
[PROOFSTEP]
funext i
[GOAL]
case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (horizontal l v) i) x) x i = Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) v i
[PROOFSTEP]
cases i
[GOAL]
case h.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
v : ι' → α
x : α
val✝ : ι
⊢ (fun x i => Option.getD (idxFun (horizontal l v) i) x) x (Sum.inl val✝) =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) v (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
v : ι' → α
x : α
val✝ : ι'
⊢ (fun x i => Option.getD (idxFun (horizontal l v) i) x) x (Sum.inr val✝) =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) v (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x)
[PROOFSTEP]
funext i
[GOAL]
case h
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x i =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x) i
[PROOFSTEP]
cases i
[GOAL]
case h.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x (Sum.inl val✝) =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι'
⊢ (fun x i => Option.getD (idxFun (prod l l') i) x) x (Sum.inr val✝) =
    Sum.elim ((fun x i => Option.getD (idxFun l i) x) x) ((fun x i => Option.getD (idxFun l' i) x) x) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
x : α
⊢ (fun x i => Option.getD (idxFun (diagonal α ι) i) x) x = fun x_1 => x
[PROOFSTEP]
simp_rw [Line.diagonal, Option.getD_none]
[GOAL]
α α' : Type u
e : α ≃ α'
κ : Type (max v u)
x✝¹ : Finite κ
ι : Type
x✝ : Fintype ι
h : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (ι → α') → κ
l : Line α ι
c : κ
lc : ∀ (x : α), (fun v => C (↑e ∘ v)) ((fun x i => Option.getD (idxFun l i) x) x) = c
x : α
⊢ C ((fun x i => Option.getD (idxFun (map (↑e) l) i) x) (↑e x)) = c
[PROOFSTEP]
rw [← lc x, Line.map_apply]
[GOAL]
⊢ ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → PEmpty) → κ), ∃ l, IsMono C l
[PROOFSTEP]
intro κ _
[GOAL]
κ : Type (max v u)
inst✝ : Finite κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty) → κ), ∃ l, IsMono C l
[PROOFSTEP]
by_cases h : Nonempty κ
[GOAL]
case pos
κ : Type (max v u)
inst✝ : Finite κ
h : Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty) → κ), ∃ l, IsMono C l
[PROOFSTEP]
refine' ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩
[GOAL]
case neg
κ : Type (max v u)
inst✝ : Finite κ
h : ¬Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty) → κ), ∃ l, IsMono C l
[PROOFSTEP]
exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩
[GOAL]
⊢ ∀ {α : Type u} [inst : Fintype α],
    (∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) →
      ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
intro α _ ihα κ _
[GOAL]
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
cases nonempty_fintype κ
[GOAL]
case intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
by_cases h : Nonempty α
[GOAL]
case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
case neg
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
case neg =>
  refine' ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
  rintro (_ | ⟨a⟩)
  · rfl
  · exact (h ⟨a⟩).elim
[GOAL]
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
case neg =>
  refine' ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
  rintro (_ | ⟨a⟩)
  · rfl
  · exact (h ⟨a⟩).elim
[GOAL]
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
refine' ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
[GOAL]
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
C : (Unit → Option α) → κ
⊢ ∀ (x : Option α), C ((fun x i => Option.getD (idxFun (diagonal (Option α) Unit) i) x) x) = C fun x => none
[PROOFSTEP]
rintro (_ | ⟨a⟩)
[GOAL]
case none
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
C : (Unit → Option α) → κ
⊢ C ((fun x i => Option.getD (idxFun (diagonal (Option α) Unit) i) x) none) = C fun x => none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
C : (Unit → Option α) → κ
a : α
⊢ C ((fun x i => Option.getD (idxFun (diagonal (Option α) Unit) i) x) (some a)) = C fun x => none
[PROOFSTEP]
exact (h ⟨a⟩).elim
[GOAL]
case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
suffices key :
  ∀ r : ℕ,
    ∃ (ι : Type) (_ : Fintype ι),
      ∀ C : (ι → Option α) → κ, (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
[GOAL]
case pos
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
[GOAL]
case pos.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
[PROOFSTEP]
refine' ⟨ι, _inst, fun C => (hι C).resolve_left _⟩
[GOAL]
case pos.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
⊢ ¬∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1
[PROOFSTEP]
rintro ⟨s, sr⟩
[GOAL]
case pos.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ False
[PROOFSTEP]
apply Nat.not_succ_le_self (Fintype.card κ)
[GOAL]
case pos.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ Nat.succ (Fintype.card κ) ≤ Fintype.card κ
[PROOFSTEP]
rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
[GOAL]
case pos.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ Finset.card { val := Multiset.map ?pos.intro.intro.intro.f✝ s.lines, nodup := ?m.16664 } ≤ Fintype.card κ
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ Type ?u.16661
case pos.intro.intro.intro.f
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ AlmostMono C → ?m.16662
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ Multiset.Nodup (Multiset.map ?pos.intro.intro.intro.f✝ s.lines)
case pos.intro.intro.intro.f
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : ↑Multiset.card s.lines = Fintype.card κ + 1
⊢ AlmostMono C → ?m.16662
[PROOFSTEP]
exact
  Finset.card_le_univ
    ⟨_, s.distinct_colors⟩
      -- We now prove the key claim, by induction on `r`.
[GOAL]
case key
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
intro r
[GOAL]
case key
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
induction' r with r ihr
[GOAL]
case key.zero
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.zero) ∨ ∃ l, IsMono C l
[PROOFSTEP]
exact
  ⟨Empty, inferInstance, fun C => Or.inl ⟨default, Multiset.card_zero⟩⟩
    -- Supposing the key claim holds for `r`, we need to show it for `r+1`. First pick a high
        -- enough dimension `ι` for `r`.
[GOAL]
case key.succ
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ihr : ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
obtain ⟨ι, _inst, hι⟩ := ihr
[GOAL]
case key.succ.intro.intro
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
specialize ihα ((ι → Option α) → κ)
[GOAL]
case key.succ.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ihα : ∃ ι_1 x, ∀ (C : (ι_1 → α) → (ι → Option α) → κ), ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
obtain ⟨ι', _inst, hι'⟩ := ihα
[GOAL]
case key.succ.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
refine' ⟨Sum ι ι', inferInstance, _⟩
[GOAL]
case key.succ.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ l, IsMono C l
⊢ ∀ (C : (ι ⊕ ι' → Option α) → κ), (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
intro C
[GOAL]
case key.succ.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
hι' : ∀ (C : (ι' → α) → (ι → Option α) → κ), ∃ l, IsMono C l
C : (ι ⊕ ι' → Option α) → κ
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
specialize
  hι' fun v' v =>
    C
      (Sum.elim v (some ∘ v'))
        -- By choice of `ι'` this coloring has a monochromatic line `l'` with color class `C'`, where
            -- `C'` is a `κ`-coloring of `ι → α`.
[GOAL]
case key.succ.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
hι' : ∃ l, IsMono (fun v' v => C (Sum.elim v (some ∘ v'))) l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
obtain ⟨l', C', hl'⟩ := hι'
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
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']
    -- By choice of `ι`, `C'` either has `r` color-focused lines or a monochromatic line.
[GOAL]
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
⊢ (∃ l, IsMono C' l) → ∃ l, IsMono C l
[PROOFSTEP]
rintro ⟨l, c, hl⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
l : Line (Option α) ι
c : κ
hl : ∀ (x : Option α), C' ((fun x i => Option.getD (idxFun l i) x) x) = c
⊢ ∃ l, IsMono C l
[PROOFSTEP]
refine' ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => _⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
l : Line (Option α) ι
c : κ
hl : ∀ (x : Option α), C' ((fun x i => Option.getD (idxFun l i) x) x) = c
x : Option α
⊢ C
      ((fun x i =>
          Option.getD
            (idxFun (horizontal l (some ∘ (fun x i => Option.getD (idxFun l' i) x) (Classical.arbitrary α))) i) x)
        x) =
    c
[PROOFSTEP]
rw [Line.horizontal_apply, ← hl, ← hl']
  -- By choice of `ι`, `C'` either has `r` color-focused lines or a monochromatic line.
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
specialize hι C'
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
hι : (∃ s, ↑Multiset.card s.lines = r) ∨ ∃ l, IsMono C' l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
rcases hι with (⟨s, sr⟩ | h)
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro.inl.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
case key.succ.intro.intro.intro.intro.intro.intro.inr
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
h : ∃ l, IsMono C' l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
on_goal 2 =>
  exact
    Or.inr
      (mono_of_mono h)
        -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether
            -- one of these `r` lines has the same color as the focus point.
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro.inl.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
case key.succ.intro.intro.intro.intro.intro.intro.inr
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
h : ∃ l, IsMono C' l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
on_goal 2 =>
  exact
    Or.inr
      (mono_of_mono h)
        -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether
            -- one of these `r` lines has the same color as the focus point.
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro.inr
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
h : ∃ l, IsMono C' l
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
exact
  Or.inr
    (mono_of_mono h)
      -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether
          -- one of these `r` lines has the same color as the focus point.
[GOAL]
case key.succ.intro.intro.intro.intro.intro.intro.inl.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
by_cases h : ∃ p ∈ s.lines, (p : AlmostMono _).color = C' s.focus
[GOAL]
case pos
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
obtain ⟨p, p_mem, hp⟩ := h
[GOAL]
case pos.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
refine' Or.inr (mono_of_mono ⟨p.line, p.color, _⟩)
[GOAL]
case pos.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ ∀ (x : Option α), C' ((fun x i => Option.getD (idxFun p.line i) x) x) = p.color
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case pos.intro.intro.none
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ C' ((fun x i => Option.getD (idxFun p.line i) x) none) = p.color
case pos.intro.intro.some
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝¹ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
val✝ : α
⊢ C' ((fun x i => Option.getD (idxFun p.line i) x) (some val✝)) = p.color
[PROOFSTEP]
rw [hp, s.is_focused p p_mem]
[GOAL]
case pos.intro.intro.some
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝¹ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
val✝ : α
⊢ C' ((fun x i => Option.getD (idxFun p.line i) x) (some val✝)) = p.color
[PROOFSTEP]
apply p.has_color
[GOAL]
case neg
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ (∃ s, ↑Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l
[PROOFSTEP]
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), _, _⟩,
      _⟩
      -- Porting note: Needed to reorder the following two goals
          -- The product lines are almost monochromatic.
[GOAL]
case neg.refine'_1
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ AlmostMono C' → AlmostMono C
[PROOFSTEP]
refine' fun p => ⟨p.line.prod (l'.map some), p.color, fun x => _⟩
[GOAL]
case neg.refine'_1
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color
[PROOFSTEP]
rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
  -- The vertical line is almost monochromatic.
[GOAL]
case neg.refine'_2
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
x : α
⊢ C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) = C' s.focus
[PROOFSTEP]
rw [vertical_apply, ← congr_fun (hl' x), Line.map_apply]
  -- Our `r+1` lines have the same endpoint.
[GOAL]
case neg.refine'_3
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ ∀ (p : AlmostMono C),
    p ∈
        { line := vertical s.focus (map some l'), color := C' s.focus,
            has_color :=
              (_ :
                ∀ (x : α),
                  C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                    C' s.focus) } ::ₘ
          Multiset.map
            (fun p =>
              { line := prod p.line (map some l'), color := p.color,
                has_color :=
                  (_ :
                    ∀ (x : α),
                      C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color) })
            s.lines →
      (fun x i => Option.getD (idxFun p.line i) x) none =
        Sum.elim s.focus ((fun x i => Option.getD (idxFun (map some l') i) x) none)
[PROOFSTEP]
simp_rw [Multiset.mem_cons, Multiset.mem_map]
[GOAL]
case neg.refine'_3
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ ∀ (p : AlmostMono C),
    (p =
          { line := vertical s.focus (map some l'), color := C' s.focus,
            has_color :=
              (_ :
                ∀ (x : α),
                  C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) = C' s.focus) } ∨
        ∃ a,
          a ∈ s.lines ∧
            { line := prod a.line (map some l'), color := a.color,
                has_color :=
                  (_ :
                    ∀ (x : α),
                      C ((fun x i => Option.getD (idxFun (prod a.line (map some l')) i) x) (some x)) = a.color) } =
              p) →
      (fun i => Option.getD (idxFun p.line i) none) =
        Sum.elim s.focus fun i => Option.getD (idxFun (map some l') i) none
[PROOFSTEP]
rintro _ (rfl | ⟨q, hq, rfl⟩)
[GOAL]
case neg.refine'_3.inl
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ (fun i =>
      Option.getD
        (idxFun
          { line := vertical s.focus (map some l'), color := C' s.focus,
              has_color :=
                (_ :
                  ∀ (x : α),
                    C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                      C' s.focus) }.line
          i)
        none) =
    Sum.elim s.focus fun i => Option.getD (idxFun (map some l') i) none
[PROOFSTEP]
simp only [vertical_apply]
[GOAL]
case neg.refine'_3.inr.intro.intro
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
q : AlmostMono C'
hq : q ∈ s.lines
⊢ (fun i =>
      Option.getD
        (idxFun
          { line := prod q.line (map some l'), color := q.color,
              has_color :=
                (_ :
                  ∀ (x : α),
                    C ((fun x i => Option.getD (idxFun (prod q.line (map some l')) i) x) (some x)) = q.color) }.line
          i)
        none) =
    Sum.elim s.focus fun i => Option.getD (idxFun (map some l') i) none
[PROOFSTEP]
simp only [prod_apply, s.is_focused q hq]
  -- Our `r+1` lines have distinct colors (this is why we needed to split into cases above).
[GOAL]
case neg.refine'_4
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ Multiset.Nodup
    (Multiset.map AlmostMono.color
      ({ line := vertical s.focus (map some l'), color := C' s.focus,
          has_color :=
            (_ :
              ∀ (x : α),
                C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) = C' s.focus) } ::ₘ
        Multiset.map
          (fun p =>
            { line := prod p.line (map some l'), color := p.color,
              has_color :=
                (_ :
                  ∀ (x : α),
                    C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color) })
          s.lines))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]
[GOAL]
case neg.refine'_4
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ (¬∃ a,
        a ∈ s.lines ∧
          (AlmostMono.color ∘ fun p =>
                { line := prod p.line (map some l'), color := p.color,
                  has_color :=
                    (_ :
                      ∀ (x : α),
                        C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color) })
              a =
            { line := vertical s.focus (map some l'), color := C' s.focus,
                has_color :=
                  (_ :
                    ∀ (x : α),
                      C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                        C' s.focus) }.color) ∧
    Multiset.Nodup
      (Multiset.map
        (AlmostMono.color ∘ fun p =>
          { line := prod p.line (map some l'), color := p.color,
            has_color :=
              (_ :
                ∀ (x : α), C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color) })
        s.lines)
[PROOFSTEP]
exact
  ⟨fun ⟨q, hq, he⟩ => h ⟨q, hq, he⟩, s.distinct_colors⟩
    -- Finally, we really do have `r+1` lines!
[GOAL]
case neg.refine'_5
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => Option.getD (idxFun l' i) x) x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : ↑Multiset.card s.lines = r
h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus
⊢ ↑Multiset.card
      {
          lines :=
            { line := vertical s.focus (map some l'), color := C' s.focus,
                has_color :=
                  (_ :
                    ∀ (x : α),
                      C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                        C' s.focus) } ::ₘ
              Multiset.map
                (fun p =>
                  { line := prod p.line (map some l'), color := p.color,
                    has_color :=
                      (_ :
                        ∀ (x : α),
                          C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) = p.color) })
                s.lines,
          focus := Sum.elim s.focus ((fun x i => Option.getD (idxFun (map some l') i) x) none),
          is_focused :=
            (_ :
              ∀ (p : AlmostMono C),
                p ∈
                    { line := vertical s.focus (map some l'), color := C' s.focus,
                        has_color :=
                          (_ :
                            ∀ (x : α),
                              C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                                C' s.focus) } ::ₘ
                      Multiset.map
                        (fun p =>
                          { line := prod p.line (map some l'), color := p.color,
                            has_color :=
                              (_ :
                                ∀ (x : α),
                                  C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) =
                                    p.color) })
                        s.lines →
                  (fun x i => Option.getD (idxFun p.line i) x) none =
                    Sum.elim s.focus ((fun x i => Option.getD (idxFun (map some l') i) x) none)),
          distinct_colors :=
            (_ :
              Multiset.Nodup
                (Multiset.map AlmostMono.color
                  ({ line := vertical s.focus (map some l'), color := C' s.focus,
                      has_color :=
                        (_ :
                          ∀ (x : α),
                            C ((fun x i => Option.getD (idxFun (vertical s.focus (map some l')) i) x) (some x)) =
                              C' s.focus) } ::ₘ
                    Multiset.map
                      (fun p =>
                        { line := prod p.line (map some l'), color := p.color,
                          has_color :=
                            (_ :
                              ∀ (x : α),
                                C ((fun x i => Option.getD (idxFun (prod p.line (map some l')) i) x) (some x)) =
                                  p.color) })
                      s.lines))) }.lines =
    Nat.succ r
[PROOFSTEP]
rw [Multiset.card_cons, Multiset.card_map, sr]
[GOAL]
α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift κ
hc : ∀ (x : α), (ULift.up ∘ C) ((fun x i => Option.getD (idxFun l i) x) x) = c
x : α
⊢ C ((fun x i => Option.getD (idxFun l i) x) x) = c.down
[PROOFSTEP]
rw [← hc x, Function.comp_apply]
[GOAL]
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
[PROOFSTEP]
obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
[GOAL]
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
[PROOFSTEP]
specialize hι fun v => C <| ∑ i, v i
[GOAL]
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∃ l, Line.IsMono (fun v => C (∑ i : ι, ↑(v i))) l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
[PROOFSTEP]
obtain ⟨l, c, hl⟩ := hι
[GOAL]
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
[PROOFSTEP]
set s : Finset ι := Finset.univ.filter (fun i => l.idxFun i = none) with hs
[GOAL]
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
[PROOFSTEP]
refine' ⟨s.card, Finset.card_pos.mpr ⟨l.proper.choose, _⟩, ∑ i in sᶜ, ((l.idxFun i).map _).getD 0, c, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ s
[PROOFSTEP]
rw [hs, Finset.mem_filter]
[GOAL]
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ Finset.univ ∧
    Line.idxFun l (Exists.choose (_ : ∃ i, Line.idxFun l i = none)) = none
[PROOFSTEP]
exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
[GOAL]
case intro.intro.intro.intro.refine'_2
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
i : ι
⊢ { x // x ∈ S } → M
[PROOFSTEP]
exact fun m => m
[GOAL]
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∀ (s_1 : M),
    s_1 ∈ S → C (Finset.card s • s_1 + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) = c
[PROOFSTEP]
intro x xs
[GOAL]
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) = c
[PROOFSTEP]
rw [← hl ⟨x, xs⟩]
[GOAL]
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
[PROOFSTEP]
clear hl
[GOAL]
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
[PROOFSTEP]
congr
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i : ι, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
rw [← Finset.sum_add_sum_compl s]
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i) +
      ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
congr 1
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
rw [← Finset.sum_const]
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ _x in s, x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι), x_1 ∈ s → x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
rw [hs, Finset.mem_filter] at hi 
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ Line.idxFun l i = none
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι),
    x_1 ∈ sᶜ →
      Option.getD (Option.map (fun m => ↑m) (Line.idxFun l x_1)) 0 =
        ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ sᶜ
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
rw [hs, Finset.compl_filter, Finset.mem_filter] at hi 
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
[GOAL]
case intro.intro.intro.intro.refine'_3.e_a.e_a.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
y : { x // x ∈ S }
hy : some y = Line.idxFun l i
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
[PROOFSTEP]
simp_rw [← hy, Option.map_some', Option.getD]
