awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
h :
  ∀ (hx : (x, y) ∈ s ×ˢ t)
    (h :
      (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
        ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2)
    ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
⊢ (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
have h₁ : ∀ (hx : (x, y) ∈ s ×ˢ t)
  (h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)) ⦃x₁ : E⦄,
  x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1
Tactic: refine (and_congr_right fun hx ↦ ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩).trans and_and_and_comm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
h :
  ∀ (hx : (x, y) ∈ s ×ˢ t)
    (h :
      (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
        ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2)
    ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
h₁ :
  ∀ (hx : (x, y) ∈ s ×ˢ t)
    (h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y))
    ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1
⊢ (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
have h₂ : ∀ (hx : (x, y) ∈ s ×ˢ t)
  (h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)) ⦃x₁ : F⦄,
  x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
Tactic: refine (and_congr_right fun hx ↦ ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩).trans and_and_and_comm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
⊢ x₁ = (x, y)
have h₁ : x₁.1 = (x, y).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
h₁ : x₁.1 = (x, y).1
⊢ x₁ = (x, y)
have h₂ : x₁.2 = (x, y).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : (x, y).1 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = (x, y).1
have h₁ : (x, y) ∈ openSegment 𝕜 (x₁, (x, y).2) (x₂, (x, y).2)
Tactic: refine congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : (x, y).1 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ openSegment 𝕜 (x₁, (x, y).2) (x₂, (x, y).2)
have h₁ : Membership.mem (γ := Set (E × F)) ((fun (x_1 : E) ↦ (x_1, (x, y).2)) '' openSegment 𝕜 x₁ x₂) (x, y)
Tactic: rw [← Prod.image_mk_openSegment_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = (x, y).2
have h₁ : (x, y) ∈ openSegment 𝕜 ((x, y).1, x₁) ((x, y).1, x₂)
Tactic: refine congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ openSegment 𝕜 ((x, y).1, x₁) ((x, y).1, x₂)
have h₁ : Membership.mem (γ := Set (E × F)) ((fun (y_1 : F) ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂) (x, y)
Tactic: rw [← Prod.image_mk_openSegment_right]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)
have h : ∀ (x : (i : ι) → M i),
  x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
    Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
⊢ x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
    Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
have h : ((∀ (i : ι), x i ∈ s i) ∧
    ∀ (x₁ : (i : ι) → M i),
      (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
  (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
Tactic: simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
⊢ ((∀ (i : ι), x i ∈ s i) ∧
      ∀ (x₁ : (i : ι) → M i),
        (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
    (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
have h : ∀ (hx : ∀ (i : ι), x i ∈ s i)
  (h :
    ∀ (x₁ : (i : ι) → M i),
      (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x)
  (i : ι), ∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i
Tactic: refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
h :
  ∀ (hx : ∀ (i : ι), x i ∈ s i)
    (h :
      ∀ (x₁ : (i : ι) → M i),
        (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x)
    (i : ι), ∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i
⊢ ((∀ (i : ι), x i ∈ s i) ∧
      ∀ (x₁ : (i : ι) → M i),
        (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
    (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
have h₁ : ∀ (hx : ∀ (i : ι), x i ∈ s i) (h : ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1)
  (x₁ : (i : ι) → M i),
  (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
Tactic: refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x i
have h₁ : ∀ (i_1 : ι), update (β := M) x i x₂ i_1 ∈ s i_1
Tactic: rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
h₁ : ∀ (i_1 : ι), update (β := M) x i x₂ i_1 ∈ s i_1
⊢ x₁ = x i
have h₂ : x ∈ openSegment 𝕜 (update (β := M) x i x₁) (update (β := M) x i x₂)
Tactic: rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
h₁ : ∀ (i_1 : ι), update (β := M) x i x₂ i_1 ∈ s i_1
h₂ : x ∈ openSegment 𝕜 (update (β := M) x i x₁) (update (β := M) x i x₂)
⊢ x₁ = x i
have rw : ∀ (i_1 : ι), update (β := M) x i x₁ i_1 ∈ s i_1
Tactic: rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
j : ι
⊢ update (β := M) x i x₂ j ∈ s j
have h₁ : ∀ (x₁ : M j) (hx₁ : x₁ ∈ s j) (x₂ : M j) (hx₂ : x₂ ∈ s j) (hi : x j ∈ openSegment 𝕜 x₁ x₂),
  update (β := M) x j x₂ j ∈ s j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i, x₁, hx₁, x₂, hx₂, hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
j : ι
h₁ :
  ∀ (x₁ : M j) (hx₁ : x₁ ∈ s j) (x₂ : M j) (hx₂ : x₂ ∈ s j) (hi : x j ∈ openSegment 𝕜 x₁ x₂),
    update (β := M) x j x₂ j ∈ s j
⊢ update (β := M) x i x₂ j ∈ s j
have h₂ : ∀ (hji : j ≠ i), update (β := M) x i x₂ j ∈ s j
Tactic: obtain rfl | hji := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ openSegment 𝕜 (update (β := M) x i x₁) (update (β := M) x i x₂)
have h₁ : x ∈ update (β := M) x i '' openSegment 𝕜 x₁ x₂
Tactic: rw [← Pi.image_update_openSegment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
j : ι
⊢ update (β := M) x i x₁ j ∈ s j
have inl : ∀ (x₁ : M j) (hx₁ : x₁ ∈ s j) (x₂ : M j) (hx₂ : x₂ ∈ s j) (hi : x j ∈ openSegment 𝕜 x₁ x₂),
  update (β := M) x j x₁ j ∈ s j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i, x₁, hx₁, x₂, hx₂, hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
j : ι
inl :
  ∀ (x₁ : M j) (hx₁ : x₁ ∈ s j) (x₂ : M j) (hx₂ : x₂ ∈ s j) (hi : x j ∈ openSegment 𝕜 x₁ x₂),
    update (β := M) x j x₁ j ∈ s j
⊢ update (β := M) x i x₁ j ∈ s j
have inr : ∀ (hji : j ≠ i), update (β := M) x i x₁ j ∈ s j
Tactic: obtain rfl | hji := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
x₁ : (i : ι) → M i
hx₁ : ∀ (i : ι), x₁ i ∈ s i
x₂ : (i : ι) → M i
hx₂ : ∀ (i : ι), x₂ i ∈ s i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : ∀ (i : ι), (a • x₁ + b • x₂) i ∈ s i
h : ∀ (x : ι), ∀ x₁_1 ∈ s x, ∀ x₂_1 ∈ s x, (a • x₁ + b • x₂) x ∈ openSegment 𝕜 x₁_1 x₂_1 → x₁_1 = (a • x₁ + b • x₂) x
⊢ x₁ = a • x₁ + b • x₂
have h₁ : ∀ (i : ι), x₁ i = (a • x₁ + b • x₂) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)
have h : ∀ (x : (i : ι) → M i),
  x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
    Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
Tactic: classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
h :
  ∀ (x : (i : ι) → M i),
    x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
      Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)
have h₁ : ∀ (x : (i : ι) → M i),
  ((∀ (i : ι), x i ∈ s i) ∧
      ∀ (x₁ : (i : ι) → M i),
        (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
    (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
Tactic: classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
h :
  ∀ (x : (i : ι) → M i),
    x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
      Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
h₁ :
  ∀ (x : (i : ι) → M i),
    ((∀ (i : ι), x i ∈ s i) ∧
        ∀ (x₁ : (i : ι) → M i),
          (∀ (i : ι), x₁ i ∈ s i) →
            ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
      (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)
have h₂ : ∀ (x : (i : ι) → M i) (hx : ∀ (i : ι), x i ∈ s i)
  (h :
    ∀ (x₁ : (i : ι) → M i),
      (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x)
  (i : ι), ∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i
Tactic: classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u_5} 𝕜 (M i)
s : (i : ι) → Set (M i)
h :
  ∀ (x : (i : ι) → M i),
    x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
      Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x
h₁ :
  ∀ (x : (i : ι) → M i),
    ((∀ (i : ι), x i ∈ s i) ∧
        ∀ (x₁ : (i : ι) → M i),
          (∀ (i : ι), x₁ i ∈ s i) →
            ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x) ↔
      (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
h₂ :
  ∀ (x : (i : ι) → M i) (hx : ∀ (i : ι), x i ∈ s i)
    (h :
      ∀ (x₁ : (i : ι) → M i),
        (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x)
    (i : ι), ∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)
have h₃ : ∀ (x : (i : ι) → M i) (hx : ∀ (i : ι), x i ∈ s i)
  (h : ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1) (x₁ : (i : ι) → M i),
  (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
Tactic: classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : EquivLike L E F
inst_8 : LinearEquivClass L 𝕜 E F
f : L
s : Set E
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s))
have h : ∀ (b : F),
  Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) b ↔
    Membership.mem (γ := Set F) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s)) b
Tactic: ext b
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : EquivLike L E F
inst_8 : LinearEquivClass L 𝕜 E F
f : L
s : Set E
b : F
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) b ↔
    Membership.mem (γ := Set F) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s)) b
have h : ∀ (a : E),
  Membership.mem.{u_3, u_3} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) ((f : (a : E) → F) a : F) ↔
    Membership.mem.{u_3, u_3} (α := F) (γ := Set F) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s))
      ((f : (a : E) → F) a : F)
Tactic: obtain ⟨a, rfl⟩ := EquivLike.surjective f b
Cleared hypotheses: b