[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]


[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε'
[PROOFSTEP]
refine' (hε hs' ht' (le_trans _ hs) (le_trans _ ht)).trans_le h
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ ↑(card s) * ε ≤ ↑(card s) * ε'
[PROOFSTEP]
gcongr
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ ↑(card t) * ε ≤ ↑(card t) * ε'
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ |↑(edgeDensity G t' s') - ↑(edgeDensity G t s)| < ε
[PROOFSTEP]
rw [edgeDensity_comm _ t', edgeDensity_comm _ t]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε
[PROOFSTEP]
exact h hs' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
⊢ IsUniform G ε {a} {b}
[PROOFSTEP]
intro s' hs' t' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(card {a}) * ε ≤ ↑(card s')
ht : ↑(card {b}) * ε ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
rw [card_singleton, Nat.cast_one, one_mul] at hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(card s')
ht : ε ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ |↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
replace hs : ε ≤ 0 := by simpa using hs
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
simpa using hs
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ |↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
exact (hε.not_le hs).elim
[GOAL]
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
⊢ |↑(edgeDensity G {a} t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
[GOAL]
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ |↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
replace ht : ε ≤ 0 := by simpa using ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
simpa using ht
[GOAL]
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ |↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
exact (hε.not_le ht).elim
[GOAL]
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(card {b})
⊢ |↑(edgeDensity G {a} {b}) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
rwa [sub_self, abs_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card s) * 0 ≤ ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card t) * 0 ≤ ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ IsUniform G 1 s t
[PROOFSTEP]
intro s' hs' t' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * 1 ≤ ↑(card s')
ht : ↑(card t) * 1 ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < 1
[PROOFSTEP]
rw [mul_one] at hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < 1
[PROOFSTEP]
rw [eq_of_subset_of_card_le hs' (Nat.cast_le.1 hs), eq_of_subset_of_card_le ht' (Nat.cast_le.1 ht), sub_self, abs_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ ¬IsUniform G ε s t ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧ ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|
[PROOFSTEP]
unfold IsUniform
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t →
              ↑(card s) * ε ≤ ↑(card s') →
                ↑(card t) * ε ≤ ↑(card t') → |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε) ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧ ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|
[PROOFSTEP]
simp only [not_forall, not_lt, exists_prop, exists_and_left, Rat.cast_abs, Rat.cast_sub]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (nonuniformWitnesses G ε s t).fst ⊆ s
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (Exists.choose
          (_ :
            ∃ s',
              s' ⊆ s ∧
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤ ↑(card s') ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
        Exists.choose
          (_ :
            ∃ t',
              t' ⊆ t ∧
                ↑(card s) * ε ≤
                    ↑(card
                        (Exists.choose
                          (_ :
                            ∃ s',
                              s' ⊆ s ∧
                                ∃ t',
                                  t' ⊆ t ∧
                                    ↑(card s) * ε ≤ ↑(card s') ∧
                                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑|edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                              t' -
                            edgeDensity G s t|)).fst ⊆
    s
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.1
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).fst)
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤
    ↑(card
        (Exists.choose
              (_ :
                ∃ s',
                  s' ⊆ s ∧
                    ∃ t',
                      t' ⊆ t ∧
                        ↑(card s) * ε ≤ ↑(card s') ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
            Exists.choose
              (_ :
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤
                        ↑(card
                            (Exists.choose
                              (_ :
                                ∃ s',
                                  s' ⊆ s ∧
                                    ∃ t',
                                      t' ⊆ t ∧
                                        ↑(card s) * ε ≤ ↑(card s') ∧
                                          ↑(card t) * ε ≤ ↑(card t') ∧
                                            ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧
                        ε ≤
                          ↑|edgeDensity G
                                  (Exists.choose
                                    (_ :
                                      ∃ s',
                                        s' ⊆ s ∧
                                          ∃ t',
                                            t' ⊆ t ∧
                                              ↑(card s) * ε ≤ ↑(card s') ∧
                                                ↑(card t) * ε ≤ ↑(card t') ∧
                                                  ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                  t' -
                                edgeDensity G s t|)).fst)
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (nonuniformWitnesses G ε s t).snd ⊆ t
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (Exists.choose
          (_ :
            ∃ s',
              s' ⊆ s ∧
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤ ↑(card s') ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
        Exists.choose
          (_ :
            ∃ t',
              t' ⊆ t ∧
                ↑(card s) * ε ≤
                    ↑(card
                        (Exists.choose
                          (_ :
                            ∃ s',
                              s' ⊆ s ∧
                                ∃ t',
                                  t' ⊆ t ∧
                                    ↑(card s) * ε ≤ ↑(card s') ∧
                                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑|edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                              t' -
                            edgeDensity G s t|)).snd ⊆
    t
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.1
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card t) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).snd)
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card t) * ε ≤
    ↑(card
        (Exists.choose
              (_ :
                ∃ s',
                  s' ⊆ s ∧
                    ∃ t',
                      t' ⊆ t ∧
                        ↑(card s) * ε ≤ ↑(card s') ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
            Exists.choose
              (_ :
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤
                        ↑(card
                            (Exists.choose
                              (_ :
                                ∃ s',
                                  s' ⊆ s ∧
                                    ∃ t',
                                      t' ⊆ t ∧
                                        ↑(card s) * ε ≤ ↑(card s') ∧
                                          ↑(card t) * ε ≤ ↑(card t') ∧
                                            ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧
                        ε ≤
                          ↑|edgeDensity G
                                  (Exists.choose
                                    (_ :
                                      ∃ s',
                                        s' ⊆ s ∧
                                          ∃ t',
                                            t' ⊆ t ∧
                                              ↑(card s) * ε ≤ ↑(card s') ∧
                                                ↑(card t) * ε ≤ ↑(card t') ∧
                                                  ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                  t' -
                                edgeDensity G s t|)).snd)
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t|
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ε ≤
    ↑|edgeDensity G
            (Exists.choose
                  (_ :
                    ∃ s',
                      s' ⊆ s ∧
                        ∃ t',
                          t' ⊆ t ∧
                            ↑(card s) * ε ≤ ↑(card s') ∧
                              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
                Exists.choose
                  (_ :
                    ∃ t',
                      t' ⊆ t ∧
                        ↑(card s) * ε ≤
                            ↑(card
                                (Exists.choose
                                  (_ :
                                    ∃ s',
                                      s' ⊆ s ∧
                                        ∃ t',
                                          t' ⊆ t ∧
                                            ↑(card s) * ε ≤ ↑(card s') ∧
                                              ↑(card t) * ε ≤ ↑(card t') ∧
                                                ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧
                            ε ≤
                              ↑|edgeDensity G
                                      (Exists.choose
                                        (_ :
                                          ∃ s',
                                            s' ⊆ s ∧
                                              ∃ t',
                                                t' ⊆ t ∧
                                                  ↑(card s) * ε ≤ ↑(card s') ∧
                                                    ↑(card t) * ε ≤ ↑(card t') ∧
                                                      ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                      t' -
                                    edgeDensity G s t|)).fst
            (Exists.choose
                  (_ :
                    ∃ s',
                      s' ⊆ s ∧
                        ∃ t',
                          t' ⊆ t ∧
                            ↑(card s) * ε ≤ ↑(card s') ∧
                              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|),
                Exists.choose
                  (_ :
                    ∃ t',
                      t' ⊆ t ∧
                        ↑(card s) * ε ≤
                            ↑(card
                                (Exists.choose
                                  (_ :
                                    ∃ s',
                                      s' ⊆ s ∧
                                        ∃ t',
                                          t' ⊆ t ∧
                                            ↑(card s) * ε ≤ ↑(card s') ∧
                                              ↑(card t) * ε ≤ ↑(card t') ∧
                                                ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧
                            ε ≤
                              ↑|edgeDensity G
                                      (Exists.choose
                                        (_ :
                                          ∃ s',
                                            s' ⊆ s ∧
                                              ∃ t',
                                                t' ⊆ t ∧
                                                  ↑(card s) * ε ≤ ↑(card s') ∧
                                                    ↑(card t) * ε ≤ ↑(card t') ∧
                                                      ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                      t' -
                                    edgeDensity G s t|)).snd -
          edgeDensity G s t|
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.2
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ nonuniformWitness G ε s t ⊆ s
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd) ⊆ s
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : WellOrderingRel s t
⊢ (nonuniformWitnesses G ε s t).fst ⊆ s
[PROOFSTEP]
exact G.left_nonuniformWitnesses_subset h
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : ¬WellOrderingRel s t
⊢ (nonuniformWitnesses G ε t s).snd ⊆ s
[PROOFSTEP]
exact G.right_nonuniformWitnesses_subset fun i => h i.symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitness G ε s t))
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤
    ↑(card (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).fst)
[PROOFSTEP]
exact G.left_nonuniformWitnesses_card h
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε t s).snd)
[PROOFSTEP]
exact G.right_nonuniformWitnesses_card fun i => h i.symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitness G ε s t) (nonuniformWitness G ε t s) - edgeDensity G s t|
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
⊢ ε ≤
    ↑|edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t|
[PROOFSTEP]
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t|
[PROOFSTEP]
rw [if_pos lt, if_neg (asymm lt)]
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t|
[PROOFSTEP]
exact G.nonuniformWitnesses_spec h₂
[GOAL]
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
a b : α
h₁ : s ≠ s
h₂ : ¬IsUniform G ε s s
⊢ ε ≤
    ↑|edgeDensity G
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd)
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd) -
          edgeDensity G s s|
[PROOFSTEP]
cases h₁ rfl
[GOAL]
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t|
[PROOFSTEP]
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
[GOAL]
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε t s).fst (nonuniformWitnesses G ε t s).snd - edgeDensity G t s|
[PROOFSTEP]
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ : 𝕜
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈ nonUniforms P G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ nonUniforms ⊥ G ε = ∅
[PROOFSTEP]
rw [eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), ¬x ∈ nonUniforms ⊥ G ε
[PROOFSTEP]
rintro ⟨u, v⟩
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ¬(u, v) ∈ nonUniforms ⊥ G ε
[PROOFSTEP]
simp only [Finpartition.mk_mem_nonUniforms_iff, Finpartition.parts_bot, mem_map, not_and, Classical.not_not, exists_imp]
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = u →
      ∀ (x : α),
        x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = v →
          u ≠ v → SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
dsimp
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α), x ∈ A ∧ {x} = u → ∀ (x : α), x ∈ A ∧ {x} = v → ¬u = v → SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rintro x ⟨_, xu⟩ y ⟨_, yv⟩ _
[GOAL]
case mk.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rw [← xu, ← yv]
[GOAL]
case mk.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε {x} {y}
[PROOFSTEP]
exact G.isUniform_singleton hε
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ IsUniform ⊥ G ε
[PROOFSTEP]
rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty, Nat.cast_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(card A * (card A - 1)) * ε
[PROOFSTEP]
exact mul_nonneg (Nat.cast_nonneg _) hε.le
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ IsUniform P G 1
[PROOFSTEP]
rw [IsUniform, mul_one, Nat.cast_le]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ card (nonUniforms P G 1) ≤ card P.parts * (card P.parts - 1)
[PROOFSTEP]
refine' (card_filter_le _ (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans _
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ card (offDiag P.parts) ≤ card P.parts * (card P.parts - 1)
[PROOFSTEP]
rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ ε ε' : 𝕜
hP : IsUniform P G ε
h : ε ≤ ε'
⊢ ↑(card P.parts * (card P.parts - 1)) * ε ≤ ↑(card P.parts * (card P.parts - 1)) * ε'
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.parts = ∅
⊢ IsUniform P G ε
[PROOFSTEP]
simp [IsUniform, hP, nonUniforms]


[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : Fintype α
inst✝ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
hε : FarFromTriangleFree G ε
h : δ ≤ ε
⊢ δ * ↑(Fintype.card α ^ 2) ≤ ε * ↑(Fintype.card α ^ 2)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
⊢ ε ≤ 0
[PROOFSTEP]
have := h₀ (empty_subset _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
this : (fun H => CliqueFree H 3) (deleteEdges G ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(Finset.card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty_eq] at this
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
this : (fun H => CliqueFree H 3) G → ε * ↑(Fintype.card α ^ 2) ≤ 0
⊢ ε ≤ 0
[PROOFSTEP]
exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)