awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ (↑J' : WithBot (Box ι))
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
have this : ∀ (J : Box ι), (↑J : WithBot (Box ι)) ∈ boxes → ∃ J' ∈ π, J ≤ J'
Tactic: have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
    simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
have rcases : ∀ (J' : WithBot (Box ι)) (J'mem : J' ∈ boxes) (hle : (↑J : WithBot (Box ι)) ≤ J'),
  ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
Tactic: rcases H J hJ with ⟨J', J'mem, hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ (↑I : WithBot (Box ι))
pairwise_disjoint : (↑boxes : Set (WithBot (Box ι))).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, (↑J : WithBot (Box ι)) ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : (↑J : WithBot (Box ι)) ≤ J'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
have lift : ∀ (J' : Box ι) (J'mem : (↑J' : WithBot (Box ι)) ∈ boxes) (hle : (↑J : WithBot (Box ι)) ≤ (↑J' : WithBot (Box ι))),
  ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
Tactic: lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle
Cleared hypotheses: J', J'mem, hle
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
J' : WithBot (Box ι)
hJ' :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes) J'
⊢ J' ≤ (↑J : WithBot (Box ι))
have rcases : ∀ (J' : Box ι)
  (hJ' :
    Membership.mem (γ := Finset (WithBot (Box ι)))
      (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)))),
  (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
Tactic: rcases Finset.mem_image.1 hJ' with ⟨J', -, rfl⟩
Cleared hypotheses: J', hJ'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
⊢ (↑(Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes) :
        Set (WithBot (Box ι))).Pairwise
    Disjoint
have simp : ∀ ⦃x : WithBot (Box ι)⦄,
  (∃ a ∈ π.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = x) →
    ∀ ⦃y : WithBot (Box ι)⦄, (∃ a ∈ π.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = y) → x ≠ y → Disjoint x y
Tactic: simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J_1 J₁_1 J₂_1 : Box ι
π_1 π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ (↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι))
⊢ Disjoint ((↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι))) ((↑J : WithBot (Box ι)) ⊓ (↑J₂ : WithBot (Box ι)))
have this : J₁ ≠ J₂
Tactic: have : J₁ ≠ J₂ := by
        rintro rfl
        exact Hne rfl
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J
have refine : ∀ (J₁ : WithBot (Box ι))
  (hJ₁ :
    Membership.mem (γ := Finset (WithBot (Box ι)))
      (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
  (hne : J₁ ≠ ⊥),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      J₁ ≤ J'
Tactic: refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ :
  Membership.mem (γ := Finset (WithBot (Box ι)))
    (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁
hne : J₁ ≠ ⊥
⊢ ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      J₁ ≤ J'
have hJ₂ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁
Tactic: rw [Finset.mem_image] at hJ₁
Cleared hypotheses: hJ₁, hne
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁
hne : J₁ ≠ ⊥
⊢ ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      J₁ ≤ J'
have rcases : ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
Tactic: rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
Cleared hypotheses: J₁, hJ₁, hne
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥
⊢ ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
have rcases : ∀ (J₂ : Box ι) (hJ₂ : J₂ ∈ π₂) (hle : J₁ ≤ J₂),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
Tactic: rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J
have refine : ∀ (J₁ : WithBot (Box ι))
  (hJ₁ :
    Membership.mem (γ := Finset (WithBot (Box ι)))
      (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
  (hne : J₁ ≠ ⊥),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      J₁ ≤ J'
Tactic: classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
refine :
  ∀ (J₁ : WithBot (Box ι))
    (hJ₁ :
      Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
    (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
⊢ π₁.restrict J ≤ π₂.restrict J
have refine₁ : ∀ (J₁ : WithBot (Box ι)) (hJ₁ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁) (hne : J₁ ≠ ⊥),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      J₁ ≤ J'
Tactic: classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
refine :
  ∀ (J₁ : WithBot (Box ι))
    (hJ₁ :
      Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
    (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
refine₁ refine₂ :
  ∀ (J₁ : WithBot (Box ι)) (hJ₁ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁) (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
⊢ π₁.restrict J ≤ π₂.restrict J
have refine₃ : ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
Tactic: classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
refine :
  ∀ (J₁ : WithBot (Box ι))
    (hJ₁ :
      Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₁.boxes) J₁)
    (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
refine₁ refine₂ :
  ∀ (J₁ : WithBot (Box ι)) (hJ₁ : ∃ a ∈ π₁.boxes, (↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)) = J₁) (hne : J₁ ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        J₁ ≤ J'
refine₃ :
  ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥),
    ∃ (J' : WithBot (Box ι)),
      Membership.mem (γ := Finset (WithBot (Box ι)))
          (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
        (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
⊢ π₁.restrict J ≤ π₂.restrict J
have refine₄ : ∀ (J₁ : Box ι) (hJ₁ : J₁ ∈ π₁.boxes) (hne : (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≠ ⊥) (J₂ : Box ι)
  (hJ₂ : J₂ ∈ π₂) (hle : J₁ ≤ J₂),
  ∃ (J' : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι)))
        (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π₂.boxes) J' ∧
      (↑J : WithBot (Box ι)) ⊓ (↑J₁ : WithBot (Box ι)) ≤ J'
Tactic: classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.restrict J).boxes = π.boxes
have simp : Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
    Option.toFinset =
  π.boxes
Tactic: simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
have refine : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
Tactic: refine Finset.image_biUnion.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
have refine : ∀ a ∈ π.boxes, Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι))) = {a}
Tactic: refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) = {J'}
have rw : (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
Tactic: rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.restrict J).boxes = π.boxes
have simp : Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
    Option.toFinset =
  π.boxes
Tactic: classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
simp :
  Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
⊢ (π.restrict J).boxes = π.boxes
have simp₁ : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
Tactic: classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
simp :
  Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
simp₁ : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
⊢ (π.restrict J).boxes = π.boxes
have simp₂ : ∀ a ∈ π.boxes, Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι))) = {a}
Tactic: classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
simp :
  Finset.biUnion (Finset.image (fun (J' : Box ι) ↦ (↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) π.boxes)
      Option.toFinset =
    π.boxes
simp₁ : (π.boxes.biUnion fun (a : Box ι) ↦ Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑a : WithBot (Box ι)))) = π.boxes
simp₂ simp₃ :
  ∀ (J' : Box ι) (hJ' : J' ∈ π.boxes), Option.toFinset ((↑J : WithBot (Box ι)) ⊓ (↑J' : WithBot (Box ι))) = {J'}
⊢ (π.restrict J).boxes = π.boxes
have simp₄ : ∀ (J' : Box ι) (hJ' : J' ∈ π.boxes), (↑J' : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
Tactic: classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans 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).restrict J = πi J
have refine_1 : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ (πi J).boxes), J₁ ∈ ((π.biUnion πi).restrict J).boxes
Tactic: refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm
-- 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 ∈ π
refine_1 : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ (πi J).boxes), J₁ ∈ ((π.biUnion πi).restrict J).boxes
⊢ (π.biUnion πi).restrict J = πi J
have refine_2 : ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion
Tactic: refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm
-- 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 ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes
have refine_1 : (↑J₁ : WithBot (Box ι)) ≤ (↑J : WithBot (Box ι))
Tactic: refine (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right ?_).symm⟩
-- 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).restrict J).iUnion ⊆ (πi J).iUnion
have refine_2 : ∀ (x : ι → ℝ), (x ∈ (↑J : Set (ι → ℝ)) ∧ ∃ (i : Box ι) (_ : i ∈ π), x ∈ (πi i).iUnion) → x ∈ (πi J).iUnion
Tactic: simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J
have mp : π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict 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
π' : Prepartition I
mp : π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict J
⊢ π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J
have mpr : (∀ J ∈ π, πi J ≤ π'.restrict J) → π.biUnion πi ≤ π'
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
π' : Prepartition I
H : π.biUnion πi ≤ π'
J : Box ι
hJ : J ∈ π
⊢ πi J ≤ π'.restrict J
have mp : (π.biUnion πi).restrict J ≤ π'.restrict J
Tactic: rw [← π.restrict_biUnion πi hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ ∃ I' ∈ π', J ≤ I'
have hJ₁ : ∃ J' ∈ π, J ∈ πi J'
Tactic: rw [mem_biUnion] at hJ
Cleared hypotheses: 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
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : ∃ J' ∈ π, J ∈ πi J'
⊢ ∃ I' ∈ π', J ≤ I'
have mpr : ∀ (J₁ : Box ι) (h₁ : J₁ ∈ π) (hJ : J ∈ πi J₁), ∃ I' ∈ π', J ≤ I'
Tactic: rcases hJ with ⟨J₁, h₁, hJ⟩
Cleared hypotheses: 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
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
⊢ ∃ I' ∈ π', J ≤ I'
have mpr : ∀ (J₂ : Box ι) (h₂ : J₂ ∈ π'.restrict J₁) (Hle : J ≤ J₂), ∃ I' ∈ π', J ≤ I'
Tactic: rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
⊢ ∃ I' ∈ π', J ≤ I'
have mpr : ∀ (J₃ : Box ι) (h₃ : J₃ ∈ π') (H : (↑J₂ : WithBot (Box ι)) = (↑J₁ : WithBot (Box ι)) ⊓ (↑J₃ : WithBot (Box ι))),
  ∃ I' ∈ π', J ≤ I'
Tactic: rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J
have refine_1 : ∀ (H : π' ≤ π.biUnion πi) (J : Box ι) (hJ : J ∈ π), π'.restrict J ≤ πi J
Tactic: refine ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun 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
π' : Prepartition I
refine_1 : ∀ (H : π' ≤ π.biUnion πi) (J : Box ι) (hJ : J ∈ π), π'.restrict J ≤ πi J
⊢ π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J
have refine_2 : (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi
Tactic: refine ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun 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
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ πi J
have refine_1 : π'.restrict J ≤ (π.biUnion πi).restrict J
Tactic: rw [← π.restrict_biUnion πi 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
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π) (hle : J' ≤ J), ∃ I' ∈ π.biUnion πi, J' ≤ I'
Tactic: rcases H hJ' with ⟨J, hJ, hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'
have this : J' ∈ π'.restrict J
Tactic: have : J' ∈ π'.restrict J :=
      π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩