-- Mathlib/Analysis/Convex/Extreme.lean
theorem extremePoints_prod (s : Set E) (t : Set F) :
    (s ×ˢ t).extremePoints 𝕜 = s.extremePoints 𝕜 ×ˢ t.extremePoints 𝕜

Proof state:
case h.refine_1.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : x✝.2 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x✝.2 ∧ x₂ = x✝.2

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

Result:
case h.refine_1.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : x✝.2 ∈ openSegment 𝕜 x₁ x₂
⊢ x✝ ∈ openSegment 𝕜 (x✝.1, x₁) (x✝.1, x₂)

Proof state:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : x✝.1 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x✝.1 ∧ x₂ = x✝.1

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

Result:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : x✝.1 ∈ openSegment 𝕜 x₁ x₂
⊢ x✝ ∈ openSegment 𝕜 (x₁, x✝.2) (x₂, x✝.2)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
⊢ x✝ ∈ extremePoints 𝕜 (s ×ˢ t) ↔ x✝ ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

Tactic:
refine (and_congr_right fun hx ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩).trans and_and_and_comm

Result:
case h.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
⊢ (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.2

case h.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.2
⊢ ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝

Proof state:
case h.refine_1.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : x✝.2 ∈ openSegment 𝕜 x₁ x₂
⊢ x✝ ∈ (fun y => (x✝.1, y)) '' openSegment 𝕜 x₁ x₂

Tactic:
exact ⟨_, hx_snd, rfl⟩

Result:
no goals

Proof state:
case h.refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.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✝
⊢ x₁ = x✝ ∧ x₂ = x✝

Tactic:
simp_rw [Prod.ext_iff]

Result:
case h.refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.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✝
⊢ (x₁.1 = x✝.1 ∧ x₁.2 = x✝.2) ∧ x₂.1 = x✝.1 ∧ x₂.2 = x✝.2

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
⊢ extremePoints 𝕜 (s ×ˢ t) = extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
⊢ x✝ ∈ extremePoints 𝕜 (s ×ˢ t) ↔ x✝ ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

Proof state:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1

Tactic:
rintro x₁ hx₁ x₂ hx₂ hx_fst

Result:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : x✝.1 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x✝.1 ∧ x₂ = x✝.1

Proof state:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : x✝.1 ∈ openSegment 𝕜 x₁ x₂
⊢ x✝ ∈ openSegment 𝕜 (x₁, x✝.2) (x₂, x✝.2)

Tactic:
rw [← Prod.image_mk_openSegment_left]

Result:
case h.refine_1.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x✝ : E × F
hx : x✝ ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : x✝.1 ∈ openSegment 𝕜 x₁ x₂
⊢ x✝ ∈ (fun x => (x, x✝.2)) '' openSegment 𝕜 x₁ x₂