awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
rw :
  (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
rw [mem_extremePoints]

Premises used: mem_extremePoints
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ ?_

Premises used: and_congr_right, forall₄_congr
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
refine :
  ∀ (hxA : x ∈ A) (x₁ : E) (h₁ : x₁ ∈ A) (x₂ : E) (h₂ : x₂ ∈ A),
    x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
refine and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ ?_

Premises used: and_congr_right, forall₄_congr
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
mp : (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
mpr : (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
mp : (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
rw [← insert_endpoints_openSegment]

Premises used: insert_endpoints_openSegment
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₂ : E
h₂ : x₂ ∈ A
h₁ : x ∈ A
H : x ∈ openSegment 𝕜 x x₂ → x = x ∧ x₂ = x
⊢ x = x ∨ x₂ = x

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
h₂ : x ∈ A
H : x ∈ openSegment 𝕜 x₁ x → x₁ = x ∧ x = x
⊢ x₁ = x ∨ x = x

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∨ x₂ = x

Tactic:
Or.inl <| (H hx).1

Premises used: And.left, Or.inl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₂ : E
h₂ : x₂ ∈ A
h₁ : x ∈ A
H : x ∈ openSegment 𝕜 x x₂ → x = x ∧ x₂ = x
⊢ x = x ∨ x₂ = x

Tactic:
exacts [Or.inl rfl, Or.inr rfl, Or.inl <| (H hx).1]

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
mpr : ∀ (hxA : x₁ ∈ A) (H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁) (hx : x₁ ∈ openSegment 𝕜 x₁ x₂), x₁ = x₁ ∧ x₂ = x₁
mpr₁ :
  ∀ (hxA : x₂ ∈ A) (H : x₂ ∈ segment 𝕜 x₁ x₂ → x₁ = x₂ ∨ x₂ = x₂) (hx : x₂ ∈ openSegment 𝕜 x₁ x₂), x₁ = x₂ ∧ x₂ = x₂
⊢ x₁ = x ∧ x₂ = x

Tactic:
rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)

Premises used: openSegment_subset_segment, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
hxA : x₁ ∈ A
H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁
hx : x₁ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₁ ∧ x₂ = x₁

Tactic:
⟨rfl, (left_mem_openSegment_iff.1 hx).symm⟩

Premises used: And.intro, Iff.mp, left_mem_openSegment_iff, Eq.symm, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ hxA : x₂ ∈ A
H : x₂ ∈ segment 𝕜 x₁ x₂ → x₁ = x₂ ∨ x₂ = x₂
hx : x₂ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₂ ∧ x₂ = x₂

Tactic:
⟨right_mem_openSegment_iff.1 hx, rfl⟩

Premises used: right_mem_openSegment_iff, And.intro, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
hxA : x₁ ∈ A
H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁
hx : x₁ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₁ ∧ x₂ = x₁

Tactic:
exacts [⟨rfl, (left_mem_openSegment_iff.1 hx).symm⟩, ⟨right_mem_openSegment_iff.1 hx, rfl⟩]
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
mpr : x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})

Tactic:
use fun hx ↦ ⟨hx.1, (isExtreme_singleton.2 hx).convex_diff hA⟩
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
⊢ x ∈ extremePoints 𝕜 A

Tactic:
mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ ?_⟩

Premises used: Iff.mpr, mem_extremePoints_iff_forall_segment, And.intro
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
mpr : ∀ (x₁ : E) (hx₁ : x₁ ∈ A) (x₂ : E) (hx₂ : x₂ ∈ A) (hx : x ∈ [x₁ -[𝕜] x₂]), x₁ = x ∨ x₂ = x
⊢ x ∈ extremePoints 𝕜 A

Tactic:
refine mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ ?_⟩

Premises used: Iff.mpr, mem_extremePoints_iff_forall_segment, And.intro
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
mpr :
  ∀ (hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}) (x₁ : E) (hx₁ : x₁ ∈ A)
    (x₂ : E) (hx₂ : x₂ ∈ A) (hx : x ∈ [x₁ -[𝕜] x₂]), x₁ = x ∨ x₂ = x
⊢ x₁ = x ∨ x₂ = x

Tactic:
rw [convex_iff_segment_subset] at hAx

Premises used: convex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
mpr : ∀ (h : x₁ ≠ x ∧ x₂ ≠ x), False
⊢ x₁ = x ∨ x₂ = x

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
h : x₁ ≠ x ∧ x₂ ≠ x
⊢ False

Tactic:
(hAx ⟨hx₁, fun hx₁ ↦ h.1 (mem_singleton_iff.2 hx₁)⟩
      ⟨hx₂, fun hx₂ ↦ h.2 (mem_singleton_iff.2 hx₂)⟩ hx).2 rfl

Premises used: Iff.mpr, Set.mem_singleton_iff, And.right, And.left, And.intro, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
h : x₁ ≠ x ∧ x₂ ≠ x
⊢ False

Tactic:
exact (hAx ⟨hx₁, fun hx₁ ↦ h.1 (mem_singleton_iff.2 hx₁)⟩
      ⟨hx₂, fun hx₂ ↦ h.2 (mem_singleton_iff.2 hx₂)⟩ hx).2 rfl

Premises used: Iff.mpr, Set.mem_singleton_iff, And.right, And.left, And.intro, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
rw : x ∈ A ∧ Convex 𝕜 (A \ {x}) ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
rw₁ :
  x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E) ↔
    x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
rw₂ rw₃ :
  x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E) ↔
    x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E)
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})

Tactic:
rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_diff]

Premises used: Convex.convex_remove_iff_notMem_convexHull_remove, Set.mem_diff, Convex.mem_extremePoints_iff_convex_diff
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx : Membership.mem (γ := Set E) (extremePoints 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) A)) x
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
    Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})

Tactic:
rw [(convex_convexHull 𝕜 _).mem_extremePoints_iff_convex_diff] at hx

Premises used: convex_convexHull, Convex.mem_extremePoints_iff_convex_diff
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
    Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})
by_contra : ∀ (h : x ∉ A), False
⊢ x ∈ A

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
    Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})
h : x ∉ A
⊢ False

Tactic:
(convexHull_min (subset_diff.2 ⟨subset_convexHull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2
    hx.1).2 rfl

Premises used: Iff.mpr, Set.disjoint_singleton_right, subset_convexHull, Set.subset_diff, And.right, And.left, And.intro, convexHull_min, rfl
-- Module: Mathlib.Analysis.Convex.Extreme
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
    Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})
h : x ∉ A
⊢ False

Tactic:
exact (convexHull_min (subset_diff.2 ⟨subset_convexHull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2
    hx.1).2 rfl

Premises used: Iff.mpr, Set.disjoint_singleton_right, subset_convexHull, Set.subset_diff, And.right, And.left, And.intro, convexHull_min, rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
⊢ ConcaveOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
hf

Premises used: ConcaveOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
⊢ ConvexOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
hf

Premises used: ConvexOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
⊢ StrictConcaveOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
hf

Premises used: StrictConcaveOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
⊢ StrictConvexOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
hf

Premises used: StrictConvexOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x : β
h : x ∈ s
y : β
h_1 : y ∈ s
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ _root_.id (a • x + b • y) ≤ _root_.id (a • x + b • y)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x : β
h : x ∈ s
y : β
h_1 : y ∈ s
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ a • _root_.id x + b • _root_.id y ≤ a • _root_.id x + b • _root_.id y

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • g x + b • g y ≤ g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • x + b • y) < a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • g x + b • g y < g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
t : Set E
hf : ConvexOn 𝕜 t f
hst : s ⊆ t
hs : Convex 𝕜 s
⊢ ConvexOn 𝕜 s f

Tactic:
⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩

Premises used: And.right, And.intro, ConvexOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
t : Set E
hf : ConcaveOn 𝕜 t f
hst : s ⊆ t
hs : Convex 𝕜 s
⊢ ConcaveOn 𝕜 s f

Tactic:
⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩

Premises used: And.right, And.intro, ConcaveOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
t : Set E
hf : StrictConvexOn 𝕜 t f
hst : s ⊆ t
hs : Convex 𝕜 s
⊢ StrictConvexOn 𝕜 s f

Tactic:
⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩

Premises used: StrictConvexOn, And.right, And.intro
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
t : Set E
hf : StrictConcaveOn 𝕜 t f
hst : s ⊆ t
hs : Convex 𝕜 s
⊢ StrictConcaveOn 𝕜 s f

Tactic:
⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩

Premises used: StrictConcaveOn, And.right, And.intro
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : ConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
⊢ ConvexOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
    (hg' (mem_image_of_mem f <| hf.1 hx hy ha hb hab)
            (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab) <|
          hf.2 hx hy ha hb hab).trans <|
      hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab⟩

Premises used: And.right, And.left, Set.mem_image_of_mem, And.intro, LE.le.trans, ConvexOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : ConcaveOn 𝕜 (f '' s) g
hf : ConcaveOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
⊢ ConcaveOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
    (hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab).trans <|
      hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab)
          (mem_image_of_mem f <| hf.1 hx hy ha hb hab) <|
        hf.2 hx hy ha hb hab⟩

Premises used: And.right, And.left, Set.mem_image_of_mem, And.intro, LE.le.trans, ConcaveOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : ConvexOn 𝕜 (f '' s) g
hf : ConcaveOn 𝕜 s f
hg' : AntitoneOn g (f '' s)
⊢ ConvexOn 𝕜 s (g ∘ f)

Tactic:
hg.dual.comp hf hg'

Premises used: ConcaveOn.comp, ConvexOn.dual, ConvexOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : ConcaveOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : AntitoneOn g (f '' s)
⊢ ConcaveOn 𝕜 s (g ∘ f)

Tactic:
hg.dual.comp hf hg'

Premises used: ConcaveOn, ConvexOn.comp, ConcaveOn.dual