awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u
huv : u < v
hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b
hv₀ : v < 0
x : E
hx : x ∈ C
inr : ∀ (hx₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)), False
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
by_contra! hx₀
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K (↑C : Set E)
x₀ : E
hx₀_1 : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, (f : (a : E) → ℝ) a < u
huv : u < v
hv : ∀ b ∈ (↑C : Set E), v < (f : (a : E) → ℝ) b
hv₀ : v < 0
x : E
hx : x ∈ C
hx₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ False

Tactic:
simpa [hx₀.ne] using hv ((v * (f x)⁻¹) • x)
    (C.smul_mem hx <| le_of_lt <| mul_pos_of_neg_of_neg hv₀ <| inv_neg''.2 hx₀)

Premises used: Iff.mpr, HMul.hMul, le_of_lt, inv_neg'', ProperCone.smul_mem, Inv.inv, HSMul.hSMul, mul_pos_of_neg_of_neg, DFunLike.coe, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ (f : StrongDual ℝ E),
    (∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) ∧ LT.lt (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (0 : ℝ)

Tactic:
simpa [*] using C.hyperplane_separation (convex_singleton x₀)

Premises used: convex_singleton, ProperCone.hyperplane_separation
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
⊢ dual p.flip (↑(dual p (↑C : Set E)) : Set F) = C

Tactic:
le_antisymm (fun x ↦ ?_) subset_dual_dual

Premises used: ProperCone.subset_dual_dual, le_antisymm
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
refine : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (dual p.flip (↑(dual p (↑C : Set E)) : Set F)) x → x ∈ C
⊢ dual p.flip (↑(dual p (↑C : Set E)) : Set F) = C

Tactic:
refine le_antisymm (fun x ↦ ?_) subset_dual_dual

Premises used: ProperCone.subset_dual_dual, le_antisymm
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
x : E
simp :
  (∀ ⦃x_1 : F⦄,
      (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) →
        LE.le (α := ℝ) (0 : ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)) →
    x ∈ C
⊢ Membership.mem (γ := ProperCone ℝ E) (dual p.flip (↑(dual p (↑C : Set E)) : Set F)) x → x ∈ C

Tactic:
simp only [mem_dual, SetLike.mem_coe]

Premises used: ProperCone.mem_dual, SetLike.mem_coe
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
x : E
contrapose! :
  x ∉ C →
    ∃ (x_1 : F),
      (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) ∧
        LT.lt (α := ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ (∀ ⦃x_1 : F⦄,
      (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) →
        LE.le (α := ℝ) (0 : ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)) →
    x ∈ C

Tactic:
contrapose!
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) E (F →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
x : E
⊢ x ∉ C →
    ∃ (x_1 : F),
      (∀ ⦃x : E⦄, x ∈ C → LE.le (α := ℝ) (0 : ℝ) ((((p : (a : E) → F →ₗ[ℝ] ℝ) x : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) x_1 : ℝ)) ∧
        LT.lt (α := ℝ) ((((p.flip : (a : F) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simpa [p.flip.toContPerfPair.surjective.exists] using C.hyperplane_separation_point

Premises used: Function.Surjective.exists, LinearEquiv.surjective, ProperCone.hyperplane_separation_point, LinearMap.toContPerfPair, LinearMap.flip
-- Module: Mathlib.Analysis.Convex.Cone.Dual
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup F
inst_5 : Module ℝ E
inst_6 : ContinuousSMul ℝ E
inst_7 : LocallyConvexSpace ℝ E
inst_8 : Module ℝ F
p : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) F (E →ₗ[ℝ] ℝ)
inst_9 : p.IsContPerfPair
C : ProperCone ℝ E
⊢ dual p (↑(dual p.flip (↑C : Set E)) : Set F) = C

Tactic:
C.dual_flip_dual p.flip

Premises used: LinearMap.mk₂'ₛₗ, ProperCone.dual_flip_dual, LinearMap.flip
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
⊢ ∃ (y : E), Membership.mem (γ := Submodule ℝ E) ⊤ y ∧ y ∉ f.domain

Tactic:
SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)

Premises used: Iff.mpr, SetLike.exists_of_lt, Set.Mem, lt_top_iff_ne_top
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
obtain :
  ∀ (y : E) (hy : y ∉ f.domain),
    ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x

Tactic:
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)

Premises used: Iff.mpr, SetLike.exists_of_lt, lt_top_iff_ne_top, LinearPMap.domain
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
this : (upperBounds Sn ∩ lowerBounds Sp).Nonempty
⊢ ∃ (c : ℝ),
    (∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c) ∧
      ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x

Tactic:
simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this

Premises used: lowerBounds, upperBounds, Set.Nonempty, Set.forall_mem_image
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
suffices : (upperBounds Sn ∩ lowerBounds Sp).Nonempty
⊢ ∃ (c : ℝ),
    (∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c) ∧
      ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x

Tactic:
suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
      simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
⊢ (upperBounds Sn ∩ lowerBounds Sp).Nonempty

Tactic:
exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_

Premises used: exists_between_of_forall_le, Set.Nonempty.image, LinearPMap.toFun'
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
refine_1 : Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
refine_2 : ∀ x ∈ Sn, ∀ y ∈ Sp, x ≤ y
⊢ (upperBounds Sn ∩ lowerBounds Sp).Nonempty

Tactic:
refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_

Premises used: exists_between_of_forall_le, Set.Nonempty.image, LinearPMap.toFun'
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
refine_1 :
  ∀ (x : ↥f.domain) (hx : (↑x : E) + -y ∈ s), Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
⊢ Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}

Tactic:
rcases dense (-y) with ⟨x, hx⟩

Premises used: Neg.neg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
x : ↥f.domain
hx : (↑x : E) + -y ∈ s
⊢ -(↑(-x) : E) - y ∈ s

Tactic:
rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx

Premises used: sub_eq_add_neg, neg_neg, NegMemClass.coe_neg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
x : ↥f.domain
hx : -(↑(-x) : E) - y ∈ s
⊢ Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}

Tactic:
⟨_, hx⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
x : ↥f.domain
hx : -(↑(-x) : E) - y ∈ s
⊢ Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}

Tactic:
exact ⟨_, hx⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
xn : ↥f.domain
hxn : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s} xn
xp : ↥f.domain
hxp : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | (↑x : E) + y ∈ s} xp
⊢ (↑xp : E) + y + (-(↑xn : E) - y) ∈ s

Tactic:
have := s.add_mem hxp hxn
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
xn : ↥f.domain
hxn : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s} xn
xp : ↥f.domain
hxp : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | (↑x : E) + y ∈ s} xp
this : (↑xp : E) + y + (-(↑xn : E) - y) ∈ s
⊢ (↑(xp - xn) : E) ∈ s

Tactic:
rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this

Premises used: AddSubgroupClass.coe_sub, add_assoc, sub_eq_add_neg, add_sub_cancel
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
xn : ↥f.domain
hxn : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s} xn
xp : ↥f.domain
hxp : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | (↑x : E) + y ∈ s} xp
this : (↑(xp - xn) : E) ∈ s
⊢ 0 ≤ (↑f : ↥f.domain → ℝ) (xp - xn)

Tactic:
replace := nonneg _ this
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | (↑x : E) + y ∈ s}
Sn : Set ℝ := (↑f : ↥f.domain → ℝ) '' {x : ↥f.domain | -(↑x : E) - y ∈ s}
xn : ↥f.domain
hxn : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s} xn
xp : ↥f.domain
hxp : Membership.mem (γ := Set ↥f.domain) {x : ↥f.domain | (↑x : E) + y ∈ s} xp
this : 0 ≤ (↑f : ↥f.domain → ℝ) (xp - xn)
refine_2 :
  ∀ (this : 0 ≤ (↑f : ↥f.domain → ℝ) xp - (↑f : ↥f.domain → ℝ) xn), (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (this : (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp), (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp

Tactic:
rwa [f.map_sub, sub_nonneg] at this

Premises used: LinearPMap.map_sub, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
obtain :
  ∀ (c : ℝ) (le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c)
    (c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x),
    ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x

Tactic:
obtain ⟨c, le_c, c_le⟩ :
      ∃ c, (∀ x : f.domain, -(x : E) - y ∈ s → f x ≤ c) ∧
        ∀ x : f.domain, (x : E) + y ∈ s → c ≤ f x := by
    set Sp := f '' { x : f.domain | (x : E) + y ∈ s }
    set Sn := f '' { x : f.domain | -(x : E) - y ∈ s }
    suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
      simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
    refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_
    · rcases dense (-y) with ⟨x, hx⟩
      rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
      exact ⟨_, hx⟩
    rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
    have := s.add_mem hxp hxn
    rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
    replace := nonneg _ this
    rwa [f.map_sub, sub_nonneg] at this
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x

Tactic:
⟨f.supSpanSingleton y (-c) hy, ?_, ?_⟩

Premises used: And.intro, Exists.intro, LinearPMap.supSpanSingleton, Neg.neg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
refine_1 : f < f.supSpanSingleton y (-c) hy
refine_2 :
  ∀ (x : ↥(f.supSpanSingleton y (-c) hy).domain),
    (↑x : E) ∈ s → 0 ≤ (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ) x
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x

Tactic:
refine ⟨f.supSpanSingleton y (-c) hy, ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
⊢ f < f.supSpanSingleton y (-c) hy

Tactic:
lt_iff_le_not_ge.2 ⟨f.left_le_sup _ _, fun H => ?_⟩

Premises used: Iff.mpr, LinearPMap.left_le_sup, lt_iff_le_not_ge, And.intro
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
refine_1 : ∀ (H : f.supSpanSingleton y (-c) hy ≤ f), False
⊢ f < f.supSpanSingleton y (-c) hy

Tactic:
refine lt_iff_le_not_ge.2 ⟨f.left_le_sup _ _, fun H => ?_⟩

Premises used: Iff.mpr, LinearPMap.left_le_sup, lt_iff_le_not_ge, And.intro
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
H : f.supSpanSingleton y (-c) hy ≤ f
⊢ (f.supSpanSingleton y (-c) hy).domain ≤ f.domain

Tactic:
replace H := LinearPMap.domain_mono.monotone H
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
H : (f.supSpanSingleton y (-c) hy).domain ≤ f.domain
⊢ f.domain ≤ f.domain ∧ y ∈ (↑f.domain : Set E)

Tactic:
rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H

Premises used: Set.singleton_subset_iff, LinearPMap.domain_supSpanSingleton, sup_le_iff, Submodule.span_le
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
H : f.domain ≤ f.domain ∧ y ∈ (↑f.domain : Set E)
⊢ False

Tactic:
hy H.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
H : f.domain ≤ f.domain ∧ y ∈ (↑f.domain : Set E)
⊢ False

Tactic:
exact hy H.2

Premises used: And.right