awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
x : E
y : ℝ
refine : (↑(Subtype.mk (p := fun (x : E × ℝ) ↦ x ∈ f'.domain) (0, N x - y) ⋯) : E × ℝ) + (x, y) ∈ s
⊢ ∃ (x_1 : ↥f'.domain), (↑x_1 : E × ℝ) + (x, y) ∈ s

Tactic:
refine ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
x : E
y : ℝ
⊢ (↑(Subtype.mk (p := fun (x : E × ℝ) ↦ x ∈ f'.domain) (0, N x - y) ⋯) : E × ℝ) + (x, y) ∈ s

Tactic:
simp only [s, ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
      sub_add_cancel, le_rfl]

Premises used: le_rfl, Set.mem_setOf_eq, zero_add, ConvexCone.mem_mk, Prod.fst_add, sub_add_cancel, Prod.snd_add
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
⊢ ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s

Tactic:
have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s := by
    rintro ⟨x, y⟩
    refine ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩
    simp only [s, ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
      sub_add_cancel, le_rfl]
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
obtain :
  ∀ (g : E × ℝ →ₗ[ℝ] ℝ) (g_eq : ∀ (x : ↥f'.domain), (g : (a : E × ℝ) → ℝ) (↑x : E × ℝ) = (↑f' : ↥f'.domain → ℝ) x)
    (g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)),
    ∃ (g : E →ₗ[ℝ] ℝ),
      (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x

Tactic:
obtain ⟨g, g_eq, g_nonneg⟩ := riesz_extension s f' hf'_nonneg hf'_dense

Premises used: riesz_extension
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥f'.domain), (g : (a : E × ℝ) → ℝ) (↑x : E × ℝ) = (↑f' : ↥f'.domain → ℝ) x
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
⊢ ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x

Tactic:
replace g_eq : ∀ (x : f.domain) (y : ℝ), g (x, y) = y - f x := fun x y ↦
    (g_eq ⟨(x, y), ⟨x.2, trivial⟩⟩).trans (sub_eq_neg_add _ _).symm
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x

Tactic:
⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩

Premises used: Real, LinearMap.inl, LinearMap.comp, And.intro, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
refine_1 : ∀ (x : ↥f.domain), (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
refine_2 : ∀ (x : E), (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x

Tactic:
refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
x : ↥f.domain
⊢ (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x

Tactic:
simp [g_eq x 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
x : E
⊢ -(g : (a : E × ℝ) → ℝ) (x, 0) =
    HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E × ℝ) → ℝ) (0, N x) : ℝ) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ)

Tactic:
simp [← map_sub, ← map_neg]

Premises used: map_sub, map_neg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
x : E
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E × ℝ) → ℝ) (0, N x) : ℝ) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ) =
    HSub.hSub (β := ℝ) (N x) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ)

Tactic:
simpa using g_eq 0 (N x)

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
x : E
⊢ HSub.hSub (β := ℝ) (N x) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ) ≤ N x

Tactic:
simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))

Premises used: le_refl, Prod.mk
-- Module: Mathlib.Analysis.Convex.Cone.Extension
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
x : E
calc :
  -(g : (a : E × ℝ) → ℝ) (x, 0) =
    HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E × ℝ) → ℝ) (0, N x) : ℝ) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ)
calc₁ :
  HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E × ℝ) → ℝ) (0, N x) : ℝ) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ) =
    HSub.hSub (β := ℝ) (N x) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ)
calc₂ : HSub.hSub (β := ℝ) (N x) ((g : (a : E × ℝ) → ℝ) (x, N x) : ℝ) ≤ N x
⊢ (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x

Tactic:
calc -g (x, 0) = g (0, N x) - g (x, N x) := by simp [← map_sub, ← map_neg]
      _ = N x - g (x, N x) := by simpa using g_eq 0 (N x)
      _ ≤ N x := by simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))

Premises used: Prod.mk, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
s : Set E
y : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual s) y ↔ ∀ ⦃x : E⦄, x ∈ s → 0 ≤ ⟪x, y⟫

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
h : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (innerDual ∅) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual ∅) ⊤

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual ∅) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
h : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (innerDual 0) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual 0) ⊤

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual 0) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
hx : Membership.mem (γ := ProperCone ℝ E) (innerDual univ) x
⊢ Membership.mem (γ := ProperCone ℝ E) ⊥ x

Tactic:
simpa using hx (mem_univ (-x))

Premises used: Set.mem_univ, Neg.neg
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
⊢ LE.le.{u_2} (α := ProperCone ℝ E) ⊥ (innerDual univ)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
s t : Set E
h : t ⊆ s
⊢ LE.le (α := ProperCone ℝ E) (innerDual s) (innerDual t)

Tactic:
fun _y hy _x hx ↦ hy (h hx)

Premises used: Set.Mem, setOf
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
h :
  ∀ (x_1 : E),
    Membership.mem (γ := ProperCone ℝ E) (innerDual {x}) x_1 ↔
      Membership.mem (γ := ProperCone ℝ E) (comap ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x) (positive ℝ ℝ)) x_1
⊢ Eq (α := ProperCone ℝ E) (innerDual {x}) (comap ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x) (positive ℝ ℝ))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x x_1 : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual {x}) x_1 ↔
    Membership.mem (γ := ProperCone ℝ E) (comap ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x) (positive ℝ ℝ)) x_1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
s t : Set E
⊢ Eq (α := ProperCone ℝ E) (innerDual (s ∪ t)) (innerDual s ⊓ innerDual t)

Tactic:
le_antisymm (le_inf (fun _ hx _ hy ↦ hx <| .inl hy) fun _ hx _ hy ↦ hx <| .inr hy)
    fun _ hx _ => Or.rec (fun h ↦ hx.1 h) (fun h ↦ hx.2 h)

Premises used: Or.rec, le_inf, le_antisymm, Or.inl, Or.inr
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
s : Set E
rw : Eq (α := ProperCone ℝ E) (innerDual ({x} ∪ s)) (innerDual {x} ⊓ innerDual s)
rw₁ rw₂ : Eq (α := ProperCone ℝ E) (innerDual {x} ⊓ innerDual s) (innerDual {x} ⊓ innerDual s)
⊢ Eq (α := ProperCone ℝ E) (innerDual (insert x s)) (innerDual {x} ⊓ innerDual s)

Tactic:
rw [insert_eq, innerDual_union]

Premises used: Set.insert_eq, ProperCone.innerDual_union
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
ι : Sort u_4
f : ι → Set E
h :
  ∀ (x : E),
    Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃ (i : ι), f i)) x ↔
      Membership.mem (γ := ProperCone ℝ E) (⨅ (i : ι), innerDual (f i)) x
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual (⋃ (i : ι), f i)) (⨅ (i : ι), innerDual (f i))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
ι : Sort u_4
f : ι → Set E
x : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := ProperCone ℝ E) (⨅ (i : ι), innerDual (f i)) x

Tactic:
simp [forall_comm (α := E)]

Premises used: forall_comm
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
S : Set (Set E)
h :
  ∀ (x : E),
    Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃₀ S)) x ↔
      Membership.mem (γ := ProperCone ℝ E) (sInf (innerDual '' S)) x
⊢ Eq (α := ProperCone ℝ E) (innerDual (⋃₀ S)) (sInf (innerDual '' S))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
S : Set (Set E)
x : E
⊢ Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃₀ S)) x ↔
    Membership.mem (γ := ProperCone ℝ E) (sInf (innerDual '' S)) x

Tactic:
simp [forall_comm (α := E)]

Premises used: forall_comm
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
obtain :
  ∀ (f : StrongDual ℝ E) (hf : ∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ))
    (hf₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (0 : ℝ)), ∃ (y : E), (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0
⊢ ∃ (y : E), (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0

Tactic:
obtain ⟨f, hf, hf₀⟩ := C.hyperplane_separation_point hx₀

Premises used: ProperCone.hyperplane_separation_point
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
f : StrongDual ℝ E
hf : ∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
hf₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ ∃ (y : E), (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0

Tactic:
⟨(InnerProductSpace.toDual ℝ E).symm f, ?_⟩

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.symm, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
f : StrongDual ℝ E
hf : ∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
hf₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (0 : ℝ)
refine :
  (∀ x ∈ C, 0 ≤ ⟪x, (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) f⟫) ∧
    ⟪x₀, (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) f⟫ < 0
⊢ ∃ (y : E), (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0

Tactic:
refine ⟨(InnerProductSpace.toDual ℝ E).symm f, ?_⟩
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
f : StrongDual ℝ E
hf : ∀ x ∈ C, LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
hf₀ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ (∀ x ∈ C, 0 ≤ ⟪x, (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) f⟫) ∧
    ⟪x₀, (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) f⟫ < 0

Tactic:
simpa [← real_inner_comm _ ((InnerProductSpace.toDual ℝ E).symm f), *]

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.symm, DFunLike.coe, real_inner_comm
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
C : ProperCone ℝ E
⊢ innerDual (↑(innerDual (↑C : Set E)) : Set E) = C

Tactic:
simpa using C.dual_flip_dual (innerₗ E)

Premises used: ProperCone.dual_flip_dual, innerₗ
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
simp :
  ∀ (x : ℕ → F) (x_1 : (x : ℕ) → E),
    (∀ (x : ℕ), x_1 x ∈ C) →
      (∀ (x_2 : ℕ), (f : (a : E) → F) (x_1 x_2) = x x_2) →
        Filter.Tendsto x Filter.atTop (nhds b) →
          ∀ (y : F), (∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ) → 0 ≤ ⟪b, y⟫_ℝ
⊢ b ∈ map f C →
    ∀ (y : F),
      Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑C : Set E))
          ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) →
        0 ≤ ⟪b, y⟫_ℝ

Tactic:
simp only [map, ClosedSubmodule.map, Submodule.closure, Submodule.topologicalClosure,
      AddSubmonoid.topologicalClosure, Submodule.coe_toAddSubmonoid, Submodule.map_coe,
      ContinuousLinearMap.coe_coe,
      ContinuousLinearMap.coe_restrictScalars', ClosedSubmodule.coe_toSubmodule,
      ClosedSubmodule.mem_mk, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
      mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, Classical.skolem, forall_and,
      mem_innerDual, ContinuousLinearMap.adjoint_inner_right, forall_exists_index, and_imp]

Premises used: Classical.skolem, Submodule.coe_toAddSubmonoid, and_imp, AddSubsemigroup.mem_mk, Set.mem_image, forall_exists_index, ContinuousLinearMap.coe_coe, mem_closure_iff_seq_limit, Submodule.closure, AddSubmonoid.mem_mk, SetLike.mem_coe, ClosedSubmodule.mem_mk, ProperCone.mem_innerDual, ContinuousLinearMap.coe_restrictScalars', ContinuousLinearMap.adjoint_inner_right, Submodule.topologicalClosure, ProperCone.map, Submodule.map_coe, AddSubmonoid.topologicalClosure, ClosedSubmodule.map, Submodule.mem_mk, ClosedSubmodule.coe_toSubmodule, forall_and
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
x : ℕ → F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
hx : ∀ (x_1 : ℕ), (f : (a : E) → F) (seq x_1) = x x_1
htends : Filter.Tendsto x Filter.atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
⊢ (⇑f : (a : E) → F) ∘ seq = x

Tactic:
funext hx

Premises used: funext
-- Module: Mathlib.Analysis.Convex.Cone.InnerDual
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
x : ℕ → F
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
hx : ∀ (x_1 : ℕ), (f : (a : E) → F) (seq x_1) = x x_1
htends : Filter.Tendsto x Filter.atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
⊢ ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)

Tactic:
obtain rfl : f ∘ seq = x := funext hx

Premises used: funext, rfl