-- Mathlib/Analysis/Convex/Extreme.lean
theorem extremePoints_pi (s : ∀ i, Set (π i)) :
    (univ.pi s).extremePoints 𝕜 = univ.pi fun i ↦ (s i).extremePoints 𝕜

Proof state:
case h.refine_1.refine_2.inl
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
j : ι
x₁ : π j
hx₁ : x₁ ∈ s j
x₂ : π j
hx₂ : x₂ ∈ s j
hi : x j ∈ openSegment 𝕜 x₁ x₂
⊢ update x j x₂ j ∈ s j

Tactic:
rwa [update_self]

Result:
no goals

Proof state:
case h.refine_1.refine_3
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
x₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ update x i '' openSegment 𝕜 x₁ x₂

Tactic:
exact ⟨_, hi, update_eq_self _ _⟩

Result:
no goals

Proof state:
case h.refine_1.refine_3
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
x₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ openSegment 𝕜 (update x i x₁) (update x i x₂)

Tactic:
rw [← Pi.image_update_openSegment]

Result:
case h.refine_1.refine_3
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
x₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ update x i '' openSegment 𝕜 x₁ x₂

Proof state:
case h
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ ((∀ (i : ι), x i ∈ s i) ∧
      ∀ (x₁ : (i : ι) → π i),
        (∀ (i : ι), x₁ i ∈ s i) →
          ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → 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₂ = x x_1

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

Result:
case h.refine_1
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
⊢ ∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i ∧ x₂ = x i

case h.refine_2
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π 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₂ = x x_1
⊢ ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Proof state:
case h.refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π 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₂ = x x_1
x₁ : (i : ι) → π i
hx₁ : ∀ (i : ι), x₁ i ∈ s i
x₂ : (i : ι) → π i
hx₂ : ∀ (i : ι), x₂ i ∈ s i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = x
⊢ x₁ = x ∧ x₂ = x

Tactic:
simp_rw [funext_iff, ← forall_and]

Result:
case h.refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π 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₂ = x x_1
x₁ : (i : ι) → π i
hx₁ : ∀ (i : ι), x₁ i ∈ s i
x₂ : (i : ι) → π i
hx₂ : ∀ (i : ι), x₂ i ∈ s i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = x
⊢ ∀ (x_1 : ι), x₁ x_1 = x x_1 ∧ x₂ x_1 = x x_1

Proof state:
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
x₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
h₁ : update x i x₁ = x
⊢ x₁ = x i

Tactic:
rw [← h₁, update_self]

Result:
no goals

Proof state:
case h.refine_1.refine_2.inr
𝕜 : Type u_1
ι : Type u_4
π : ι → Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommGroup (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : (i : ι) → Set (π i)
x : (i : ι) → π i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → π i),
    (∀ (i : ι), x₁ i ∈ s i) →
      ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
i : ι
x₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
j : ι
hji : j ≠ i
⊢ x j ∈ s j

Tactic:
exact hx _

Result:
no goals