Lint to mathlib standards

Author: YaelDillies

LeanCamCombi.lean

@@ -13,7 +13,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 import LeanCamCombi.Mathlib.Probability.Distributions.Bernoulli
 import LeanCamCombi.Mathlib.Probability.HasLaw
-import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter
 import LeanCamCombi.PlainCombi.ProbLYM

LeanCamCombi/ExtrProbCombi/BollobasContainment.lean

@@ -20,8 +20,8 @@ open scoped MeasureTheory  ENNReal NNReal SimpleGraph Topology unitInterval
 
 namespace SimpleGraph
 variable {V W Ω : Type*} [Fintype W] {G : ℕ → Ω → SimpleGraph V} (H : SimpleGraph W)
-  [Fintype H.edgeSet] [∀ n ω, DecidableRel (G n ω).Adj] [MeasurableSpace Ω] (μ : Measure Ω)
-  [IsProbabilityMeasure μ] {p : ℕ → I} (hG : ∀ n, IsBinomialRandom (G n) (p n) μ)
+  [Fintype H.edgeSet] [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {p : ℕ → I}
+  (hG : ∀ n, IsBinomialRandom (G n) (p n) μ)
 
 /-- **Bollobás' Graph Containment Lemma**, zero statement -/
 lemma zero_statement

LeanCamCombi/GraphTheory/ExampleSheet1.lean

@@ -76,7 +76,7 @@ Show that if $$G$$ is acyclic and $$|G| ≥ 1$$, then $$e(G) ≤ n − 1$$.
 -/
 
 -- Note: The statement is true without `nonempty α` due to nat subtraction.
-lemma q5 [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.IsAcyclic) :
+lemma q5 [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.IsAcyclic) :
     G.edgeFinset.card ≤ card α - 1 := by
   cases isEmpty_or_nonempty α
   · simp
@@ -153,7 +153,7 @@ Show that the possible clique numbers for a regular graph on $$n$$ vertices are
 $$1, 2, \dots, n/2$$ and $$n$$.
 -/
 
-lemma q10 [Fintype α] [DecidableEq α] (n : ℕ) :
+lemma q10 [Fintype α] (n : ℕ) :
     (∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj) (k : _),
         G.IsRegularOfDegree k ∧ cliqueNum G = n) ↔
       n ≤ card α / 2 ∨ n = card α :=

LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean

@@ -25,6 +25,7 @@ lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {A :
 
 end IsApproximateSubgroup
 
+set_option linter.flexible false in
 open Finset in
 open scoped RightActions in
 @[to_additive]

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Density.lean

@@ -8,7 +8,6 @@ Rename `edgeDensity` to `edgeDensityBtw`
 -/
 
 open Finset
-open scoped Classical
 
 namespace SimpleGraph
 variable {α : Type*} [Fintype α] (G : SimpleGraph α) [Fintype G.edgeSet]
@@ -18,8 +17,9 @@ variable {α : Type*} [Fintype α] (G : SimpleGraph α) [Fintype G.edgeSet]
 In other words, it is half of its average degree. -/
 def edgeDensity' : ℚ≥0 := #G.edgeFinset / Fintype.card α
 
+open scoped Classical in
 /-- The maximum edge density of a subgraph of a graph. -/
 noncomputable def maxEdgeSubdensity : ℚ≥0 :=
-  Finset.univ.sup' Finset.univ_nonempty fun G' : G.Subgraph ↦ G'.coe.edgeDensity'
+  univ.sup' univ_nonempty fun G' : G.Subgraph ↦ G'.coe.edgeDensity'
 
 end SimpleGraph

LeanCamCombi/Mathlib/Probability/Combinatorics/BinomialRandomGraph/Defs.lean

@@ -50,6 +50,7 @@ lemma measurable_adj : Measurable (Adj : SimpleGraph V → V → V → Prop) :=
 lemma measurable_edgeSet : Measurable (edgeSet : SimpleGraph V → Set (Sym2 V)) :=
   measurable_set_iff.2 <| by rintro ⟨u, v⟩; simp only [mem_edgeSet]; fun_prop
 
+set_option linter.flexible false in
 @[simp, fun_prop]
 lemma measurable_fromEdgeSet : Measurable (fromEdgeSet : Set (Sym2 V) → SimpleGraph V) := by
   simp [measurable_iff_adj]; fun_prop

LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

@@ -25,7 +25,7 @@ as probabilistic events, the size of the certificator `𝒜 □ ℬ` corresponds
 * D. Reimer, *Proof of the Van den Berg–Kesten Conjecture*
 -/
 
-open scoped Classical FinsetFamily
+open scoped FinsetFamily
 
 variable {α : Type*}
 
@@ -34,8 +34,8 @@ section BooleanAlgebra
 variable [BooleanAlgebra α] (s t u : Finset α) {a : α}
 
 noncomputable def certificator : Finset α :=
-  {a ∈ s ∩ t |
-    ∃ x y, IsCompl x y ∧ (∀ ⦃b⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b⦄, a ⊓ y = b ⊓ y → b ∈ t}
+  open scoped Classical in
+  {a ∈ s ∩ t | ∃ x y, IsCompl x y ∧ (∀ ⦃b⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b⦄, a ⊓ y = b ⊓ y → b ∈ t}
 
 scoped[FinsetFamily] infixl:70 " □ " => Finset.certificator
 
@@ -44,12 +44,15 @@ variable {s t u}
 @[simp] lemma mem_certificator :
     a ∈ s □ t ↔
       ∃ x y, IsCompl x y ∧ (∀ ⦃b⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b⦄, a ⊓ y = b ⊓ y → b ∈ t := by
+  classical
   rw [certificator, mem_filter, and_iff_right_of_imp]
   rintro ⟨u, v, _, hu, hv⟩
   exact mem_inter.2 ⟨hu rfl, hv rfl⟩
 
-lemma certificator_subset_inter : s □ t ⊆ s ∩ t := filter_subset _ _
+lemma certificator_subset_inter [DecidableEq α] : s □ t ⊆ s ∩ t := by
+  unfold certificator; convert filter_subset ..
 
+open scoped Classical in
 lemma certificator_subset_disjSups : s □ t ⊆ s ○ t := by
   simp_rw [subset_iff, mem_certificator, mem_disjSups]
   rintro x ⟨u, v, huv, hu, hv⟩
@@ -62,22 +65,23 @@ variable (s t u)
 lemma certificator_comm : s □ t = t □ s := by
   ext s; rw [mem_certificator, exists_comm]; simp [isCompl_comm, and_comm]
 
-lemma IsUpperSet.certificator_eq_inter (hs : IsUpperSet (s : Set α)) (ht : IsLowerSet (t : Set α)) :
-    s □ t = s ∩ t := by
+lemma IsUpperSet.certificator_eq_inter [DecidableEq α] (hs : IsUpperSet (s : Set α))
+    (ht : IsLowerSet (t : Set α)) : s □ t = s ∩ t := by
   refine
     certificator_subset_inter.antisymm fun a ha ↦ mem_certificator.2 ⟨a, aᶜ, isCompl_compl, ?_⟩
   rw [mem_inter] at ha
   simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
   exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
 
-lemma IsLowerSet.certificator_eq_inter (hs : IsLowerSet (s : Set α)) (ht : IsUpperSet (t : Set α)) :
-    s □ t = s ∩ t := by
+lemma IsLowerSet.certificator_eq_inter [DecidableEq α] (hs : IsLowerSet (s : Set α))
+    (ht : IsUpperSet (t : Set α)) : s □ t = s ∩ t := by
   refine certificator_subset_inter.antisymm fun a ha ↦
     mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, ?_⟩
   rw [mem_inter] at ha
   simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
   exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
 
+open scoped Classical in
 lemma IsUpperSet.certificator_eq_disjSups (hs : IsUpperSet (s : Set α))
     (ht : IsUpperSet (t : Set α)) : s □ t = s ○ t := by
   refine certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 ?_

LeanCamCombi/PlainCombi/VanDenBergKesten.lean

@@ -3,38 +3,15 @@ keywords = ["math", "combinatorics", "additive-combinatorics", "probabilitistic-
 defaultTargets = ["LeanCamCombi"]
 
 [leanOptions]
-autoImplicit = false        # Prevent typos to be interpreted as new free variables
+# Pretty-prints `fun a ↦ b`
+pp.unicode.fun = true
+# Don't assume a typo is a new variable
+autoImplicit = false
 relaxedAutoImplicit = false
-pp.unicode.fun = true       # Pretty-print lambdas as `fun a ↦ b`
-pp.proofs.withType = false  # Elide the types of proofs in terms
-weak.linter.docPrime = false
-weak.linter.hashCommand = true
-weak.linter.oldObtain = true
-weak.linter.refine = true
-weak.linter.style.cdot = true
-weak.linter.style.dollarSyntax = true
-weak.linter.style.header = true
-weak.linter.style.lambdaSyntax = true
-weak.linter.style.longLine = true
-weak.linter.style.longFile = 1500
-weak.linter.style.missingEnd = true
-weak.linter.style.multiGoal = true
-weak.linter.style.setOption = true
-
-[moreServerOptions]
-linter.docPrime = false
-linter.hashCommand = true
-linter.oldObtain = true
-weak.linter.refine = true
-linter.style.cdot = true
-linter.style.dollarSyntax = true
-linter.style.header = true
-linter.style.lambdaSyntax = true
-linter.style.longLine = true
-linter.style.longFile = 1500
-linter.style.missingEnd = true
-linter.style.multiGoal = true
-linter.style.setOption = true
+# Enable all mathlib linters: automatically matches what mathlib uses.
+weak.linter.mathlibStandardSet = true
+# Switch off warnings generated by `sorry`
+warn.sorry = false
 
 [[require]]
 name = "mathlib"