-- 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_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

Tactic:
exact fun i ↦ h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, congr_fun hx' _⟩

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
⊢ update x i x₂ j ∈ s j

Tactic:
rw [update_of_ne hji]

Result:
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

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
⊢ x ∈ extremePoints 𝕜 (univ.pi s) ↔ x ∈ univ.pi fun i => extremePoints 𝕜 (s i)

Tactic:
simp only [mem_extremePoints, mem_pi, mem_univ, true_imp_iff, @forall_and ι]

Result:
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

Proof state:
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

Tactic:
rintro x₁ hx₁ x₂ hx₂ hi

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₁ : π i
hx₁ : x₁ ∈ s i
x₂ : π i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x i ∧ x₂ = x i

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)
⊢ extremePoints 𝕜 (univ.pi s) = univ.pi fun i => extremePoints 𝕜 (s i)

Tactic:
ext x

Result:
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
⊢ x ∈ extremePoints 𝕜 (univ.pi s) ↔ x ∈ univ.pi fun i => extremePoints 𝕜 (s i)

Proof state:
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

Tactic:
rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hx'⟩

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₁ = x ∧ x₂ = x