awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
inl : ∀ (hi₁ : J₁.lower i = x i), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have inr : ∀ (hi₁ : J₁.lower i < x i), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
Tactic: rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have hi₂ : J₂.lower i = x i
Tactic: have hi₂ : J₂.lower i = x i := (H _).1 hi₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have H₁ : x i < J₁.upper i
Tactic: have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have H₂ : x i < J₂.upper i
Tactic: have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have inl : x i < min (J₁.upper i) (J₂.upper i)
Tactic: rw [Set.Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i < x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have hi₂ : J₂.lower i < x i
Tactic: have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card ι)
have rw : #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
  Fintype.card.{u_1} (Set ι)
Tactic: rw [← Fintype.card_set]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
inst : Fintype ι
x : ι → ℝ
⊢ #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) ≤
    Fintype.card.{u_1} (Set ι)
have refine : InjOn (β := Set ι) (fun (J : Box ι) ↦ {i : ι | J.lower i = x i})
  (↑({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x}) :
    Set (Box ι))
Tactic: refine Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
    (fun _ _ => Finset.mem_univ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
have h : ∀ (x_1 : Box ι), x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ (↑x_1 : Set (ι → ℝ))
Tactic: convert! Set.mem_iUnion₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x_1 : Box ι
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ (↑x_1 : Set (ι → ℝ))
have h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ x_1
Tactic: rw [Box.mem_coe, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x_1 : Box ι
h : x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ x_1
⊢ x_1 ∈ π ∧ x ∈ x_1 ↔ ∃ (_ : x_1 ∈ π), x ∈ (↑x_1 : Set (ι → ℝ))
have h₁ : x_1 ∈ π ∧ x ∈ x_1 ↔ x_1 ∈ π ∧ x ∈ x_1
Tactic: rw [Box.mem_coe, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
have mp : π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
mp :
  π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
⊢ π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
have mpr : (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion → π₁ ≤ π₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
have mp : ∀ (H : π₁ ≤ π₂) (J : Box ι) (hJ : J ∈ π₁) (J' : Box ι) (hJ' : J' ∈ π₂)
  (Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty), J ≤ J'
Tactic: refine fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty
⊢ J ≤ J'
have mp : ∀ (J'' : Box ι) (hJ'' : J'' ∈ π₂) (Hle : J ≤ J''), J ≤ J'
Tactic: rcases H hJ with ⟨J'', hJ'', Hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
⊢ J ≤ J'
have mp : ∀ (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))) (hx' : x ∈ (↑J' : Set (ι → ℝ))), J ≤ J'
Tactic: rcases Hne with ⟨x, hx, hx'⟩
Cleared hypotheses: Hne
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
HU : π₁.iUnion ⊆ π₂.iUnion
J : Box ι
hJ : J ∈ π₁
⊢ ∃ I' ∈ π₂, J ≤ I'
have HU₁ : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
Tactic: simp only [Set.subset_def, mem_iUnion] at HU
Cleared hypotheses: HU
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : ∀ J ∈ π₁, ∀ J' ∈ π₂, ((↑J : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))).Nonempty → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J ∈ π₁, x ∈ J) → ∃ J ∈ π₂, x ∈ J
⊢ ∃ I' ∈ π₂, J ≤ I'
have mpr : ∀ (J₂ : Box ι) (hJ₂ : J₂ ∈ π₂) (hx : J.upper ∈ J₂), ∃ I' ∈ π₂, J ≤ I'
Tactic: rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : Membership.mem (γ := Finset (Box ι)) (π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes) J
⊢ J ≤ I
have hJ₁ : ∃ a ∈ π, J ∈ πi a
Tactic: simp only [Finset.mem_biUnion, mem_boxes] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ∃ a ∈ π, J ∈ πi a
⊢ J ≤ I
have rcases : ∀ (J' : Box ι) (hJ' : J' ∈ π) (hJ : J ∈ πi J'), J ≤ I
Tactic: rcases hJ with ⟨J', hJ', hJ⟩
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
⊢ (↑(π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes) : Set (Box ι)).Pairwise (Disjoint on Box.toSet)
have simp : ∀ ⦃x : Box ι⦄,
  (∃ a ∈ π.boxes, x ∈ (πi a).boxes) →
    ∀ ⦃y : Box ι⦄, (∃ a ∈ π.boxes, y ∈ (πi a).boxes) → x ≠ y → (Disjoint on Box.toSet) x y
Tactic: simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_biUnion]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
⊢ (Disjoint on Box.toSet) J₁' J₂'
have rw : ∀ ⦃a : ι → ℝ⦄, a ∈ (↑J₁' : Set (ι → ℝ)) → a ∉ (↑J₂' : Set (ι → ℝ))
Tactic: rw [Function.onFun, Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
⊢ False
have apply : J₁' = J₂'
Tactic: apply Hne
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x_1 : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ (↑J₁' : Set (ι → ℝ))
hx₂ : x ∈ (↑J₂' : Set (ι → ℝ))
hJ₃ : J₁ ∈ π.boxes
⊢ J₁' = J₂'
have hJ₂'₁ : J₂' ∈ (πi J₁).boxes
Tactic: obtain rfl : J₁ = J₂ :=
      π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)
Cleared hypotheses: J₂, hJ₂, hJ₂'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (π.biUnion fun (x : Box ι) ↦ ⊤) = π
have h : ∀ (J : Box ι), (J ∈ π.biUnion fun (x : Box ι) ↦ ⊤) ↔ J ∈ π
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₂.biUnion πi₂
have subst : π₁.biUnion πi₁ = π₁.biUnion πi₂
Tactic: subst π₂
Cleared hypotheses: π₂, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
⊢ π₁.biUnion πi₁ = π₁.biUnion πi₂
have h : ∀ (J : Box ι), J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂
Tactic: ext J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂
have h : (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'
Tactic: simp only [mem_biUnion]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'
have h : (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
h : (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'
have h₁ : (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
M : Type u_2
inst : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π.boxes.biUnion fun (J : Box ι) ↦ (πi J).boxes, f J)
    (∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J')
have refine : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ (↑π.boxes : Set (Box ι))) (J₂ : Box ι) (h₂ : J₂ ∈ (↑π.boxes : Set (Box ι))) (hne : J₁ ≠ J₂)
  (J' : Box ι) (h₁' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₁) J')
  (h₂' : Membership.mem (γ := Finset (Box ι)) ((fun (J : Box ι) ↦ (πi J).boxes) J₂) J'), False
Tactic: refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ∈ π
have rw : sorry.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') ∈ π
Tactic: rw [biUnionIndex, dif_pos hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
⊢ π.biUnionIndex πi J ≤ I
have pos : ∀ (hJ : J ∈ π.biUnion πi), π.biUnionIndex πi J ≤ I
Tactic: by_cases hJ : J ∈ π.biUnion πi
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
pos : ∀ (hJ : J ∈ π.biUnion πi), π.biUnionIndex πi J ≤ I
⊢ π.biUnionIndex πi J ≤ I
have neg : ∀ (hJ : J ∉ π.biUnion πi), π.biUnionIndex πi J ≤ I
Tactic: by_cases hJ : J ∈ π.biUnion πi
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I
have neg : (if hJ : J ∈ π.biUnion πi then sorry.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') else I) ≤ I
Tactic: rw [biUnionIndex, dif_neg hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
neg : (if hJ : J ∈ π.biUnion πi then ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J') else I) ≤ I
⊢ π.biUnionIndex πi J ≤ I
have neg₁ : I ≤ I
Tactic: rw [biUnionIndex, dif_neg hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ Membership.mem (γ := Prepartition (π.biUnionIndex πi J)) (πi (π.biUnionIndex πi J)) J
have h : π.biUnionIndex πi J = sorry.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')
Tactic: convert! (π.mem_biUnion.1 hJ).choose_spec.2
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
h : π.biUnionIndex πi J = ⋯.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')
⊢ Membership.mem (γ := Prepartition (π.biUnionIndex πi J)) (πi (π.biUnionIndex πi J)) J
have h₁ : Prepartition (π.biUnionIndex πi J) = Prepartition (sorry.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')) →
  π.biUnionIndex πi J = sorry.choose (p := fun (J' : Box ι) ↦ J' ∈ π ∧ J ∈ πi J')
Tactic: convert! (π.mem_biUnion.1 hJ).choose_spec.2
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
⊢ (π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) =
    (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J
have h : ∀ (J : Box ι),
  (J ∈ π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) ↔
    J ∈ (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J
Tactic: ext J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (J ∈ π.biUnion fun (J : Box ι) ↦ (πi J).biUnion (πi' J)) ↔
    J ∈ (π.biUnion πi).biUnion fun (J : Box ι) ↦ πi' (π.biUnionIndex πi J) J
have h : (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔
  ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
Tactic: simp only [mem_biUnion]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
have h : (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) →
  ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
h :
  (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) →
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
⊢ (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔
    ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
have h₁ : (∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J') →
  ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ ∃ (J' : Box ι), (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'
have h : J ∈ πi' (π.biUnionIndex πi J₂) J₂
Tactic: refine ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1
have h : J ∈ πi' J₂ J₁
Tactic: refine ⟨J₂, hJ₂, J₁, hJ₁, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ J ∈ πi' J₂ J₁
have h : ∀ (hJ : J ∈ πi' J₂ J₁) (hJ₂ : J₂ ∈ π) (hJ₁ : J₁ ∈ πi J₂), J ∈ πi' J₂ J₁
Tactic: rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ
Cleared hypotheses: hJ, hJ₂, hJ₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J : Box ι
hJ :
  Membership.mem (γ := Finset (Box ι))
    ((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) J
⊢ J ≤ I
have hJ₁ : some J ∈ boxes
Tactic: rw [mem_eraseNone] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ : Box ι
h₁ : J₁ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
hne : J₁ ≠ J₂
⊢ (Disjoint on Box.toSet) J₁ J₂
have h₃ : some J₁ ∈ boxes
Tactic: simp only [mem_coe, mem_eraseNone] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J J₁_1 J₂_1 : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
J₁ : Box ι
h₁ : J₁ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
J₂ : Box ι
h₂ : J₂ ∈ (↑((eraseNone : (a : Finset (Option (Box ι))) → Finset (Box ι)) boxes : Finset (Box ι)) : Set (Box ι))
hne : J₁ ≠ J₂
h₃ : some J₁ ∈ boxes
⊢ (Disjoint on Box.toSet) J₁ J₂
have h₄ : some J₂ ∈ boxes
Tactic: simp only [mem_coe, mem_eraseNone] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, (↑J : Set (ι → ℝ))
have suffices : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) ∈ boxes), (↑J : Set (ι → ℝ)))
  (⋃ J ∈ boxes, (↑J : Set (ι → ℝ)))
Tactic: suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by
    simpa [ofWithBot, Prepartition.iUnion]