awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have refine_2 : ∀ (x : E), (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x
Tactic: refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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 ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x
have calc : -(g : (a : E × ℝ) → ℝ) (x, 0) =
  HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E × ℝ) → ℝ) (0, N x) : ℝ) ((g : (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))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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) : ℝ)
⊢ (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x
have 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) : ℝ)
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))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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) : ℝ)
⊢ (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) x ≤ N x
have calc₂ : HSub.hSub (β := ℝ) (N x) ((g : (a : E × ℝ) → ℝ) (x, N 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))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual ∅) ⊤
have h : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (innerDual ∅) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual 0) ⊤
have h : ∀ (x : E), Membership.mem (γ := ProperCone ℝ E) (innerDual 0) x ↔ Membership.mem (γ := ProperCone ℝ E) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
⊢ Eq (α := ProperCone ℝ E) (innerDual {x}) (comap ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x) (positive ℝ ℝ))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x : E
s : Set E
⊢ Eq (α := ProperCone ℝ E) (innerDual (insert x s)) (innerDual {x} ⊓ innerDual s)
have rw : Eq (α := ProperCone ℝ E) (innerDual ({x} ∪ s)) (innerDual {x} ⊓ innerDual s)
Tactic: rw [insert_eq, innerDual_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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)
⊢ Eq (α := ProperCone ℝ E) (innerDual (insert x s)) (innerDual {x} ⊓ innerDual s)
have rw₁ : Eq (α := ProperCone ℝ E) (innerDual {x} ⊓ innerDual s) (innerDual {x} ⊓ innerDual s)
Tactic: rw [insert_eq, innerDual_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
ι : Sort u_4
f : ι → Set E
⊢ Eq.{u_2 + 1} (α := ProperCone ℝ E) (innerDual (⋃ (i : ι), f i)) (⨅ (i : ι), innerDual (f i))
have h : ∀ (x : E),
  Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := ProperCone ℝ E) (⨅ (i : ι), innerDual (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
S : Set (Set E)
⊢ Eq (α := ProperCone ℝ E) (innerDual (⋃₀ S)) (sInf (innerDual '' S))
have h : ∀ (x : E),
  Membership.mem (γ := ProperCone ℝ E) (innerDual (⋃₀ S)) x ↔
    Membership.mem (γ := ProperCone ℝ E) (sInf (innerDual '' S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ (y : E), (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0
have 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
Tactic: obtain ⟨f, hf, hf₀⟩ := C.hyperplane_separation_point hx₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
have 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
Tactic: refine ⟨(InnerProductSpace.toDual ℝ E).symm f, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
⊢ 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⟫_ℝ
have 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⟫_ℝ
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (hypothesis)
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⟫_ℝ
⊢ 0 ≤ ⟪b, y⟫_ℝ
have hx₁ : ∀ (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
Cleared hypotheses: x, hx, htends
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (hypothesis)
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⟫_ℝ
hx₁ : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
⊢ 0 ≤ ⟪b, y⟫_ℝ
have htends₁ : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
Tactic: obtain rfl : f ∘ seq = x := funext hx
Cleared hypotheses: x, hx, htends
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (hypothesis)
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
seq : (x : ℕ) → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪(f : (a : E) → F) x, y⟫_ℝ
hx : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((f : (a : E) → F) (seq x) : F) (((⇑f : (a : E) → F) ∘ seq) x : F)
htends : Filter.Tendsto ((⇑f : (a : E) → F) ∘ seq) Filter.atTop (nhds b)
⊢ 0 ≤ ⟪b, y⟫_ℝ
have h : ∀ (n : ℕ), 0 ≤ ⟪(f : (a : E) → F) (seq n), y⟫_ℝ
Tactic: have h n : 0 ≤ ⟪f (seq n), y⟫_ℝ := by simpa [real_inner_comm] using hinner (hmem n)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
h :
  ∀ (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⟫_ℝ
⊢ b ∈ map f C
have contrapose! : ∀ (h : 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) ∧
      ⟪b, y⟫_ℝ < 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
h : 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) ∧
      ⟪b, y⟫_ℝ < 0
have obtain : ∀ (y : F) (hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ) (hyb : ⟪b, y⟫_ℝ < 0),
  ∃ (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) ∧
      ⟪b, y⟫_ℝ < 0
Tactic: obtain ⟨y, hxy, hyb⟩ := (C.map f).hyperplane_separation' h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
⊢ ∃ (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) ∧
      ⟪b, y⟫_ℝ < 0
have refine : ∀ (x : E) (hx : x ∈ (↑C : Set E)),
  LE.le (α := ℝ) (0 : ℝ)
    (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) :
      ℝ)
Tactic: refine ⟨y, fun x hx ↦ ?_, hyb⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.InnerDual (goal)
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
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : b ∉ map f K
⊢ ∃ (y : F),
    Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E) ∧
      ⟪b, y⟫_ℝ < 0
have contrapose! : ∀
  (disj :
    ∀ (y : F)
      (_ :
        Membership.mem (α := E) (γ := ProperCone ℝ E) (innerDual (↑K : Set E))
          ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) f : F →L[ℝ] E) : (a : F) → E) y : E)),
      0 ≤ ⟪b, y⟫_ℝ),
  b ∈ map f K
Tactic: contrapose! disj
Cleared hypotheses: disj
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
⊢ Membership.mem (γ := PointedCone R (Dual R M)) (dual (Dual.eval R M) (↑C : Set M)) (b.coord i)
have refine : Membership.mem (γ := Submodule { c : R // 0 ≤ c } (M →ₗ[R] R))
  (dual (Dual.eval R M) (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)) (b.coord i)
Tactic: refine dual_le_dual hC ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : (↑C : Set M) ⊆ (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)
i : ι
⊢ Membership.mem (γ := PointedCone R (Dual R M)) (dual (Dual.eval R M) (↑C : Set M)) (b.coord i)
have refine : Membership.mem (γ := Submodule { c : R // 0 ≤ c } (M →ₗ[R] R))
  (dual (Dual.eval R M) (↑(hull R (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → M))) : Set M)) (b.coord i)
Tactic: classical
  refine dual_le_dual hC ?_
  simp [Finsupp.single_apply, ite_nonneg zero_le_one le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_simp : C₁.IsSimplicial
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have obtain : ∀ (s : Set E) (hs_fin : s.Finite) (hs_lin : LinearIndepOn ℝ id s) (hs_span : hull ℝ s = C₁),
  Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
Tactic: obtain ⟨s, hs_fin, hs_lin, hs_span⟩ := h₁_simp
Cleared hypotheses: h₁_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have haveI : ∀ (this : Fintype (↑s : Type u_1)),
  Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
Tactic: haveI : Fintype s := hs_fin.fintype
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
hx : x ∈ (↑(hull ℝ s) : Set E)
⊢ x ∈ (↑(Submodule.span ℝ s) : Set E)
have hx₁ : ∃ (c : E →₀ ℝ),
  (↑c.support : Set E) ⊆ s ∧
    (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) ∧ (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x
Tactic: rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
x : E
hx :
  ∃ (c : E →₀ ℝ),
    (↑c.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) ∧ (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x
⊢ x ∈ (↑(Submodule.span ℝ s) : Set E)
have obtain : ∀ (c : E →₀ ℝ) (hc_supp : (↑c.support : Set E) ⊆ s),
  (∀ (y : E), LE.le (α := ℝ) (0 : ℝ) ((c : (a : E) → ℝ) y : ℝ)) →
    ∀ (hc_sum : (c.sum fun (m : E) (r : ℝ) ↦ r • m) = x), x ∈ (↑(Submodule.span ℝ s) : Set E)
Tactic: obtain ⟨c, hc_supp, _, hc_sum⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
Tactic: have hull_sub_span : (hull ℝ s : Set E) ⊆ Submodule.span ℝ s := by
    intro x hx
    rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx
    obtain ⟨c, hc_supp, _, hc_sum⟩ := hx
    exact hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))