-- 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)
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)
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)
refine_2₇ :
  ∀ (this : r * c ≤ 1 * (↑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 ≤ (↑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