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
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}
⊢ Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
have refine_1 : ∀ (x : ↥f.domain) (hx : (↑x : E) + -y ∈ s), Set.Nonempty.{u_2} (α := ↥f.domain) {x : ↥f.domain | -(↑x : E) - y ∈ s}
Tactic: rcases dense (-y) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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}
have hx₁ : -(↑(-x) : E) - y ∈ s
Tactic: rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
have this : (↑xp : E) + y + (-(↑xn : E) - y) ∈ s
Tactic: have := s.add_mem hxp hxn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
have this₁ : (↑(xp - xn) : E) ∈ s
Tactic: rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
have this₁ : 0 ≤ (↑f : ↥f.domain → ℝ) (xp - xn)
Tactic: replace := nonneg _ this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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)
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
have refine_2 : ∀ (this : 0 ≤ (↑f : ↥f.domain → ℝ) xp - (↑f : ↥f.domain → ℝ) xn), (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
Tactic: rwa [f.map_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
⊢ (↑f : ↥f.domain → ℝ) xn ≤ (↑f : ↥f.domain → ℝ) xp
have refine_2₁ : ∀ (this : (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
have refine_1 : f < f.supSpanSingleton y (-c) hy
Tactic: refine ⟨f.supSpanSingleton y (-c) hy, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
⊢ ∃ (g : E →ₗ.[ℝ] ℝ), f < g ∧ ∀ (x : ↥g.domain), (↑x : E) ∈ s → 0 ≤ (↑g : ↥g.domain → ℝ) x
have 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
Tactic: refine ⟨f.supSpanSingleton y (-c) hy, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
have refine_1 : ∀ (H : f.supSpanSingleton y (-c) hy ≤ f), False
Tactic: refine lt_iff_le_not_ge.2 ⟨f.left_le_sup _ _, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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
⊢ False
have H₁ : (f.supSpanSingleton y (-c) hy).domain ≤ f.domain
Tactic: replace H := LinearPMap.domain_mono.monotone H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
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
⊢ False
have H₁ : f.domain ≤ f.domain ∧ y ∈ (↑f.domain : Set E)
Tactic: rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
z : E
hz : z ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) z hz) : E) ∈ s
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) z hz)
have refine_2 : ∀ (x : E) (hx : x ∈ f.domain) (y' : E)
  (hy' :
    Membership.mem (γ := Submodule ℝ E)
      (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) sorry)) y')
  (hz : x + y' ∈ (f.supSpanSingleton y (-c) hy).domain)
  (hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz) : E) ∈ s),
  0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz)
Tactic: rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩
Cleared hypotheses: z, hz, hzs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
y' : E
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) y'
hz : x + y' ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz) : E) ∈ s
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz)
have refine_2 : ∀ (r : ℝ)
  (hy' :
    Membership.mem (γ := Submodule ℝ E)
      (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) sorry)) (r • y))
  (hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain)
  (hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz) : E) ∈ s),
  0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz)
Tactic: rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩
Cleared hypotheses: y', hy', hz, hzs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz)
have refine_2 : HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
  (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2 : ∀ (hr : r < 0),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
refine_2 :
  ∀ (hr : r < 0),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2₁ : ∀ (hr : r = 0),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
refine_2 :
  ∀ (hr : r < 0),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (hr : r = 0),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2₂ : ∀ (hr : 0 < r),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ -(r⁻¹ • x) - y ∈ s
have rwa : -r • (-(r⁻¹ • x) - y) ∈ s
Tactic: rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
rwa : -r • (-(r⁻¹ • x) - y) ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₁ : -r • -(r⁻¹ • x) - -r • y ∈ s
Tactic: rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
rwa : -r • (-(r⁻¹ • x) - y) ∈ s
rwa₁ : -r • -(r⁻¹ • x) - -r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₂ : -(-r • r⁻¹ • x) - -r • y ∈ s
Tactic: rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
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
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
rwa : -r • (-(r⁻¹ • x) - y) ∈ s
rwa₁ : -r • -(r⁻¹ • x) - -r • y ∈ s
rwa₂ : -(-r • r⁻¹ • x) - -r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
Tactic: rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]