awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
fg_min_on : IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x

Tactic:
simpa only [hg0, hg1, comp_apply, mem_setOf_eq] using fg_min_on (right_mem_Icc.2 zero_le_one)

Premises used: Iff.mpr, Set.right_mem_Icc, Set.mem_setOf_eq, zero_le_one, Function.comp_apply
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmax : IsLocalMaxOn f s a
h_conc : ConcaveOn ℝ s f
⊢ IsMaxOn f s a

Tactic:
IsMinOn.of_isLocalMinOn_of_convexOn (β := βᵒᵈ) a_in_s h_localmax h_conc

Premises used: IsMaxOn, IsMinOn.of_isLocalMinOn_of_convexOn, IsMaxFilter
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
f : E → β
a : E
h_local_min : IsLocalMin f a
h_conv : ConvexOn ℝ univ f
⊢ ∀ (x : E), f a ≤ f x

Tactic:
fun x =>
  (IsMinOn.of_isLocalMinOn_of_convexOn (mem_univ a) (h_local_min.on univ) h_conv) (mem_univ x)

Premises used: Set.Mem, Set.univ, setOf, IsMinOn.of_isLocalMinOn_of_convexOn, IsLocalMin.on, Set.mem_univ
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
f : E → β
a : E
h_local_max : IsLocalMax f a
h_conc : ConcaveOn ℝ univ f
⊢ ∀ (x : E), f x ≤ f a

Tactic:
IsMinOn.of_isLocalMin_of_convex_univ (β := βᵒᵈ) h_local_max h_conc

Premises used: IsMinOn.of_isLocalMin_of_convex_univ
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
⊢ IsExtreme 𝕜 A A

Tactic:
⟨Subset.rfl, fun _ hx₁A _ _ _ _ _ ↦ hx₁A⟩

Premises used: Set.Subset.rfl, IsExtreme.mk
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
⊢ IsExtreme 𝕜 A A

Tactic:
IsExtreme.refl 𝕜 A

Premises used: IsExtreme.refl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B : Set E
x : E
h : IsExtreme 𝕜 A B
y z : E
hx : x ∈ A
hy : y ∈ A
hz : z ∈ B
hzxy rwa rwa₁ rwa₂ rwa₃ : z ∈ openSegment 𝕜 x y
⊢ z ∈ openSegment 𝕜 y x

Tactic:
rwa [openSegment_symm]

Premises used: openSegment_symm
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
⊢ IsExtreme 𝕜 A C

Tactic:
⟨hBC.subset.trans hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩

Premises used: IsExtreme.subset, HasSubset.Subset.trans, IsExtreme.mk
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
refine :
  ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxC : x ∈ C) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₁ ∈ C
⊢ IsExtreme 𝕜 A C

Tactic:
refine ⟨hBC.subset.trans hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C

Tactic:
hBC.left_mem_of_mem_openSegment
    (hAB.left_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx)
    (hAB.right_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx) hxC hx

Premises used: IsExtreme.subset, IsExtreme.left_mem_of_mem_openSegment, IsExtreme.right_mem_of_mem_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C

Tactic:
exact hBC.left_mem_of_mem_openSegment
    (hAB.left_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx)
    (hAB.right_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx) hxC hx

Premises used: IsExtreme.subset, IsExtreme.left_mem_of_mem_openSegment, IsExtreme.right_mem_of_mem_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
⊢ Std.Antisymm.{u_2 + 1} (α := Set E) (IsExtreme 𝕜)

Tactic:
⟨fun _ _ hAB hBA ↦ Subset.antisymm hBA.1 hAB.1⟩

Premises used: Set.Subset.antisymm, IsExtreme.subset, Std.Antisymm.mk
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
left_mem_of_mem_openSegment :
  ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B ∩ C → z ∈ openSegment 𝕜 x y → x ∈ B ∩ C
⊢ IsExtreme 𝕜 A (B ∩ C)

Tactic:
use Subset.trans inter_subset_left hAB.1

Premises used: IsExtreme.subset, Set.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∩ C

Tactic:
⟨hAB.left_mem_of_mem_openSegment hx₁A hx₂A hxB hx,
    hAC.left_mem_of_mem_openSegment hx₁A hx₂A hxC hx⟩

Premises used: IsExtreme.left_mem_of_mem_openSegment, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∩ C

Tactic:
exact ⟨hAB.left_mem_of_mem_openSegment hx₁A hx₂A hxB hx,
    hAC.left_mem_of_mem_openSegment hx₁A hx₂A hxC hx⟩
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAC : IsExtreme 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
⊢ IsExtreme 𝕜 B C

Tactic:
⟨hCB, fun _ hx₁B _ hx₂B _ hxC hx ↦ hAC.2 (hBA hx₁B) (hBA hx₂B) hxC hx⟩

Premises used: IsExtreme.left_mem_of_mem_openSegment, IsExtreme.mk
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabit : ∀ (inhabited_h : Inhabited ι), IsExtreme 𝕜 A (⋂ (i : ι), F i)
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)

Tactic:
inhabit ι
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)

Tactic:
⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩

Premises used: IsExtreme.subset, Inhabited.default, IsExtreme.mk, Set.iInter_subset_of_subset
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
refine :
  ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxF : Membership.mem (γ := Set E) (⋂ (i : ι), F i) x)
    (hx : x ∈ openSegment 𝕜 x₁ x₂), Membership.mem (γ := Set E) (⋂ (i : ι), F i) x₁
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)

Tactic:
refine ⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : Membership.mem (γ := Set E) (⋂ (i : ι), F i) x
hx : x ∈ openSegment 𝕜 x₁ x₂
rw : ∀ (hxF : ∀ (i : ι), x ∈ F i) (hx : x ∈ openSegment 𝕜 x₁ x₂) (i : ι), x₁ ∈ F i
⊢ Membership.mem (γ := Set E) (⋂ (i : ι), F i) x₁

Tactic:
rw [mem_iInter] at hxF ⊢

Premises used: Set.mem_iInter
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : ∀ (i : ι), x ∈ F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ ∀ (i : ι), x₁ ∈ F i

Tactic:
fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx

Premises used: IsExtreme.left_mem_of_mem_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : ∀ (i : ι), x ∈ F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ ∀ (i : ι), x₁ ∈ F i

Tactic:
exact fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx

Premises used: IsExtreme.left_mem_of_mem_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
⊢ Nonempty.{u_2 + 1} (↑F : Type u_2)

Tactic:
haveI := hF.to_subtype
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
this : Nonempty.{u_2 + 1} (↑F : Type u_2)
⊢ IsExtreme 𝕜 A (⋂ B ∈ F, B)

Tactic:
simpa only [iInter_subtype] using isExtreme_iInter fun i : F ↦ hA _ i.2

Premises used: Set.iInter_subtype, isExtreme_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂₀ F)

Tactic:
simpa [sInter_eq_biInter] using isExtreme_biInter hF hAF

Premises used: isExtreme_biInter, Set.sInter_eq_biInter
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
refine :
  ∀ (h : x ∈ extremePoints 𝕜 A) (x₁ : E) (hx₁ : x₁ ∈ A) (x₂ : E) (hx₂ : x₂ ∈ A) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₂ = x
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
refine ⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ openSegment 𝕜 x₁ x₂
apply : x ∈ openSegment 𝕜 x₂ x₁
⊢ x₂ = x

Tactic:
apply h.2 hx₂ hx₁

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ openSegment 𝕜 x₂ x₁

Tactic:
rwa [openSegment_symm]

Premises used: openSegment_symm
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x

Tactic:
.rfl

Premises used: Set.extremePoints, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
⊢ IsExtreme 𝕜 A {x} ↔ x ∈ extremePoints 𝕜 A

Tactic:
simp [isExtreme_iff, extremePoints]

Premises used: Set.extremePoints, isExtreme_iff
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
⊢ extremePoints 𝕜 A ⊆ A

Tactic:
fun _ hx ↦ hx.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) (extremePoints 𝕜 ∅) ∅

Tactic:
subset_empty_iff.1 extremePoints_subset

Premises used: Iff.mp, extremePoints_subset, Set.subset_empty_iff
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
⊢ Eq (α := Set E) (extremePoints 𝕜 {x}) {x}

Tactic:
extremePoints_subset.antisymm <| singleton_subset_iff.2 ⟨mem_singleton x, fun _ hx₁ _ _ _ ↦ hx₁⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, HasSubset.Subset.antisymm, And.intro, extremePoints_subset
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B : Set E
hBA : B ⊆ A
⊢ B ∩ extremePoints 𝕜 A ⊆ extremePoints 𝕜 B

Tactic:
fun _ ⟨hxB, hxA⟩ ↦ ⟨hxB, fun _ hx₁ _ hx₂ hx ↦ hxA.2 (hBA hx₁) (hBA hx₂) hx⟩

Premises used: Set.extremePoints, Membership.mem, Set.Subset, And.right, And.intro, _private.0.inter_extremePoints_subset_extremePoints_of_subset.match_1
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B : Set E
hAB : IsExtreme 𝕜 A B
x : E
⊢ x ∈ extremePoints 𝕜 B → x ∈ extremePoints 𝕜 A

Tactic:
simpa only [← isExtreme_singleton] using hAB.trans

Premises used: isExtreme_singleton, IsExtreme.trans
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B : Set E
hAB : IsExtreme 𝕜 A B
⊢ extremePoints 𝕜 B = B ∩ extremePoints 𝕜 A

Tactic:
Subset.antisymm (fun _ hx ↦ ⟨hx.1, hAB.extremePoints_subset_extremePoints hx⟩)
    (inter_extremePoints_subset_extremePoints_of_subset hAB.1)

Premises used: Set.Subset.antisymm, IsExtreme.subset, IsExtreme.extremePoints_subset_extremePoints, And.left, And.intro, inter_extremePoints_subset_extremePoints_of_subset
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
inst_4 : Subsingleton E
A : Set E
⊢ extremePoints 𝕜 A = A

Tactic:
subset_antisymm extremePoints_subset fun _ h ↦ ⟨h, fun _ _ _ _ _ ↦ Subsingleton.elim ..⟩

Premises used: subset_antisymm, And.intro, extremePoints_subset, Subsingleton.elim
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
A B : Set E
inst_4 : IsOrderedRing 𝕜
hA : Convex 𝕜 A
hAB : IsExtreme 𝕜 A B
⊢ Convex 𝕜 (A \ B)

Tactic:
convex_iff_openSegment_subset.2 fun _ ⟨hx₁A, hx₁B⟩ _ ⟨hx₂A, _⟩ _ hx ↦
    ⟨hA.openSegment_subset hx₁A hx₂A hx, fun hxB ↦ hx₁B (hAB.2 hx₁A hx₂A hxB hx)⟩

Premises used: Iff.mpr, IsExtreme.left_mem_of_mem_openSegment, convex_iff_openSegment_subset, Membership.mem, Convex.openSegment_subset, SDiff.sdiff, _private.0.IsExtreme.convex_diff.match_1, And.intro
-- 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
h : ∀ (x : E) (y : F), (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
⊢ extremePoints 𝕜 (s ×ˢ t) = extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

Tactic:
ext ⟨x, y⟩
-- 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
⊢ (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

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

Premises used: Set.extremePoints, Set.Mem, setOf, and_congr_right, and_and_and_comm, Iff.intro, Iff.trans
-- 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
h :
  ∀ (hx : (x, y) ∈ s ×ˢ t)
    (h :
      (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
        ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2)
    ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
h₁ :
  ∀ (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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1
h₂ :
  ∀ (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⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
⊢ (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

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

Premises used: and_congr_right, and_and_and_comm, Iff.intro, Iff.trans
-- 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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).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, y)
h₁ : x₁.1 = (x, y).1
h₂ : x₁.2 = (x, y).2
⊢ x₁ = (x, y)

Tactic:
ext
-- 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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).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, y)
⊢ x₁.1 = (x, y).1

Tactic:
h.1 hx₁.1 hx₂.1 ⟨a, b, ha, hb, hab, congrArg Prod.fst hx'⟩

Premises used: congrArg, Prod.fst, And.left, And.intro, Exists.intro
-- 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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).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, y)
⊢ x₁.1 = (x, y).1

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

Premises used: congrArg, Prod.fst, And.left, And.intro, Exists.intro
-- 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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).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, y)
⊢ x₁.2 = (x, y).2

Tactic:
h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congrArg Prod.snd hx'⟩

Premises used: congrArg, And.right, And.intro, Exists.intro, 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⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).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, y)
⊢ x₁.2 = (x, y).2

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

Premises used: congrArg, And.right, And.intro, Exists.intro, Prod.snd