internlm/Lean-Github huggingface dataset:
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
⊢ { parts := image (fun i => filter (fun j => j % d = i) (range s)) (range d), supIndep := ⋯, sup_parts := ⋯,
        not_bot_mem := ⋯ }.parts =
    image (fun i => image (fun x => i + d * x) (range ((s - i - 1) / d + 1))) (range d)
Tactic:
ext x
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
⊢ x ∈
      { parts := image (fun i => filter (fun j => j % d = i) (range s)) (range d), supIndep := ⋯, sup_parts := ⋯,
          not_bot_mem := ⋯ }.parts ↔
    x ∈ image (fun i => image (fun x => i + d * x) (range ((s - i - 1) / d + 1))) (range d)
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
⊢ x ∈
      { parts := image (fun i => filter (fun j => j % d = i) (range s)) (range d), supIndep := ⋯, sup_parts := ⋯,
          not_bot_mem := ⋯ }.parts ↔
    x ∈ image (fun i => image (fun x => i + d * x) (range ((s - i - 1) / d + 1))) (range d)
Tactic:
simp only [mem_image, mem_range]
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
⊢ (∃ a < d, filter (fun j => j % d = a) (range s) = x) ↔
    ∃ a < d, image (fun x => a + d * x) (range ((s - a - 1) / d + 1)) = x
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
⊢ (∃ a < d, filter (fun j => j % d = a) (range s) = x) ↔
    ∃ a < d, image (fun x => a + d * x) (range ((s - a - 1) / d + 1)) = x
Tactic:
refine' exists_congr fun i ↦ and_congr_right fun hi ↦ _
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
i : ℕ
hi : i < d
⊢ filter (fun j => j % d = i) (range s) = x ↔ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = x
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
i : ℕ
hi : i < d
⊢ filter (fun j => j % d = i) (range s) = x ↔ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = x
Tactic:
suffices
  ((range ((s - i - 1) / d + 1)).image fun x ↦ i + d * x) = (range s).filter fun j ↦ j % d = i
  by rw [this]
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
i : ℕ
hi : i < d
⊢ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = filter (fun j => j % d = i) (range s)
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
i : ℕ
hi : i < d
⊢ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = filter (fun j => j % d = i) (range s)
Tactic:
clear x
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
⊢ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = filter (fun j => j % d = i) (range s)
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
⊢ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = filter (fun j => j % d = i) (range s)
Tactic:
ext j
Proof state after:
case a.a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ j ∈ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) ↔ j ∈ filter (fun j => j % d = i) (range s)
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ j ∈ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) ↔ j ∈ filter (fun j => j % d = i) (range s)
Tactic:
simp only [mem_image, mem_filter, mem_range, Nat.lt_add_one_iff]
Proof state after:
case a.a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ (∃ a ≤ (s - i - 1) / d, i + d * a = j) ↔ j < s ∧ j % d = i
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ (∃ a ≤ (s - i - 1) / d, i + d * a = j) ↔ j < s ∧ j % d = i
Tactic:
constructor
Proof state after:
case a.a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ (∃ a ≤ (s - i - 1) / d, i + d * a = j) → j < s ∧ j % d = i

case a.a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ j < s ∧ j % d = i → ∃ a ≤ (s - i - 1) / d, i + d * a = j
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
x : Finset ℕ
i : ℕ
hi : i < d
this : image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = filter (fun j => j % d = i) (range s)
⊢ filter (fun j => j % d = i) (range s) = x ↔ image (fun x => i + d * x) (range ((s - i - 1) / d + 1)) = x
Tactic:
rw [this]
Proof state after:
no goals
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ (∃ a ≤ (s - i - 1) / d, i + d * a = j) → j < s ∧ j % d = i
Tactic:
rintro ⟨j, hj, rfl⟩
Proof state after:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j ≤ (s - i - 1) / d
⊢ i + d * j < s ∧ (i + d * j) % d = i
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j ≤ (s - i - 1) / d
⊢ i + d * j < s ∧ (i + d * j) % d = i
Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hi, eq_self_iff_true, and_true_iff, ←
  Nat.lt_sub_iff_add_lt', mul_comm]
Proof state after:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j ≤ (s - i - 1) / d
⊢ j * d < s - i
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j ≤ (s - i - 1) / d
⊢ j * d < s - i
Tactic:
rwa [Nat.le_div_iff_mul_le hd.bot_lt, Nat.le_sub_iff_add_le, Nat.succ_le_iff] at hj
Proof state after:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 1 ≤ s - i
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 1 ≤ s - i
Tactic:
rw [Nat.succ_le_iff]
Proof state after:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 0 < s - i
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 0 < s - i
Tactic:
exact Nat.sub_pos_of_lt (hi.trans_le h)
Proof state after:
no goals
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
⊢ j < s ∧ j % d = i → ∃ a ≤ (s - i - 1) / d, i + d * a = j
Tactic:
rintro ⟨hj, rfl⟩
Proof state after:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ ∃ a ≤ (s - j % d - 1) / d, j % d + d * a = j
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ ∃ a ≤ (s - j % d - 1) / d, j % d + d * a = j
Tactic:
refine' ⟨j / d, _, Nat.mod_add_div _ _⟩
Proof state after:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j / d ≤ (s - j % d - 1) / d
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j / d ≤ (s - j % d - 1) / d
Tactic:
rwa [Nat.le_div_iff_mul_le' hd.bot_lt, Nat.le_sub_iff_add_le, Nat.le_sub_iff_add_le',
  ← add_assoc, mul_comm, Nat.mod_add_div, Nat.add_one_le_iff]
Proof state after:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j % d ≤ s

case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ 1 ≤ s - j % d
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ 1 ≤ s - j % d
Tactic:
rw [Nat.succ_le_iff]
Proof state after:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ 0 < s - j % d
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ 0 < s - j % d
Tactic:
exact Nat.sub_pos_of_lt (hi.trans_le h)
Proof state after:
no goals
Theorem: Finpartition.modPartitions_parts_eq
Proof state before:
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j % d ≤ s
Tactic:
exact hi.le.trans h
Proof state after:
no goals
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ IsExtreme 𝕜 s t ↔ t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
Tactic:
refine' ⟨fun h => ⟨h.1, fun x y hx hy z hz =>
  ⟨hAconv.openSegment_subset hx hy.1 hz, fun hzB => hy.2 (h.2 hx hy.1 hzB hz).2⟩⟩,
    fun h => ⟨h.1, fun x hx y hy z hzB hz => ⟨_, _⟩⟩⟩
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ x ∈ t

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ y ∈ t
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ x ∈ t
Tactic:
by_contra hxB
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hxB : x ∉ t
⊢ False
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hxB : x ∉ t
⊢ False
Tactic:
rw [openSegment_symm] at hz
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 y x
hxB : x ∉ t
⊢ False
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 y x
hxB : x ∉ t
⊢ False
Tactic:
exact (h.2 hy ⟨hx, hxB⟩ hz).2 hzB
Proof state after:
no goals
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ y ∈ t
Tactic:
by_contra hyB
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hyB : y ∉ t
⊢ False
Theorem: Convex.isExtreme_iff_openSegment_subset_diff
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hyB : y ∉ t
⊢ False
Tactic:
exact (h.2 hx ⟨hy, hyB⟩ hz).2 hzB
Proof state after:
no goals
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s ↔ ConvexIndependent 𝕜 fun p => ↑p
Tactic:
refine' ⟨fun h => _, fun hs => _⟩
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
h : extremePoints 𝕜 ((convexHull 𝕜) s) = s
⊢ ConvexIndependent 𝕜 fun p => ↑p

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ConvexIndependent 𝕜 fun p => ↑p
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ConvexIndependent 𝕜 fun p => ↑p
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Tactic:
rw [convexIndependent_set_iff_not_mem_convexHull_diff] at hs
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Tactic:
refine' extremePoints_convexHull_subset.antisymm fun x hxs => ⟨subset_convexHull 𝕜 _ hxs, _⟩
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Tactic:
by_contra! h
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
h : ∃ x₁ ∈ (convexHull 𝕜) s, ∃ x₂ ∈ (convexHull 𝕜) s, x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
h : ∃ x₁ ∈ (convexHull 𝕜) s, ∃ x₂ ∈ (convexHull 𝕜) s, x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Tactic:
obtain ⟨x₁, hx₁, x₂, hx₂, hx⟩ := h
Proof state after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Tactic:
suffices h : x₁ ∈ convexHull 𝕜 (s \ {x}) ∧ x₂ ∈ convexHull 𝕜 (s \ {x}) by
  exact hs _ hxs (convex_iff_openSegment_subset.1 (convex_convexHull 𝕜 _) h.1 h.2 hx.1)
Proof state after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Tactic:
have hx₁₂ : segment 𝕜 x₁ x₂ ⊆ convexHull 𝕜 s := (convex_convexHull 𝕜 _).segment_subset hx₁ hx₂
Proof state after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
hx₁₂ : segment 𝕜 x₁ x₂ ⊆ (convexHull 𝕜) s
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
hx₁₂ : segment 𝕜 x₁ x₂ ⊆ (convexHull 𝕜) s
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Tactic:
sorry
Proof state after:
no goals
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
h : extremePoints 𝕜 ((convexHull 𝕜) s) = s
⊢ ConvexIndependent 𝕜 fun p => ↑p
Tactic:
exact (convex_convexHull 𝕜 _).convexIndependent_extremePoints
Proof state after:
no goals
Theorem: extremePoints_convexHull_eq_iff_convexIndependent
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
h : x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
⊢ False
Tactic:
exact hs _ hxs (convex_iff_openSegment_subset.1 (convex_convexHull 𝕜 _) h.1 h.2 hx.1)
Proof state after:
no goals
Theorem: inter_frontier_self_inter_convexHull_extreme
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
⊢ IsExtreme 𝕜 (closure s) (closure s ∩ frontier ((convexHull 𝕜) s))
Tactic:
refine' ⟨inter_subset_left, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ frontier ((convexHull 𝕜) s)

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)