awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
rw : (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x
⊢ J ∈ (split J i x).boxes

Tactic:
rw [mem_boxes, mem_split_iff]

Premises used: BoxIntegral.Prepartition.mem_split_iff, BoxIntegral.Prepartition.mem_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ x ≤ J.lower i ∨ J.upper i ≤ x

Tactic:
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h

Premises used: Set.mem_Ioo, not_lt, not_and_or
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
inr : J.upper i ≤ x → (↑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

Tactic:
cases h
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i
inl : (↑J : WithBot (Box ι)) = J.splitUpper i x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x

Tactic:
right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : J.upper i ≤ x
inr : (↑J : WithBot (Box ι)) = J.splitLower i x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x

Tactic:
left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
inr : J.upper i ≤ x → (↑J : WithBot (Box ι)) = J.splitLower i x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x ∨ (↑J : WithBot (Box ι)) = J.splitUpper i x

Tactic:
cases h <;> [right; left]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i
inl : J.splitUpper i x = (↑J : WithBot (Box ι))
inl₁ inl₂ inl₃ inl₄ : x ≤ J.lower i
⊢ (↑J : WithBot (Box ι)) = J.splitUpper i x

Tactic:
rwa [eq_comm, Box.splitUpper_eq_self]

Premises used: BoxIntegral.Box.splitUpper_eq_self, eq_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : J.upper i ≤ x
inr : J.splitLower i x = (↑J : WithBot (Box ι))
inr₁ inr₂ inr₃ inr₄ : J.upper i ≤ x
⊢ (↑J : WithBot (Box ι)) = J.splitLower i x

Tactic:
rwa [eq_comm, Box.splitLower_eq_self]

Premises used: eq_comm, BoxIntegral.Box.splitLower_eq_self
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}

Tactic:
(mem_split_iff'.1 h₁).resolve_right fun H => ?_

Premises used: BoxIntegral.Prepartition.mem_split_iff', Iff.mp, Or.resolve_right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
refine : ∀ (H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}), False
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
refine (mem_split_iff'.1 h₁).resolve_right fun H => ?_

Premises used: BoxIntegral.Prepartition.mem_split_iff', Iff.mp, Or.resolve_right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
⊢ y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ y i ≤ x

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h₅ : y i ≤ x
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h₃ : y i ≤ x
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ False

Tactic:
h₃.not_gt h₂.2

Premises used: And.right, LE.le.not_gt
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h₃ : y i ≤ x
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ False

Tactic:
exact h₃.not_gt h₂.2

Premises used: And.right, LE.le.not_gt
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}

Tactic:
(mem_split_iff'.1 h₁).resolve_left fun H => ?_

Premises used: BoxIntegral.Prepartition.mem_split_iff', Or.resolve_left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
refine : ∀ (H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}), False
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
refine (mem_split_iff'.1 h₁).resolve_left fun H => ?_

Premises used: BoxIntegral.Prepartition.mem_split_iff', Or.resolve_left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
⊢ y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ x < y i

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
h₄ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
h₅ : x < y i
⊢ (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
rw [← Box.mem_coe, H] at h₂

Premises used: BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
h₃ : x < y i
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ False

Tactic:
h₃.not_ge h₂.2

Premises used: And.right, LT.lt.not_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
h₃ : x < y i
H : (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ False

Tactic:
exact h₃.not_ge h₂.2

Premises used: And.right, LT.lt.not_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ (split J i x).restrict I = split I i x

Tactic:
((isPartitionSplit J i x).restrict h).eq_of_boxes_subset ?_

Premises used: BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset, BoxIntegral.Prepartition.IsPartition.restrict, BoxIntegral.Prepartition.isPartitionSplit
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
refine : ((split J i x).restrict I).boxes ⊆ (split I i x).boxes
⊢ (split J i x).restrict I = split I i x

Tactic:
refine ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset ?_

Premises used: BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset, BoxIntegral.Prepartition.IsPartition.restrict, BoxIntegral.Prepartition.isPartitionSplit
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
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}
⊢ ((split J i x).restrict I).boxes ⊆ (split I i x).boxes

Tactic:
simp only [Finset.subset_iff, mem_boxes, mem_restrict', mem_split_iff']

Premises used: BoxIntegral.Prepartition.mem_split_iff', BoxIntegral.Prepartition.mem_restrict', Finset.subset_iff, BoxIntegral.Prepartition.mem_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ (s : Set (ι → ℝ)), (↑I : Set (ι → ℝ)) ∩ s ⊆ (↑J : Set (ι → ℝ))

Tactic:
have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => inter_subset_left.trans h
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
inl : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
    (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}
inr : (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
    (↑J₁ : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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}

Tactic:
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]

Premises used: BoxIntegral.Box.toSet, Set.inter_left_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : ι → ℝ | x < y i}

Tactic:
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]

Premises used: BoxIntegral.Box.toSet, Set.inter_left_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
i : ι
x : ℝ
⊢ π ⊓ split I i x = π.biUnion fun (J : Box ι) ↦ split J i x

Tactic:
biUnion_congr_of_le rfl fun _ hJ => restrict_split hJ i x

Premises used: BoxIntegral.Prepartition.restrict_split, rfl, BoxIntegral.Prepartition.biUnion_congr_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
⊢ splitMany I ∅ = ⊤

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.inf, BoxIntegral.Prepartition.splitMany, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
rw₃ 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
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2

Tactic:
rw [splitMany, Finset.inf_insert, inf_comm, splitMany]

Premises used: Finset.inf_insert, inf_comm, BoxIntegral.Prepartition.splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
hp : p ∈ s
⊢ splitMany I s ≤ split I p.1 p.2

Tactic:
Finset.inf_le hp

Premises used: Set.Mem, setOf, Finset.inf_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I ∅).IsPartition

Tactic:
simp only [splitMany_empty, isPartitionTop]

Premises used: BoxIntegral.Prepartition.isPartitionTop, BoxIntegral.Prepartition.splitMany_empty
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s_1 : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
h : a ∉ s
hs : (splitMany I s).IsPartition
⊢ (splitMany I (insert a s)).IsPartition

Tactic:
simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

Premises used: BoxIntegral.Prepartition.inf_split, BoxIntegral.Prepartition.IsPartition.biUnion, BoxIntegral.Prepartition.splitMany_insert, BoxIntegral.Prepartition.isPartitionSplit
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I s).IsPartition

Tactic:
exact Finset.induction_on s (by simp only [splitMany_empty, isPartitionTop]) fun a s _ hs => by
    simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I s).IsPartition

Tactic:
classical
  exact Finset.induction_on s (by simp only [splitMany_empty, isPartitionTop]) fun a s _ hs => by
    simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I s).iUnion = (↑I : Set (ι → ℝ))

Tactic:
(isPartition_splitMany I s).iUnion_eq

Premises used: BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.Prepartition.isPartition_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
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
⊢ π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)

Tactic:
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]

Premises used: BoxIntegral.Prepartition.biUnion_assoc, BoxIntegral.Prepartition.inf_split, BoxIntegral.Prepartition.splitMany_insert, inf_assoc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
insert :
  ∀ (p : ι × ℝ) (s : Finset (ι × ℝ)),
    p ∉ s →
      ∀ (ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s),
        π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J 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]

Premises used: BoxIntegral.Prepartition.biUnion_assoc, Insert.insert, BoxIntegral.Prepartition.inf_split, BoxIntegral.Prepartition.splitMany_insert, inf_assoc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
empty : π ⊓ splitMany I ∅ = π.biUnion fun (J : Box ι) ↦ splitMany J ∅
insert :
  ∀ (p : ι × ℝ) (s : Finset (ι × ℝ)),
    p ∉ s →
      ∀ (ihp : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J s),
        π ⊓ splitMany I (Insert.insert p s) = π.biUnion fun (J : Box ι) ↦ splitMany J (Insert.insert p s)
⊢ π ⊓ splitMany I s = π.biUnion fun (J : Box ι) ↦ splitMany J 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]

Premises used: BoxIntegral.Prepartition.biUnion_assoc, Insert.insert, BoxIntegral.Prepartition.inf_split, BoxIntegral.Prepartition.splitMany_insert, inf_assoc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 ι))
⊢ ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s

Tactic:
simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H

Premises used: Finset.insert_subset_iff, Finset.singleton_subset_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
rcases : ∀ (x : ι → ℝ) (hx : x ∈ (↑J : Set (ι → ℝ))) (hxs : x ∈ (↑Js : Set (ι → ℝ))), Js ≤ J
⊢ Js ≤ J

Tactic:
rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩

Premises used: BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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

Tactic:
fun y hy i => ⟨?_, ?_⟩

Premises used: Set.Ioc, Set.Mem, setOf, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
refine_2 : ∀ (y : ι → ℝ) (hy : y ∈ Js) (i : ι), y i ≤ J.upper i
⊢ Js ≤ J

Tactic:
refine fun y hy i => ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : ι
refine_1 : ∀ (Jl : Box ι) (Hmem : Jl ∈ split I i (J.lower i)) (Hle : Js ≤ Jl), J.lower i < y i
⊢ 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⟩

Premises used: BoxIntegral.Prepartition.split, BoxIntegral.Box.lower, And.left, BoxIntegral.Prepartition.splitMany_le_split
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
⊢ x ∈ Jl

Tactic:
have := Hle hxs
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
⊢ (↑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

Premises used: And.left, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
Hle₁ : (↑Js : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | J.lower i < y i}
⊢ x ∈ Jl

Tactic:
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle

Premises used: And.left, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | J.lower i < y i}
this : x ∈ Jl
⊢ J.lower i < y i

Tactic:
(Hle hy).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | J.lower i < y i}
this : x ∈ Jl
⊢ J.lower i < y i

Tactic:
exact (Hle hy).2

Premises used: And.right