awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Extreme
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

Tactic:
congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)

Premises used: congrArg, Prod.fst, And.right, Set.mk_mem_prod
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
h₁ : (x, y) ∈ openSegment 𝕜 (x₁, (x, y).2) (x₂, (x, y).2)
⊢ x₁ = (x, y).1

Tactic:
refine congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)

Premises used: congrArg, Prod.fst, And.right, Set.mk_mem_prod
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
h₁ : Membership.mem (γ := Set (E × F)) ((fun (x_1 : E) ↦ (x_1, (x, y).2)) '' openSegment 𝕜 x₁ x₂) (x, y)
⊢ (x, y) ∈ openSegment 𝕜 (x₁, (x, y).2) (x₂, (x, y).2)

Tactic:
rw [← Prod.image_mk_openSegment_left]

Premises used: Prod.image_mk_openSegment_left
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
⊢ Membership.mem (γ := Set (E × F)) ((fun (x_1 : E) ↦ (x_1, (x, y).2)) '' openSegment 𝕜 x₁ x₂) (x, y)

Tactic:
mem_image_of_mem _ hx_fst

Premises used: Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
⊢ Membership.mem (γ := Set (E × F)) ((fun (x_1 : E) ↦ (x_1, (x, y).2)) '' openSegment 𝕜 x₁ x₂) (x, y)

Tactic:
exact mem_image_of_mem _ hx_fst

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Extreme
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

Tactic:
congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)

Premises used: congrArg, And.left, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
h₁ : (x, y) ∈ openSegment 𝕜 ((x, y).1, x₁) ((x, y).1, x₂)
⊢ x₁ = (x, y).2

Tactic:
refine congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)

Premises used: congrArg, And.left, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
h₁ : Membership.mem (γ := Set (E × F)) ((fun (y_1 : F) ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂) (x, y)
⊢ (x, y) ∈ openSegment 𝕜 ((x, y).1, x₁) ((x, y).1, x₂)

Tactic:
rw [← Prod.image_mk_openSegment_right]

Premises used: Prod.image_mk_openSegment_right
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
⊢ Membership.mem (γ := Set (E × F)) ((fun (y_1 : F) ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂) (x, y)

Tactic:
mem_image_of_mem _ hx_snd

Premises used: Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Extreme
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₂
⊢ Membership.mem (γ := Set (E × F)) ((fun (y_1 : F) ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂) (x, y)

Tactic:
exact mem_image_of_mem _ hx_snd

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Extreme
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)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Extreme
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 :
  ((∀ (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
⊢ x ∈ extremePoints 𝕜 (pi (α := M) univ s) ↔
    Membership.mem (γ := Set ((i : ι) → M i)) (pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s i)) x

Tactic:
simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]

Premises used: mem_extremePoints_iff_left, Set.mem_univ_pi, forall_and
-- Module: Mathlib.Analysis.Convex.Extreme
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

Tactic:
and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.Analysis.Convex.Extreme
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
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
⊢ ((∀ (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:
refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.Analysis.Convex.Extreme
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₂)
rw : ∀ (i_1 : ι), update (β := M) x i x₁ i_1 ∈ s i_1
⊢ x₁ = x i

Tactic:
rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]

Premises used: Function.update, Function.update_self
-- Module: Mathlib.Analysis.Convex.Extreme
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
h₂ : ∀ (hji : j ≠ i), update (β := M) x i x₂ j ∈ s j
⊢ update (β := M) x i x₂ j ∈ s j

Tactic:
obtain rfl | hji := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
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
j : ι
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:
simp [*]
-- Module: Mathlib.Analysis.Convex.Extreme
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 : ι
hji : j ≠ i
⊢ update (β := M) x i x₂ j ∈ s j

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Extreme
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₁ : x ∈ update (β := M) x i '' openSegment 𝕜 x₁ x₂
⊢ x ∈ openSegment 𝕜 (update (β := M) x i x₁) (update (β := M) x i x₂)

Tactic:
rw [← Pi.image_update_openSegment]

Premises used: Pi.image_update_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
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 ∈ update (β := M) x i '' openSegment 𝕜 x₁ x₂

Tactic:
⟨_, hi, update_eq_self _ _⟩

Premises used: Function.update_eq_self, Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.Convex.Extreme
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 ∈ update (β := M) x i '' openSegment 𝕜 x₁ x₂

Tactic:
exact ⟨_, hi, update_eq_self _ _⟩
-- Module: Mathlib.Analysis.Convex.Extreme
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
inr : ∀ (hji : j ≠ i), update (β := M) x i x₁ j ∈ s j
⊢ update (β := M) x i x₁ j ∈ s j

Tactic:
obtain rfl | hji := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
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
j : ι
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:
simp [*]
-- Module: Mathlib.Analysis.Convex.Extreme
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 : ι
hji : j ≠ i
⊢ update (β := M) x i x₁ j ∈ s j

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Extreme
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
h₁ : ∀ (i : ι), x₁ i = (a • x₁ + b • x₂) i
⊢ x₁ = a • x₁ + b • x₂

Tactic:
ext i
-- Module: Mathlib.Analysis.Convex.Extreme
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
i : ι
⊢ x₁ i = (a • x₁ + b • x₂) i

Tactic:
h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
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
i : ι
⊢ x₁ i = (a • x₁ + b • x₂) i

Tactic:
exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
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
h₃ 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
⊢ extremePoints 𝕜 (pi (α := M) univ s) = pi (α := M) univ fun (i : ι) ↦ extremePoints 𝕜 (s 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⟩

Premises used: mem_extremePoints_iff_left, Pi.image_update_openSegment, and_congr_right, Iff.intro, Set.mem_univ_pi, rfl, forall_and
-- Module: Mathlib.Analysis.Convex.Extreme
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
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
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s))

Tactic:
ext b
-- Module: Mathlib.Analysis.Convex.Extreme
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
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)
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) b ↔
    Membership.mem (γ := Set F) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s)) b

Tactic:
obtain ⟨a, rfl⟩ := EquivLike.surjective f b

Premises used: EquivLike.surjective, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
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
a : E
⊢ ∀ (x y : E),
    Eq.{u_3 + 1} (α := Set F) ((⇑f : (a : E) → F) '' openSegment 𝕜 x y : Set F)
      (openSegment 𝕜 ((f : (a : E) → F) x) ((f : (a : E) → F) y) : Set F)

Tactic:
have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
    image_openSegment _ (LinearMapClass.linearMap f).toAffineMap
-- Module: Mathlib.Analysis.Convex.Extreme
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
a : E
this :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := Set F) ((⇑f : (a : E) → F) '' openSegment 𝕜 x y : Set F)
      (openSegment 𝕜 ((f : (a : E) → F) x) ((f : (a : E) → F) y) : Set F)
⊢ 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:
simp only [mem_extremePoints, (EquivLike.surjective f).forall,
    (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this]

Premises used: Function.Surjective.forall, Function.Injective.eq_iff, mem_extremePoints, EquivLike.surjective, EquivLike.injective, Function.Injective.mem_set_image