awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
subset_convexHull 𝕜 _

Premises used: subset_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
exact subset_convexHull 𝕜 _

Premises used: subset_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
convexHull_empty

Premises used: convexHull_empty
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
exact convexHull_empty

Premises used: convexHull_empty
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
rw : ¬Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅
⊢ Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) s) ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]

Premises used: Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ ¬Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅

Tactic:
not_congr convexHull_eq_empty

Premises used: convexHull_eq_empty, not_congr
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ ¬Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅

Tactic:
exact not_congr convexHull_eq_empty

Premises used: convexHull_eq_empty, not_congr
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ segment 𝕜 x y ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
(convex_convexHull _ _).segment_subset (subset_convexHull _ _ hx) (subset_convexHull _ _ hy)

Premises used: subset_convexHull, convex_convexHull, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {x} : Set E) ({x} : Set E)

Tactic:
(convex_singleton x).convexHull_eq

Premises used: convex_singleton, Convex.convexHull_eq
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
rw : s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s
rw₁ : s.Nonempty
⊢ s = {x}

Tactic:
rw [← Set.Nonempty.subset_singleton_iff, ← hs]

Premises used: Set.Nonempty.subset_singleton_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
⊢ s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
subset_convexHull ..

Premises used: subset_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
⊢ s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
exact subset_convexHull ..

Premises used: subset_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
by_contra! : ∀ (hs : s = ∅), False
⊢ s.Nonempty

Tactic:
by_contra! hs
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs_1 : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
hs : s = ∅
⊢ False

Tactic:
simp_all [eq_comm (a := ∅)]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : s = {x}
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)

Tactic:
simp [hs]
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) 0 : Set E) (0 : Set E)

Tactic:
convexHull_singleton 0

Premises used: convexHull_singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (0 : Set E) ↔ s = 0

Tactic:
convexHull_eq_singleton

Premises used: convexHull_eq_singleton
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) {x, y} = segment 𝕜 x y

Tactic:
(convexHull_min ?_ <| convex_segment _ _).antisymm
    (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)

Premises used: Set.mem_singleton, segment_subset_convexHull, HasSubset.Subset.antisymm, Set.mem_insert, convexHull_min, Set.subset_insert, convex_segment
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
refine : {x, y} ⊆ segment 𝕜 x y
⊢ (convexHull 𝕜 : (a : Set E) → Set E) {x, y} = segment 𝕜 x y

Tactic:
refine (convexHull_min ?_ <| convex_segment _ _).antisymm
    (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)

Premises used: Set.mem_singleton, segment_subset_convexHull, HasSubset.Subset.antisymm, Set.mem_insert, convexHull_min, Set.subset_insert, convex_segment
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
rw : x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
⊢ {x, y} ⊆ segment 𝕜 x y

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y

Tactic:
⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩

Premises used: left_mem_segment, And.intro, right_mem_segment
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y

Tactic:
exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s ∪ t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (s ∪ t) : Set E)

Tactic:
ClosureOperator.closure_sup_closure_left _ _ _

Premises used: ClosureOperator.closure_sup_closure_left
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s ∪ (convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (s ∪ t) : Set E)

Tactic:
ClosureOperator.closure_sup_closure_right _ _ _

Premises used: ClosureOperator.closure_sup_closure_right
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
mp : Convex 𝕜 (s \ {x}) → x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
mpr : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) → Convex 𝕜 (s \ {x})
⊢ Convex 𝕜 (s \ {x}) ↔ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) x
⊢ x ∈ s \ {x}

Tactic:
rw [hsx.convexHull_eq] at hx

Premises used: Convex.convexHull_eq
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False

Tactic:
hx.2 (mem_singleton _)

Premises used: Set.mem_singleton, And.right
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False

Tactic:
exact hx.2 (mem_singleton _)

Premises used: Set.mem_singleton, And.right
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
h : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
rw : Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}))
⊢ Convex 𝕜 (s \ {x})

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
h : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}))

Tactic:
convex_convexHull 𝕜 _

Premises used: convex_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
h : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}))

Tactic:
exact convex_convexHull 𝕜 _

Premises used: convex_convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
mpr : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
⊢ Convex 𝕜 (s \ {x})

Tactic:
suffices h : s \ {x} = convexHull 𝕜 (s \ {x}) by
    rw [h]
    exact convex_convexHull 𝕜 _
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hx : y ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {y}) : Set E)
hy : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {y}) : Set E) y
⊢ False

Tactic:
hx hy
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hx : y ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {y}) : Set E)
hy : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {y}) : Set E) y
⊢ False

Tactic:
exact hx hy
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
⊢ s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})

Tactic:
exact
    Subset.antisymm (subset_convexHull 𝕜 _) fun y hy =>
      ⟨convexHull_min diff_subset hs hy, by
        rintro (rfl : y = x)
        exact hx hy⟩
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E → F
hf : IsLinearMap 𝕜 f
s : Set E
⊢ f '' (convexHull 𝕜 : (a : Set E) → Set E) s = (convexHull 𝕜 : (a : Set F) → Set F) (f '' s)

Tactic:
Set.Subset.antisymm
    (image_subset_iff.2 <|
      convexHull_min (image_subset_iff.1 <| subset_convexHull 𝕜 _)
        ((convex_convexHull 𝕜 _).is_linear_preimage hf))
    (convexHull_min (image_mono (subset_convexHull 𝕜 s)) <|
      (convex_convexHull 𝕜 s).is_linear_image hf)

Premises used: Set.Subset.antisymm, Iff.mpr, subset_convexHull, Set.image_mono, Convex.is_linear_preimage, convex_convexHull, Convex.is_linear_image, Iff.mp, convexHull_min, Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ₗ[𝕜] F
s : Set E
⊢ Eq.{u_3 + 1} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
f.isLinear.image_convexHull s

Premises used: IsLinearMap.image_convexHull, LinearMap.isLinear
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (s + t) ⊆
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E)

Tactic:
convexHull_min (add_subset_add (subset_convexHull _ _) (subset_convexHull _ _))
    (Convex.add (convex_convexHull 𝕜 s) (convex_convexHull 𝕜 t))

Premises used: subset_convexHull, Convex.add, convex_convexHull, Set.add_subset_add, convexHull_min
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
a : 𝕜
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (a • s) =
    HSMul.hSMul (β := Set E) a ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
(LinearMap.lsmul _ _ a).image_convexHull _ |>.symm

Premises used: LinearMap.lsmul, LinearMap.image_convexHull, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
h₁ :
  Subset.{u_3} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
h₂ :
  Subset.{u_3} (α := Set F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s) : Set F)
    (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set F)
⊢ Eq.{u_3 + 1} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
h₁ :
  Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s)) :
      Set E)
⊢ Subset.{u_3} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s)) :
      Set E)

Tactic:
convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)

Premises used: convex_convexHull, convexHull_min, Set.image, Convex.affine_preimage, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
h₁ :
  s ⊆ preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s)) :
      Set E)

Tactic:
refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)

Premises used: convex_convexHull, convexHull_min, Set.image, Convex.affine_preimage, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
h₁ :
  Subset.{u_3} (α := Set F) ((⇑f : (a : E) → F) '' s) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
⊢ s ⊆ preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
rw [← Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset.{u_3} (α := Set F) ((⇑f : (a : E) → F) '' s) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
subset_convexHull 𝕜 (f '' s)

Premises used: subset_convexHull, Set.image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset.{u_3} (α := Set F) ((⇑f : (a : E) → F) '' s) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))

Tactic:
exact subset_convexHull 𝕜 (f '' s)

Premises used: subset_convexHull, Set.image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset.{u_3} (α := Set F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s) : Set F)
    (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set F)

Tactic:
convexHull_min (Set.image_mono (subset_convexHull 𝕜 s))
      ((convex_convexHull 𝕜 s).affine_image f)

Premises used: Convex.affine_image, subset_convexHull, Set.image_mono, convex_convexHull, convexHull_min
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset.{u_3} (α := Set F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s) : Set F)
    (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set F)

Tactic:
exact convexHull_min (Set.image_mono (subset_convexHull 𝕜 s))
      ((convex_convexHull 𝕜 s).affine_image f)

Premises used: Convex.affine_image, subset_convexHull, Set.image_mono, convex_convexHull, convexHull_min
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ (↑(affineSpan 𝕜 s) : Set E)

Tactic:
convexHull_min (subset_affineSpan 𝕜 s) (affineSpan 𝕜 s).convex

Premises used: AffineSubspace.convex, subset_affineSpan, affineSpan, convexHull_min
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)

Tactic:
le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))

Premises used: subset_convexHull, le_antisymm, affineSpan_mono
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
refine : LE.le (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)
⊢ Eq (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)

Tactic:
refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))

Premises used: subset_convexHull, le_antisymm, affineSpan_mono
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
rw : (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ (↑(affineSpan 𝕜 s) : Set E)
⊢ LE.le (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)

Tactic:
rw [affineSpan_le]

Premises used: affineSpan_le
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ (↑(affineSpan 𝕜 s) : Set E)

Tactic:
convexHull_subset_affineSpan s

Premises used: convexHull_subset_affineSpan
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ (↑(affineSpan 𝕜 s) : Set E)

Tactic:
exact convexHull_subset_affineSpan s

Premises used: convexHull_subset_affineSpan