awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : I.distortion ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition
have rw : ∀ (hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c) (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
  ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition
Tactic: rw [← Prepartition.distortion_top] at hc
Cleared hypotheses: hc, r
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition
have hc' : Prepartition.distortion.{u_1} (ι := ι) (I := I) (Prepartition.compl ⊤) ≤ c
Tactic: have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
⊢ MeasurableSet (↑I : Set (ι → ℝ))
have rw : MeasurableSet.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))
Tactic: rw [coe_eq_pi]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
⊢ (↑I : Set (ι → ℝ)) =ᶠ[ae (F := Measure (ι → ℝ)) volume] (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
have rw : (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =ᶠ[ae (F := Measure (ι → ℝ)) volume]
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
Tactic: rw [coe_eq_pi]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) π.iUnion) =
    ∑ x ∈ π.boxes, ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑x : Set (ι → ℝ)))
have rw : ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π, (↑J : Set (ι → ℝ)))) =
  ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
Tactic: rw [← ENNReal.toReal_sum (fun J _ => (J.measure_coe_lt_top μ).ne), π.iUnion_def]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
have simp : ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π.boxes, (↑J : Set (ι → ℝ)))) =
  ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
Tactic: simp only [← mem_boxes]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π.boxes, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
have rw : ∀ b ∈ π.boxes, MeasurableSet (↑b : Set (ι → ℝ))
Tactic: rw [measure_biUnion_finset π.pairwiseDisjoint]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Finite ι
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
J : Box ι
h : (↑J : WithTop (Box ι)) ≤ ⊤
π : Prepartition J
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, μ.real (↑Ji : Set (ι → ℝ)) = μ.real (↑J : Set (ι → ℝ))
have rw : μ.real π.iUnion = μ.real (↑J : Set (ι → ℝ))
Tactic: rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Finite ι
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
J : Box ι
h : (↑J : WithTop (Box ι)) ≤ ⊤
π : Prepartition J
hπ : π.IsPartition
rw : μ.real π.iUnion = μ.real (↑J : Set (ι → ℝ))
⊢ ∑ Ji ∈ π.boxes, μ.real (↑Ji : Set (ι → ℝ)) = μ.real (↑J : Set (ι → ℝ))
have rw₁ : μ.real (↑J : Set (ι → ℝ)) = μ.real (↑J : Set (ι → ℝ))
Tactic: rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
⊢ Eq (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) (∏ i : ι, (I.upper i - I.lower i) : ℝ)
have rw : Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑I : Set (ι → ℝ)) =
  ∏ i : ι, (I.upper i - I.lower i)
Tactic: rw [Measure.toBoxAdditive_apply, coe_eq_pi, measureReal_def,
    Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑I : Set (ι → ℝ)) =
    ∏ i : ι, (I.upper i - I.lower i)
⊢ Eq (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) (∏ i : ι, (I.upper i - I.lower i) : ℝ)
have rw₁ : Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
    (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =
  ∏ i : ι, (I.upper i - I.lower i)
Tactic: rw [Measure.toBoxAdditive_apply, coe_eq_pi, measureReal_def,
    Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑I : Set (ι → ℝ)) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₁ :
  Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
      (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =
    ∏ i : ι, (I.upper i - I.lower i)
⊢ Eq (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) (∏ i : ι, (I.upper i - I.lower i) : ℝ)
have rw₂ : ENNReal.toReal
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
  ∏ i : ι, (I.upper i - I.lower i)
Tactic: rw [Measure.toBoxAdditive_apply, coe_eq_pi, measureReal_def,
    Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑I : Set (ι → ℝ)) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₁ :
  Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
      (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₂ :
  ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
    ∏ i : ι, (I.upper i - I.lower i)
⊢ Eq (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) (∏ i : ι, (I.upper i - I.lower i) : ℝ)
have rw₃ : Eq (α := ℝ) (∏ i : ι, (I.upper i - I.lower i)) (∏ i : ι, (I.upper i - I.lower i))
Tactic: rw [Measure.toBoxAdditive_apply, coe_eq_pi, measureReal_def,
    Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ))) =
    ∏ i : ι, (I.upper i - I.lower i)
have rw : ENNReal.toReal
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
  ∏ i : ι, (I.upper i - I.lower i)
Tactic: rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
    ∏ i : ι, (I.upper i - I.lower i)
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ))) =
    ∏ i : ι, (I.upper i - I.lower i)
have rw₁ : Eq (α := ℝ) (∏ i : ι, (I.upper i - I.lower i)) (∏ i : ι, (I.upper i - I.lower i))
Tactic: rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Measure (goal)
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
I : Box ι
x : E
⊢ (((BoxAdditiveMap.volume : (a : Box ι) → E →L[ℝ] E) I : E →L[ℝ] E) : (a : E) → E) x =
    HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x
have rw : HSMul.hSMul (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) x =
  HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x
Tactic: rw [BoxAdditiveMap.volume, toSMul_apply]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (↑(I.splitLower i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
have rw : (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
    Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1)) =
  (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
Tactic: rw [splitLower, coe_mk']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
have h : ∀ (y : (i : ι) → ℝ),
  Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
⊢ Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
have h : (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
Tactic: simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def,
    le_update_iff, le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
have h : (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
Tactic: rw [and_comm (a := y i ≤ x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i
have rw : (min x (I.upper i) ≤ I.lower i ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
Tactic: rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i
have rw : mk' I.lower (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i))) = ⊥ ↔ x ≤ I.lower i
Tactic: classical
  rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' I.lower (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i))) = ⊥ ↔ x ≤ I.lower i
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i
have rw₁ : (∃ (i_1 : ι), update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1 ≤ I.lower i_1) ↔ x ≤ I.lower i
Tactic: classical
  rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' I.lower (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i))) = ⊥ ↔ x ≤ I.lower i
rw₁ : (∃ (i_1 : ι), update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1 ≤ I.lower i_1) ↔ x ≤ I.lower i
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i
have rw₂ : (min x (I.upper i) ≤ I.lower i ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
Tactic: classical
  rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have rw : (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
    Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
  (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: rw [splitUpper, coe_mk']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have h : ∀ (y : (i : ι) → ℝ),
  Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
⊢ Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have h : (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
  ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
Tactic: simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have rw : (↑(mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper) : Set (ι → ℝ)) =
  (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: classical
  rw [splitUpper, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
  exact and_comm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (↑(mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper) : Set (ι → ℝ)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have rw₁ : (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
    Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
  (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: classical
  rw [splitUpper, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
  exact and_comm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (↑(mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper) : Set (ι → ℝ)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
rw₁ rw₂ rw₃ :
  (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have h : ∀ (y : (i : ι) → ℝ),
  Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: classical
  rw [splitUpper, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
  exact and_comm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (↑(mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper) : Set (ι → ℝ)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
rw₁ rw₂ rw₃ :
  (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h :
  ∀ (y : (i : ι) → ℝ),
    Membership.mem (γ := Set ((i : ι) → ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
          Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
        y ↔
      y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have h₁ : ∀ (y : (i : ι) → ℝ),
  (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
Tactic: classical
  rw [splitUpper, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
  exact and_comm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
have rw : (I.upper i ≤ max x (I.lower i) ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
Tactic: rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
have rw : mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper = ⊥ ↔ I.upper i ≤ x
Tactic: classical
  rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper = ⊥ ↔ I.upper i ≤ x
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
have rw₁ : (∃ (i_1 : ι), I.upper i_1 ≤ update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) ↔ I.upper i ≤ x
Tactic: classical
  rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper = ⊥ ↔ I.upper i ≤ x
rw₁ : (∃ (i_1 : ι), I.upper i_1 ≤ update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) ↔ I.upper i ≤ x
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
have rw₂ : (I.upper i ≤ max x (I.lower i) ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
Tactic: classical
  rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
  simp [(I.lower_lt_upper _).not_ge]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)
have rw : Disjoint ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}) ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i})
Tactic: rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}) ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i})
have refine : Disjoint.{u_1} (α := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} {y : ι → ℝ | x < y i}
Tactic: refine (Disjoint.inf_left' _ ?_).inf_right' _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint.{u_1} (α := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} {y : ι → ℝ | x < y i}
have rw : ∀ ⦃a : ι → ℝ⦄, Membership.mem (γ := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} a → a ∉ {y : ι → ℝ | x < y i}
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x ≠ I.splitUpper i x
have inl : ∀ (h : x ≤ I.lower i), I.splitLower i x ≠ I.splitUpper i x
Tactic: rcases le_or_gt x (I.lower i) with h | _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
inl : ∀ (h : x ≤ I.lower i), I.splitLower i x ≠ I.splitUpper i x
⊢ I.splitLower i x ≠ I.splitUpper i x
have inr : I.lower i < x → I.splitLower i x ≠ I.splitUpper i x
Tactic: rcases le_or_gt x (I.lower i) with h | _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ I.splitLower i x ≠ I.splitUpper i x
have inl : ⊥ ≠ (↑I : WithBot (Box ι))
Tactic: rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
⊢ I.splitLower i x ≠ I.splitUpper i x
have inr : I.splitLower i x ≠ ⊥
Tactic: refine (disjoint_splitLower_splitUpper I i x).ne ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
⊢ I.splitLower i x ≠ ⊥
have inr : ¬I.splitLower i x = ⊥
Tactic: rwa [Ne, splitLower_eq_bot, not_le]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
inr : ¬I.splitLower i x = ⊥
⊢ I.splitLower i x ≠ ⊥
have inr₁ : ¬x ≤ I.lower i
Tactic: rwa [Ne, splitLower_eq_bot, not_le]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι))) {I.splitLower i x, I.splitUpper i x} J → J ≤ (↑I : WithBot (Box ι))
have simp : ∀ (J : WithBot (Box ι)), J = I.splitLower i x ∨ J = I.splitUpper i x → J ≤ (↑I : WithBot (Box ι))
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton]