Rescale To Unit Ball is Supersolution

theorem rescaleToUnitBall_isSupersolution    {x₀ : E} {R : ℝ} (hR : 0 < R)    (A : EllipticCoeff d (Metric.ball x₀ R))    {u : E → ℝ}    (hsuper : IsSupersolution A u) :    IsSupersolution (rescaleCoeffToUnitBall (d := d) hR A)      (rescaleToUnitBall (d := d) (x₀ := x₀) (R := R) u) := by  rcases hsuper with ⟨hu_mem, hsuper_ineq⟩  let hu : MemW1pWitness 2 u (Metric.ball x₀ R) := DeGiorgi.MemW1p.someWitness hu_mem  let huR := hu.rescale_to_unitBall (d := d) (x₀ := x₀) (R := R) hR  refine ⟨huR.memW1p, ?_⟩  intro hu' φ hφ0 hφ hφ_nonneg  let hφB := hφ.transportFromUnitBall (d := d) (x₀ := x₀) (R := R) hR  have hφB0 :      MemH01 (DeGiorgi.transportFromUnitBall (d := d) (x₀ := x₀) (R := R) φ)        (Metric.ball x₀ R) :=    MemW01p.transportFromUnitBall (d := d) (x₀ := x₀) (R := R) hR hφ0  have hball : 0 ≤ bilinFormOfCoeff A hu hφB := by    exact hsuper_ineq hu _ hφB0 hφB (by      intro x      exact hφ_nonneg (R⁻¹ • (x - x₀)))  have hconst_nonneg : 0 ≤ ((R ^ Module.finrank ℝ E)⁻¹ * R ^ (2 : ℕ) : ℝ) := by    positivity  calc    0 ≤ ((R ^ Module.finrank ℝ E)⁻¹ * R ^ (2 : ℕ)) * bilinFormOfCoeff A hu hφB :=      mul_nonneg hconst_nonneg hball    _ = bilinFormOfCoeff (rescaleCoeffToUnitBall (d := d) (x₀ := x₀) (R := R) hR A) huR hφ := by          symm          simpa [huR, hφB] using bilinForm_rescaleToUnitBall (d := d) (x₀ := x₀) (R := R) hR A hu hφ    _ = bilinFormOfCoeff (rescaleCoeffToUnitBall (d := d) (x₀ := x₀) (R := R) hR A) hu' hφ := by          symm          exact bilinFormOfCoeff_eq_left Metric.isOpen_ball _ hu' huR hφ