marnautov

Fix PHP Auto Indent in CodeRunner for macOS

(https://coderunnerapp.com/)

Problem

CodeRunner adds one extra indentation level to all code after <?php.

<?php

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/wiener_levy_analytic_calculus_64feeb4f40/Basic.lean

/-! Elementary Fourier synthesis for absolutely summable coefficients.
These facts are convenient since mathlib's `lp` supplies the Banach space but
`Analysis/Fourier/AddCircle` only states the inverse theorem for coefficients
of an already continuous function. -/
noncomputable section
open Set MeasureTheory

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/tverberg_theorem_65d3218943/Colorful.lean

/-! Proof-only infrastructure: a finite colorful convex hull lemma. -/
noncomputable section
open scoped BigOperators RealInnerProductSpace
open Set Filter

namespace Tverberg65

Morgan-Griffiths

import Mathlib
import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

-- BEGIN INLINED FILE: Mathlib/Support/strong_subadditivity_fb0a335e77/AnalyticBase.lean
open ComplexOrder
open scoped MatrixOrder Matrix.Norms.L2Operator
open Filter

-- Continuity of the harmless, total version of x log x on self-adjoint matrix paths.
noncomputable section

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/stable_unstable_manifolds_da940581de/ComplexEigen.lean

open scoped TensorProduct
open Polynomial

namespace StableSupport
variable {W : Type*} [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ W]

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/shannon_capacity_pentagon_cf29d4694a/Foundation.lean

open scoped BigOperators
open BigOperators

namespace ShannonCap5Support

/-- the positive golden inverse -/

Morgan-Griffiths

import Mathlib
import Mathlib.Analysis.InnerProductSpace.Projection.Reflection

-- BEGIN INLINED FILE: Mathlib/Support/semilinear_poisson_radial_symmetry_0e8f4ce1bc/Linearize.lean
open scoped NNReal

namespace SemilinearPoissonSupport

/-- Difference quotients of a Lipschitz real nonlinearity can be chosen at
zero differences too. This is the bounded coefficient in the reflected

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/schauder_fixed_point_390f5406f7/CubeParity.lean
open scoped BigOperators
open Finset Function
namespace CubeParity
variable {D : Type*} [DecidableEq D]

lemma pair_sum_zero (S : Finset D) (A : D → D → ZMod 2)
    (hs : ∀ d ∈ S, ∀ e ∈ S, d ≠ e → A d e = A e d) :

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/sard_theorem_8feee3b75b/FlatTaylor.lean
open MeasureTheory Module
open scoped ContDiff NNReal ENNReal
namespace SardSupport
-- uniform Holder estimate for a bounded flat set
lemma holderOnWith_nat_of_flat
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [FiniteDimensional ℝ E]

Morgan-Griffiths

import Mathlib

-- BEGIN INLINED FILE: Mathlib/Support/runge_theorem_ac7707d823/Rational.lean

open scoped Polynomial BigOperators
open Polynomial Finset

noncomputable section

namespace RungeSupport