feat: port Analysis.BoxIntegral.Basic (#4695)

Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -432,6 +432,7 @@ import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
 import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 import Mathlib.Analysis.Asymptotics.Theta
+import Mathlib.Analysis.BoxIntegral.Basic
 import Mathlib.Analysis.BoxIntegral.Box.Basic
 import Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Additive

Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

@@ -61,25 +61,24 @@ open Box Prepartition Finset
 variable {N : Type _} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (Box ι)} {I J : Box ι}
   {i : ι}
 
-instance : CoeFun (ι →ᵇᵃ[I₀] M) fun _ => Box ι → M :=
-  ⟨toFun⟩
+instance : FunLike (ι →ᵇᵃ[I₀] M) (Box ι) (fun _ ↦ M) where
+  coe := toFun
+  coe_injective' f g h := by cases f; cases g; congr
 
 initialize_simps_projections BoxIntegral.BoxAdditiveMap (toFun → apply)
 
 #noalign box_integral.box_additive_map.to_fun_eq_coe
 
--- Porting note: Left-hand side has variable as head symbol @[simp]
+@[simp]
 theorem coe_mk (f h) : ⇑(mk f h : ι →ᵇᵃ[I₀] M) = f := rfl
 #align box_integral.box_additive_map.coe_mk BoxIntegral.BoxAdditiveMap.coe_mk
 
-theorem coe_injective : Injective fun (f : ι →ᵇᵃ[I₀] M) x => f x := by
-  rintro ⟨f, hf⟩ ⟨g, hg⟩ (rfl : f = g)
-  rfl
+theorem coe_injective : Injective fun (f : ι →ᵇᵃ[I₀] M) x => f x :=
+  FunLike.coe_injective
 #align box_integral.box_additive_map.coe_injective BoxIntegral.BoxAdditiveMap.coe_injective
 
-@[simp]
-theorem coe_inj {f g : ι →ᵇᵃ[I₀] M} : (f : Box ι → M) = g ↔ f = g :=
-  coe_injective.eq_iff
+-- porting note: was @[simp], now can be proved by `simp`
+theorem coe_inj {f g : ι →ᵇᵃ[I₀] M} : (f : Box ι → M) = g ↔ f = g := FunLike.coe_fn_eq
 #align box_integral.box_additive_map.coe_inj BoxIntegral.BoxAdditiveMap.coe_inj
 
 theorem sum_partition_boxes (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π : Prepartition I}

Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

@@ -56,7 +56,7 @@ variable {ι : Type _}
 structure Prepartition (I : Box ι) where
   boxes : Finset (Box ι)
   le_of_mem' : ∀ J ∈ boxes, J ≤ I
-  PairwiseDisjoint : Set.Pairwise (↑boxes) (Disjoint on ((↑) : Box ι → Set (ι → ℝ)))
+  pairwiseDisjoint : Set.Pairwise (↑boxes) (Disjoint on ((↑) : Box ι → Set (ι → ℝ)))
 #align box_integral.prepartition BoxIntegral.Prepartition
 
 namespace Prepartition
@@ -76,7 +76,7 @@ theorem mem_mk {s h₁ h₂} : J ∈ (mk s h₁ h₂ : Prepartition I) ↔ J ∈
 
 theorem disjoint_coe_of_mem (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (h : J₁ ≠ J₂) :
     Disjoint (J₁ : Set (ι → ℝ)) J₂ :=
-  π.PairwiseDisjoint h₁ h₂ h
+  π.pairwiseDisjoint h₁ h₂ h
 #align box_integral.prepartition.disjoint_coe_of_mem BoxIntegral.Prepartition.disjoint_coe_of_mem
 
 theorem eq_of_mem_of_mem (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (hx₁ : x ∈ J₁) (hx₂ : x ∈ J₂) : J₁ = J₂ :=
@@ -299,7 +299,7 @@ def biUnion (πi : ∀ J : Box ι, Prepartition J) : Prepartition I where
     simp only [Finset.mem_biUnion, exists_prop, mem_boxes] at hJ
     rcases hJ with ⟨J', hJ', hJ⟩
     exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')
-  PairwiseDisjoint := by
+  pairwiseDisjoint := by
     simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_biUnion]
     rintro J₁' ⟨J₁, hJ₁, hJ₁'⟩ J₂' ⟨J₂, hJ₂, hJ₂'⟩ Hne
     rw [Function.onFun, Set.disjoint_left]
@@ -409,7 +409,7 @@ def ofWithBot (boxes : Finset (WithBot (Box ι)))
   le_of_mem' J hJ := by
     rw [mem_eraseNone] at hJ
     simpa only [WithBot.some_eq_coe, WithBot.coe_le_coe] using le_of_mem _ hJ
-  PairwiseDisjoint J₁ h₁ J₂ h₂ hne := by
+  pairwiseDisjoint J₁ h₁ J₂ h₂ hne := by
     simp only [mem_coe, mem_eraseNone] at h₁ h₂
     exact Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))
 #align box_integral.prepartition.of_with_bot BoxIntegral.Prepartition.ofWithBot
@@ -594,7 +594,7 @@ instance : SemilatticeInf (Prepartition I) :=
 def filter (π : Prepartition I) (p : Box ι → Prop) : Prepartition I where
   boxes := π.boxes.filter p
   le_of_mem' _ hJ := π.le_of_mem (mem_filter.1 hJ).1
-  PairwiseDisjoint _ h₁ _ h₂ := π.disjoint_coe_of_mem (mem_filter.1 h₁).1 (mem_filter.1 h₂).1
+  pairwiseDisjoint _ h₁ _ h₂ := π.disjoint_coe_of_mem (mem_filter.1 h₁).1 (mem_filter.1 h₂).1
 #align box_integral.prepartition.filter BoxIntegral.Prepartition.filter
 
 @[simp]
@@ -624,7 +624,7 @@ theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) :
   convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes (↑) _).symm
   · simp (config := { contextual := true })
   · rw [Set.PairwiseDisjoint]
-    convert π.PairwiseDisjoint
+    convert π.pairwiseDisjoint
     rw [Set.union_eq_left_iff_subset, filter_boxes, coe_filter]
     exact fun _ ⟨h, _⟩ => h
 #align box_integral.prepartition.Union_filter_not BoxIntegral.Prepartition.iUnion_filter_not
@@ -640,9 +640,9 @@ theorem sum_fiberwise {α M} [AddCommMonoid M] (π : Prepartition I) (f : Box ι
 def disjUnion (π₁ π₂ : Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) : Prepartition I where
   boxes := π₁.boxes ∪ π₂.boxes
   le_of_mem' J hJ := (Finset.mem_union.1 hJ).elim π₁.le_of_mem π₂.le_of_mem
-  PairwiseDisjoint :=
+  pairwiseDisjoint :=
     suffices ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint (J₁ : Set (ι → ℝ)) J₂ by
-      simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), PairwiseDisjoint]
+      simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), pairwiseDisjoint]
     fun J₁ h₁ J₂ h₂ _ => h.mono (π₁.subset_iUnion h₁) (π₂.subset_iUnion h₂)
 #align box_integral.prepartition.disj_union BoxIntegral.Prepartition.disjUnion
 

Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

@@ -305,8 +305,8 @@ It is also automatically satisfied for any `c > 1`, see TODO section of the modu
 details. -/
 structure MemBaseSet (l : IntegrationParams) (I : Box ι) (c : ℝ≥0) (r : (ι → ℝ) → Ioi (0 : ℝ))
     (π : TaggedPrepartition I) : Prop where
-  protected IsSubordinate : π.IsSubordinate r
-  protected IsHenstock : l.bHenstock → π.IsHenstock
+  protected isSubordinate : π.IsSubordinate r
+  protected isHenstock : l.bHenstock → π.IsHenstock
   protected distortion_le : l.bDistortion → π.distortion ≤ c
   protected exists_compl : l.bDistortion → ∃ π' : Prepartition I,
     π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c

Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

@@ -88,7 +88,7 @@ end Box
 theorem Prepartition.measure_iUnion_toReal [Finite ι] {I : Box ι} (π : Prepartition I)
     (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] :
     (μ π.iUnion).toReal = ∑ J in π.boxes, (μ J).toReal := by
-  erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.PairwiseDisjoint]
+  erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.pairwiseDisjoint]
   exacts [fun J _ => J.measurableSet_coe, fun J _ => (J.measure_coe_lt_top μ).ne]
 #align box_integral.prepartition.measure_Union_to_real BoxIntegral.Prepartition.measure_iUnion_toReal
 

Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean

@@ -48,7 +48,7 @@ namespace Prepartition
 def splitCenter (I : Box ι) : Prepartition I where
   boxes := Finset.univ.map (Box.splitCenterBoxEmb I)
   le_of_mem' := by simp [I.splitCenterBox_le]
-  PairwiseDisjoint := by
+  pairwiseDisjoint := by
     rw [Finset.coe_map, Finset.coe_univ, image_univ]
     rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ Hne
     exact I.disjoint_splitCenterBox (mt (congr_arg _) Hne)