awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
⊢ (↑{I.splitLower i x, I.splitUpper i x} : Set (WithBot (Box ι))).Pairwise Disjoint
have simp : ∀ (b : WithBot (Box ι)), b = I.splitUpper i x → I.splitLower i x ≠ b → Disjoint (I.splitLower i x) b
Tactic: simp only [Finset.coe_insert, Finset.coe_singleton, true_and, Set.mem_singleton_iff,
        pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw : ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} sorry sorry).boxes, f J =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
rw :
  ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw₁ : ∑ J ∈ {I.splitLower i x, I.splitUpper i x}, Option.elim' 0 f J =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
rw :
  ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
rw₁ :
  ∑ J ∈ {I.splitLower i x, I.splitUpper i x}, Option.elim' 0 f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw₂ : Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw : ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} sorry sorry).boxes, f J =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: classical
  rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
rw :
  ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw₁ : ∑ J ∈ {I.splitLower i x, I.splitUpper i x}, Option.elim' 0 f J =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: classical
  rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
rw :
  ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
rw₁ :
  ∑ J ∈ {I.splitLower i x, I.splitUpper i x}, Option.elim' 0 f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
have rw₂ : Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) =
  Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Tactic: classical
  rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
⊢ split I i x = ⊤
have refine : ∀ (J : Box ι) (hJ : Membership.mem (γ := Finset (Box ι)) (boxes (I := I) ⊤) J), J ∈ (split I i x).boxes
Tactic: refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
J : Box ι
hJ : Membership.mem (γ := Finset (Box ι)) (boxes (I := I) ⊤) J
⊢ J ∈ (split I i x).boxes
have rcases : ∀ (h : x ∉ Ioo (J.lower i) (J.upper i)) (hJ : Membership.mem (γ := Finset (Box ι)) (boxes (I := J) ⊤) J),
  J ∈ (split J i x).boxes
Tactic: rcases mem_top.1 hJ with rfl
Cleared hypotheses: I, h, hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ J ∈ (split J i x).boxes
have rw : (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
Tactic: rw [mem_boxes, mem_split_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have h₁ : x ≤ J.lower i ∨ J.upper i ≤ x
Tactic: rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inl : x ≤ J.lower i → (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
inl : x ≤ J.lower i → (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inr : J.upper i ≤ x → (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inl : (↑J : WithBot (Box ι)) = J.splitUpper i x
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : J.upper i ≤ x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inr : (↑J : WithBot (Box ι)) = J.splitLower i x
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inl : x ≤ J.lower i → (↑J : WithBot (Box ι)) = J.splitUpper i x
Tactic: cases h <;> [right; left]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
inl : x ≤ J.lower i → (↑J : WithBot (Box ι)) = J.splitUpper i x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inr : J.upper i ≤ x → (↑J : WithBot (Box ι)) = J.splitLower i x
Tactic: cases h <;> [right; left]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i
⊢ (↑J : WithBot (Box ι)) = J.splitUpper i x
have inl : J.splitUpper i x = (↑J : WithBot (Box ι))
Tactic: rwa [eq_comm, Box.splitUpper_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : J.upper i ≤ x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x
have inr : J.splitLower i x = (↑J : WithBot (Box ι))
Tactic: rwa [eq_comm, Box.splitLower_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
have refine : ∀ (H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}), False
Tactic: refine (mem_split_iff'.1 h₁).resolve_right fun H => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ False
have h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: rw [← Box.mem_coe, H] at h₂
Cleared hypotheses: h₂, h₃, H
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have refine : ∀ (H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}), False
Tactic: refine (mem_split_iff'.1 h₁).resolve_left fun H => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ False
have h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
Tactic: rw [← Box.mem_coe, H] at h₂
Cleared hypotheses: h₂, h₃, H
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ (split J i x).restrict I = split I i x
have refine : ((split J i x).restrict I).boxes ⊆ (split I i x).boxes
Tactic: refine ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ((split J i x).restrict I).boxes ⊆ (split I i x).boxes
have simp : ∀ ⦃x_1 : Box ι⦄,
  (∃ (J' : Box ι),
      ((↑J' : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
          (↑J' : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}) ∧
        (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))) →
    (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
      (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: simp only [Finset.subset_iff, mem_boxes, mem_restrict', mem_split_iff']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ (J' : Box ι),
        ((↑J' : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
            (↑J' : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}) ∧
          (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J' : Set (ι → ℝ))) →
      (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
        (↑x_1 : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have this : ∀ (s : Set (ι → ℝ)), (↑I : Set (ι → ℝ)) ∩ s ⊆ (↑J : Set (ι → ℝ))
Tactic: have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => inter_subset_left.trans h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), (↑I : Set (ι → ℝ)) ∩ s ⊆ (↑J : Set (ι → ℝ))
J₁ J₂ : Box ι
H₁ : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))
H₂ : (↑J₂ : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
    (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have inl : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), (↑I : Set (ι → ℝ)) ∩ s ⊆ (↑J : Set (ι → ℝ))
J₁ J₂ : Box ι
H₁ : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))
H₂ : (↑J₂ : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
    (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
have inr : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2
have rw : ((insert p s).inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
Tactic: rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
rw : ((insert p s).inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2
have rw₁ : (split I p.1 p.2 ⊓ s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
Tactic: rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
rw : ((insert p s).inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
rw₁ : (split I p.1 p.2 ⊓ s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2
have rw₂ : (s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) ⊓ split I p.1 p.2 = splitMany I s ⊓ split I p.1 p.2
Tactic: rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
rw : ((insert p s).inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
rw₁ : (split I p.1 p.2 ⊓ s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2
rw₂ : (s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) ⊓ split I p.1 p.2 = splitMany I s ⊓ split I p.1 p.2
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2
have rw₃ : (s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) ⊓ split I p.1 p.2 =
  (s.inf fun (p : ι × ℝ) ↦ split I p.1 p.2) ⊓ split I p.1 p.2
Tactic: rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
h : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (insert p s)
have insert : π ⊓ (splitMany I s ⊓ split I p.1 p.2) = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
Tactic: simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
h : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
insert : π ⊓ (splitMany I s ⊓ split I p.1 p.2) = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
⊢ π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)
have insert₁ : π ⊓ splitMany I s ⊓ split I p.1 p.2 = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
Tactic: simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
h : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
insert : π ⊓ (splitMany I s ⊓ split I p.1 p.2) = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
insert₁ : π ⊓ splitMany I s ⊓ split I p.1 p.2 = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
⊢ π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)
have insert₂ : (π.biUnion fun (J : Box ι) ↦ splitMany J s) ⊓ split I p.1 p.2 =
  π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
Tactic: simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
h : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
insert : π ⊓ (splitMany I s ⊓ split I p.1 p.2) = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
insert₁ : π ⊓ splitMany I s ⊓ split I p.1 p.2 = π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
insert₂ :
  (π.biUnion fun (J : Box ι) ↦ splitMany J s) ⊓ split I p.1 p.2 =
    π.biUnion fun (J : Box ι) ↦ splitMany J s ⊓ split J p.1 p.2
⊢ π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)
have insert₃ : ((π.biUnion fun (J : Box ι) ↦ splitMany J s).biUnion fun (J : Box ι) ↦ split J p.1 p.2) =
  π.biUnion fun (J : Box ι) ↦ (splitMany J s).biUnion fun (J : Box ι) ↦ split J p.1 p.2
Tactic: simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
have empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
have insert : ∀ (p : ι × ℝ) (s : Finset (ι × ℝ)),
  p ∉ s →
    ∀ (ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s),
      π ⊓ splitMany I (insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (insert p s)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
have empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s
have insert : ∀ (p : ι × ℝ) (s : Finset (ι × ℝ)),
  p ∉ s →
    ∀ (ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s),
      π ⊓ splitMany I (insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (insert p s)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
⊢ Js ≤ J
have H₁ : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
Tactic: simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
⊢ Js ≤ J
have rcases : ∀ (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))) (hxs : x ∈ (↑Js : Set (ι → ℝ))), Js ≤ J
Tactic: rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
⊢ Js ≤ J
have refine_1 : ∀ (y : ι → ℝ) (hy : y ∈ Js) (i : ι), J.lower i < y i
Tactic: refine fun y hy i => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
refine_1 : ∀ (y : ι → ℝ) (hy : y ∈ Js) (i : ι), J.lower i < y i
⊢ Js ≤ J
have refine_2 : ∀ (y : ι → ℝ) (hy : y ∈ Js) (i : ι), y i ≤ J.upper i
Tactic: refine fun y hy i => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (goal)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ J.lower i < y i
have refine_1 : ∀ (Jl : Box ι) (Hmem : Jl ∈ split I i (J.lower i)) (Hle : Js ≤ Jl), J.lower i < y i
Tactic: rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.lower i)
Hle : Js ≤ Jl
⊢ J.lower i < y i
have this : x ∈ Jl
Tactic: have := Hle hxs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Split (hypothesis)
Goal:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint (↑J : WithBot (Box ι)) (↑Js : WithBot (Box ι))
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ (↑J : Set (ι → ℝ))
hxs : x ∈ (↑Js : Set (ι → ℝ))
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.lower i)
Hle : Js ≤ Jl
this : x ∈ Jl
⊢ J.lower i < y i
have Hle₁ : (↑Js : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | J.lower i < y i}
Tactic: rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle
Cleared hypotheses: Hle, this