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
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
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
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]
-- 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
rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
rwa₄ : r • r⁻¹ • x - -r • y ∈ s
rwa₅ : (r * r⁻¹) • x - -r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₆ : HSMul.hSMul (α := ℝ) 1 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
rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
rwa₄ : r • r⁻¹ • x - -r • y ∈ s
rwa₅ : (r * r⁻¹) • x - -r • y ∈ s
rwa₆ : HSMul.hSMul (α := ℝ) 1 x - -r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₇ : 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
rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
rwa₄ : r • r⁻¹ • x - -r • y ∈ s
rwa₅ : (r * r⁻¹) • x - -r • y ∈ s
rwa₆ : HSMul.hSMul (α := ℝ) 1 x - -r • y ∈ s
rwa₇ : x - -r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₈ : 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
rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
rwa₄ : r • r⁻¹ • x - -r • y ∈ s
rwa₅ : (r * r⁻¹) • x - -r • y ∈ s
rwa₆ : HSMul.hSMul (α := ℝ) 1 x - -r • y ∈ s
rwa₇ : x - -r • y ∈ s
rwa₈ : x + -(-r • y) ∈ s
⊢ -(r⁻¹ • x) - y ∈ s
have rwa₉ : 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 (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
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
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have this : -(r⁻¹ • x) - y ∈ s
Tactic: have : -(r⁻¹ • x) - y ∈ s := by
        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 (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
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
this : -(r⁻¹ • x) - y ∈ s
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have this₁ : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
Tactic: replace := le_c (r⁻¹ • ⟨x, hx⟩) 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2 : ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
refine_2 :
  ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
    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₁ : ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -r * c),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
refine_2 :
  ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -r * c),
    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₂ : ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -(r * c)),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
refine_2 :
  ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₂ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -(r * c)),
    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₃ : ∀ (this : r * c ≤ r * (↑f : ↥f.domain → ℝ) (r⁻¹ • 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)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
refine_2 :
  ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₂ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -(r * c)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₃ :
  ∀ (this : r * c ≤ r * (↑f : ↥f.domain → ℝ) (r⁻¹ • 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)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2₄ : ∀ (this : r * c ≤ r * r⁻¹ • (↑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)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] 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
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
this : (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c
refine_2 :
  ∀ (this : -r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -r * c),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₂ :
  ∀ (this : -(r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ≤ -(r * c)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₃ :
  ∀ (this : r * c ≤ r * (↑f : ↥f.domain → ℝ) (r⁻¹ • 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)
refine_2₄ :
  ∀ (this : r * c ≤ r * r⁻¹ • (↑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)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2₅ : ∀ (this : r * c ≤ r * (r⁻¹ * (↑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)
Tactic: rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
        smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] at this
Cleared hypotheses: this