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

Tactic:
exact and_and_and_comm.1
    ⟨h.1 hx₁.1 hx₂.1 ⟨a, b, ha, hb, hab, congr_arg Prod.fst hx'⟩,
      h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congr_arg Prod.snd hx'⟩⟩

Result:
no goals

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

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

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✝ ∈ openSegment 𝕜 (x✝.1, x₁) (x✝.1, x₂)

Tactic:
rw [← Prod.image_mk_openSegment_right]

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✝ ∈ (fun y => (x✝.1, y)) '' openSegment 𝕜 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⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.2

Tactic:
rintro x₁ hx₁ x₂ hx₂ hx_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₁ = x✝.2 ∧ x₂ = x✝.2

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

Tactic:
constructor

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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1

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⦄, 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.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₂

Tactic:
exact ⟨_, hx_fst, rfl⟩

Result:
no goals