awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : Membership.mem (γ := Set F) univ x
rw : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponent x) : Set F) (univ : Set F)
rw₁ : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) univ : Set F) (univ : Set F)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set F) univ univ
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)

Tactic:
rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]

Premises used: convexHull_univ, PreconnectedSpace.connectedComponent_eq_univ, connectedComponentIn_univ
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
⊢ AmpleSet.{u_1} (F := F) ∅

Tactic:
fun _ ↦ False.elim

Premises used: Set.Mem, False.elim, AmpleSet
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)

Tactic:
rcases hx with (h | h)
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)

Tactic:
have hx := hs x h
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)

Tactic:
have hx := ht x h
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)

Tactic:
rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h]
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
inl :
  Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)

Tactic:
rw [← Set.univ_subset_iff, ← hx]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
inr :
  Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)

Tactic:
rw [← Set.univ_subset_iff, ← hx]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
inl : connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
⊢ Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)

Tactic:
apply convexHull_mono

Premises used: convexHull_mono
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
inr : connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
⊢ Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)

Tactic:
apply convexHull_mono

Premises used: convexHull_mono
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
inl : s ⊆ s ∪ t
⊢ connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x

Tactic:
apply connectedComponentIn_mono

Premises used: connectedComponentIn_mono
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
inr : t ⊆ s ∪ t
⊢ connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x

Tactic:
apply connectedComponentIn_mono

Premises used: connectedComponentIn_mono
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
⊢ s ⊆ s ∪ t

Tactic:
apply subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
⊢ t ⊆ s ∪ t

Tactic:
apply subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
rw : Eq.{u_1 + 1} (α := Set F) (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) univ) univ
rw₁ : Eq.{u_1 + 1} (α := Set F) (range.{u_1, u_2 + 1} (ι := E) (⇑L : (a : E) → F)) univ
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set F) univ univ
⊢ Eq.{u_1 + 1} (α := Set F)
    (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) ((convexHull ℝ : (a : Set E) → Set E) (connectedComponentIn s x)))
    univ

Tactic:
rw [h x hx, image_univ, L.surjective.range_eq]

Premises used: Set.image_univ, ContinuousAffineEquiv.surjective, Function.Surjective.range_eq
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set E
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet.{u_1} (F := F) ((⇑L : (a : E) → F) '' s) ↔ AmpleSet s

Tactic:
⟨fun h ↦ (L.symm_image_image s) ▸ h.image L.symm, fun h ↦ h.image L⟩

Premises used: Eq.rec, ContinuousAffineEquiv.symm, Iff.intro, AmpleSet.image, ContinuousAffineEquiv.symm_image_image
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
rw : AmpleSet.{u_2} (F := E) ((⇑L.symm : (a : F) → E) '' s)
⊢ AmpleSet.{u_2} (F := E) ((⇑L : (a : E) → F) ⁻¹' s)

Tactic:
rw [← L.image_symm_eq_preimage]

Premises used: ContinuousAffineEquiv.image_symm_eq_preimage
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet.{u_2} (F := E) ((⇑L.symm : (a : F) → E) '' s)

Tactic:
h.image L.symm

Premises used: ContinuousAffineEquiv.symm, AmpleSet.image
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet.{u_2} (F := E) ((⇑L.symm : (a : F) → E) '' s)

Tactic:
exact h.image L.symm

Premises used: ContinuousAffineEquiv.symm, AmpleSet.image
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set F
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet.{u_2} (F := E) ((⇑L : (a : E) → F) ⁻¹' s) ↔ AmpleSet s

Tactic:
⟨fun h ↦ L.image_preimage s ▸ h.image L, fun h ↦ h.preimage L⟩

Premises used: ContinuousAffineEquiv.image_preimage, Eq.rec, AmpleSet.preimage, Iff.intro, AmpleSet.image
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
s : Set E
h : AmpleSet s
y : E
⊢ AmpleSet (y +ᵥ s)

Tactic:
h.image (ContinuousAffineEquiv.constVAdd ℝ E y)

Premises used: Real, ContinuousAffineEquiv.constVAdd, AmpleSet.image
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
s : Set E
y : E
⊢ AmpleSet (y +ᵥ s) ↔ AmpleSet s

Tactic:
AmpleSet.image_iff (ContinuousAffineEquiv.constVAdd ℝ E y)

Premises used: Real, AmpleSet.image_iff, ContinuousAffineEquiv.constVAdd
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
rw : ∀ (x : F), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) x
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (↑E : Set F)ᶜ x) : Set F) (univ : Set F)

Tactic:
rw [E.connectedComponentIn_eq_self_of_one_lt_codim hcodim hx, eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, Submodule.connectedComponentIn_eq_self_of_one_lt_codim
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
pos : ∀ (h : y ∈ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
neg : ∀ (h : y ∉ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
by_cases h : y ∈ E
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
rw : ¬E = ⊤
⊢ ∃ (z : F), z ∉ E

Tactic:
rw [← not_forall, ← Submodule.eq_top_iff']

Premises used: Submodule.eq_top_iff', Classical.not_forall
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
x y : F
hcodim : 1 < Module.rank ℝ (HasQuotient.Quotient F (B := Submodule ℝ F) ⊤)
hx : x ∈ (↑⊤ : Set F)ᶜ
h : Membership.mem (γ := Submodule ℝ F) ⊤ y
⊢ False

Tactic:
simp at hcodim
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
pos : ∀ (z : F) (hz : z ∉ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
obtain ⟨z, hz⟩ : ∃ z, z ∉ E := by
      rw [← not_forall, ← Submodule.eq_top_iff']
      rintro rfl
      simp at hcodim
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z)

Premises used: segment_subset_convexHull, mem_segment_sub_add
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
pos : y - z ∈ (↑E : Set F)ᶜ
pos₁ : y + z ∈ (↑E : Set F)ᶜ
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z)

Premises used: segment_subset_convexHull, mem_segment_sub_add
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ y - z ∈ (↑E : Set F)ᶜ

Tactic:
simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]

Premises used: sub_eq_add_neg, Submodule.add_mem_iff_right
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ y + z ∈ (↑E : Set F)ᶜ

Tactic:
simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]

Premises used: sub_eq_add_neg, Submodule.add_mem_iff_right
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∉ E
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
subset_convexHull ℝ (Eᶜ : Set F) h

Premises used: Real, Compl.compl, subset_convexHull, SetLike.coe
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∉ E
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y

Tactic:
exact subset_convexHull ℝ (Eᶜ : Set F) h

Premises used: Real, Compl.compl, subset_convexHull, SetLike.coe
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
hφcv : ConvexOn ℝ s φ
⊢ Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (preimage (β := E × ℝ) (⇑(LinearMap.prodMap LinearMap.id reLm) : (a : E × 𝕜) → E × ℝ)
      {p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2})

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
hφcv : ConvexOn ℝ s φ
⊢ Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (preimage (β := E × ℝ) (⇑(LinearMap.prodMap LinearMap.id reLm) : (a : E × 𝕜) → E × ℝ)
      {p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2})

Tactic:
have lem : { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 } =
    ((LinearMap.id : E →ₗ[ℝ] E).prodMap reLm) ⁻¹' { p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2 } := by simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
hφcv : ConvexOn ℝ s φ
lem :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (preimage (β := E × ℝ) (⇑(LinearMap.prodMap LinearMap.id reLm) : (a : E × 𝕜) → E × ℝ)
      {p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2})
⊢ Convex ℝ (E := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}

Tactic:
lem ▸ hφcv.convex_epigraph.linear_preimage _

Premises used: Eq.rec, ConvexOn.convex_epigraph, Eq.symm, Convex.linear_preimage
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
hφcv : ConvexOn ℝ s φ
lem :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (preimage (β := E × ℝ) (⇑(LinearMap.prodMap LinearMap.id reLm) : (a : E × 𝕜) → E × ℝ)
      {p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2})
⊢ Convex ℝ (E := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}

Tactic:
exact lem ▸ hφcv.convex_epigraph.linear_preimage _
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
⊢ Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)

Tactic:
simp [A]
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
⊢ Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)

Tactic:
have hC : { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 }
    = (Prod.map id ((Real.toEReal ∘ re) : 𝕜 → EReal)) ⁻¹' A := by simp [A]
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ IsClosed (X := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}

Tactic:
hC.symm ▸ IsClosed.preimage ?_ ?_

Premises used: Eq.rec, IsClosed.preimage, Eq.symm
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
refine_1 : Continuous (X := E × 𝕜) (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)))
refine_2 : IsClosed A
⊢ IsClosed (X := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}

Tactic:
refine hC.symm ▸ IsClosed.preimage ?_ ?_
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ Continuous (X := E × 𝕜) (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)))

Tactic:
continuous_id.prodMap <| continuous_coe_real_ereal.comp reCLM.cont

Premises used: Continuous.prodMap, Continuous.comp, RCLike.reCLM, continuous_coe_real_ereal, continuous_id, ContinuousLinearMap.cont
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ Continuous (X := E × 𝕜) (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)))

Tactic:
exact continuous_id.prodMap <| continuous_coe_real_ereal.comp reCLM.cont

Premises used: Continuous.prodMap, Continuous.comp, RCLike.reCLM, continuous_coe_real_ereal, continuous_id, ContinuousLinearMap.cont
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ IsClosed A

Tactic:
(lowerSemicontinuousOn_iff_isClosed_epigraph hsc).1
      (continuous_coe_real_ereal.comp_lowerSemicontinuousOn hφ_cont (EReal.coe_strictMono.monotone))

Premises used: StrictMono.monotone, setOf, lowerSemicontinuousOn_iff_isClosed_epigraph, continuous_coe_real_ereal, EReal.coe_strictMono, Iff.mp, Continuous.comp_lowerSemicontinuousOn, Real.toEReal
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ IsClosed A

Tactic:
exact (lowerSemicontinuousOn_iff_isClosed_epigraph hsc).1
      (continuous_coe_real_ereal.comp_lowerSemicontinuousOn hφ_cont (EReal.coe_strictMono.monotone))

Premises used: StrictMono.monotone, lowerSemicontinuousOn_iff_isClosed_epigraph, continuous_coe_real_ereal, EReal.coe_strictMono, Iff.mp, Continuous.comp_lowerSemicontinuousOn