awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
I : Box ι
x : E
rw :
  HSMul.hSMul (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) x =
    HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x
⊢ (((BoxAdditiveMap.volume : (a : Box ι) → E →L[ℝ] E) I : E →L[ℝ] E) : (a : E) → E) x =
    HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x

Tactic:
rw [BoxAdditiveMap.volume, toSMul_apply]

Premises used: BoxIntegral.BoxAdditiveMap.toSMul_apply, BoxIntegral.BoxAdditiveMap.volume
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
I : Box ι
x : E
⊢ HSMul.hSMul (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) x =
    HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x

Tactic:
congr_arg₂ (· • ·) I.volume_apply rfl

Premises used: BoxIntegral.Box.volume_apply, HSMul.hSMul, rfl, congr_arg₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
I : Box ι
x : E
⊢ HSMul.hSMul (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) x =
    HSMul.hSMul (α := ℝ) (∏ j : ι, (I.upper j - I.lower j)) x

Tactic:
exact congr_arg₂ (· • ·) I.volume_apply rfl

Premises used: BoxIntegral.Box.volume_apply, HSMul.hSMul, rfl, congr_arg₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ (↑(I.splitLower i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
rw [splitLower, coe_mk']

Premises used: BoxIntegral.Box.coe_mk', BoxIntegral.Box.splitLower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h :
  ∀ (y : (i : ι) → ℝ),
    Membership.mem (γ := Set ((i : ι) → ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
          Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1))
        y ↔
      y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}
⊢ (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
ext y
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
h : (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
⊢ Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (I.lower i_1) (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}

Tactic:
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def,
    le_update_iff, le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]

Premises used: and_forall_ne, Set.mem_inter_iff, Set.mem_setOf_eq, BoxIntegral.Box.mem_coe, le_update_iff, BoxIntegral.Box.mem_def, and_assoc, Set.mem_Ioc, Pi.le_def, Set.mem_univ_pi, le_min_iff, forall_and
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
h h₁ : (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
⊢ (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x

Tactic:
rw [and_comm (a := y i ≤ x)]

Premises used: and_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (↑(I.splitLower i x) : Set (ι → ℝ)) ⊆ (↑(↑I : WithBot (Box ι)) : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : (min x (I.upper i) ≤ I.lower i ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Tactic:
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]

Premises used: BoxIntegral.Box.upper, LE.le, BoxIntegral.Box.mk'_eq_bot, BoxIntegral.Box.lower, BoxIntegral.Box.splitLower, Function.exists_update_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (min x (I.upper i) ≤ I.lower i ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i

Tactic:
simp [(I.lower_lt_upper _).not_ge]

Premises used: BoxIntegral.Box.lower_lt_upper, LT.lt.not_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' I.lower (update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i))) = ⊥ ↔ x ≤ I.lower i
rw₁ : (∃ (i_1 : ι), update (β := fun (a : ι) ↦ ℝ) I.upper i (min x (I.upper i)) i_1 ≤ I.lower i_1) ↔ x ≤ I.lower i
rw₂ rw₃ rw₄ : (min x (I.upper i) ≤ I.lower i ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Tactic:
classical
  rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
  simp [(I.lower_lt_upper _).not_ge]

Premises used: BoxIntegral.Box.mk'_eq_bot, BoxIntegral.Box.lower_lt_upper, LT.lt.not_ge, BoxIntegral.Box.splitLower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = (↑I : WithBot (Box ι)) ↔ I.upper i ≤ x

Tactic:
simp [splitLower]

Premises used: BoxIntegral.Box.splitLower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (I.lower i) (I.upper i)
h' : ∀ (j : ι), I.lower j < update (β := fun (a : ι) ↦ ℝ) I.upper i x j
⊢ I.splitLower i x =
    (↑{ lower := I.lower, upper := update (β := fun (a : ι) ↦ ℝ) I.upper i x, lower_lt_upper := h' } : WithBot (Box ι))

Tactic:
simp +unfoldPartialApp only [splitLower, mk'_eq_coe, min_eq_left h.2.le,
    update, and_self]

Premises used: Function.update, and_self, LT.lt.le, BoxIntegral.Box.mk'_eq_coe, min_eq_left, And.right, BoxIntegral.Box.splitLower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
rw [splitUpper, coe_mk']

Premises used: BoxIntegral.Box.coe_mk', BoxIntegral.Box.splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h :
  ∀ (y : (i : ι) → ℝ),
    Membership.mem (γ := Set ((i : ι) → ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
          Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
        y ↔
      y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
⊢ (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
ext y
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
h :
  (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
⊢ Membership.mem (γ := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
        Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
      y ↔
    y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]

Premises used: and_forall_ne, Set.mem_inter_iff, max_lt_iff, Set.mem_setOf_eq, BoxIntegral.Box.mem_coe, BoxIntegral.Box.lower, Function.forall_update_iff, BoxIntegral.Box.mem_def, LT.lt, and_assoc, Set.mem_Ioc, Set.mem_univ_pi, forall_and
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
⊢ (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i

Tactic:
and_comm

Premises used: and_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : (i : ι) → ℝ
⊢ (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i

Tactic:
exact and_comm

Premises used: and_comm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw :
  (↑(mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper) : Set (ι → ℝ)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
rw₁ rw₂ rw₃ :
  (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
      Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) =
    (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h :
  ∀ (y : (i : ι) → ℝ),
    Membership.mem (γ := Set ((i : ι) → ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i_1 : ι) ↦
          Ioc (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) (I.upper i_1))
        y ↔
      y ∈ (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}
h₁ :
  ∀ (y : (i : ι) → ℝ),
    (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
      ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
classical
  rw [splitUpper, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
    forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
    and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
  exact and_comm

Premises used: Set.mem_inter_iff, max_lt_iff, Set.mem_setOf_eq, BoxIntegral.Box.mem_coe, and_comm, BoxIntegral.Box.coe_mk', BoxIntegral.Box.mem_def, Set.mem_Ioc, Set.mem_univ_pi, BoxIntegral.Box.splitUpper, forall_and
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (↑(I.splitUpper i x) : Set (ι → ℝ)) ⊆ (↑(↑I : WithBot (Box ι)) : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : (I.upper i ≤ max x (I.lower i) ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Tactic:
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]

Premises used: BoxIntegral.Box.upper, LE.le, BoxIntegral.Box.mk'_eq_bot, BoxIntegral.Box.lower, BoxIntegral.Box.splitUpper, Function.exists_update_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ max x (I.lower i) ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x

Tactic:
simp [(I.lower_lt_upper _).not_ge]

Premises used: BoxIntegral.Box.lower_lt_upper, LT.lt.not_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : mk' (update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i))) I.upper = ⊥ ↔ I.upper i ≤ x
rw₁ : (∃ (i_1 : ι), I.upper i_1 ≤ update (β := fun (a : ι) ↦ ℝ) I.lower i (max x (I.lower i)) i_1) ↔ I.upper i ≤ x
rw₂ rw₃ rw₄ : (I.upper i ≤ max x (I.lower i) ∨ ∃ (x : ι), x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Tactic:
classical
  rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
  simp [(I.lower_lt_upper _).not_ge]

Premises used: BoxIntegral.Box.mk'_eq_bot, BoxIntegral.Box.lower_lt_upper, LT.lt.not_ge, BoxIntegral.Box.splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = (↑I : WithBot (Box ι)) ↔ x ≤ I.lower i

Tactic:
simp [splitUpper]

Premises used: BoxIntegral.Box.splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
inst : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (I.lower i) (I.upper i)
h' : ∀ (j : ι), update (β := fun (a : ι) ↦ ℝ) I.lower i x j < I.upper j
⊢ I.splitUpper i x =
    (↑{ lower := update (β := fun (a : ι) ↦ ℝ) I.lower i x, upper := I.upper, lower_lt_upper := h' } : WithBot (Box ι))

Tactic:
simp +unfoldPartialApp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le,
    update, and_self]

Premises used: Function.update, and_self, LT.lt.le, max_eq_left, BoxIntegral.Box.mk'_eq_coe, And.left, BoxIntegral.Box.splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : Disjoint ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}) ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i})
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]

Premises used: BoxIntegral.Box.disjoint_withBotCoe, BoxIntegral.Box.coe_splitLower, BoxIntegral.Box.coe_splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}) ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i})

Tactic:
(Disjoint.inf_left' _ ?_).inf_right' _

Premises used: Disjoint.inf_right', Disjoint.inf_left'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
refine : Disjoint.{u_1} (α := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} {y : ι → ℝ | x < y i}
⊢ Disjoint ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x}) ((↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i})

Tactic:
refine (Disjoint.inf_left' _ ?_).inf_right' _

Premises used: Disjoint.inf_right', Disjoint.inf_left'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
rw : ∀ ⦃a : ι → ℝ⦄, Membership.mem (γ := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} a → a ∉ {y : ι → ℝ | x < y i}
⊢ Disjoint.{u_1} (α := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} {y : ι → ℝ | x < y i}

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, Membership.mem (γ := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} a → a ∉ {y : ι → ℝ | x < y i}

Tactic:
fun y (hle : y i ≤ x) hlt => not_lt_of_ge hle hlt

Premises used: Set.Mem, setOf, Not, not_lt_of_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, Membership.mem (γ := Set (ι → ℝ)) {y : ι → ℝ | y i ≤ x} a → a ∉ {y : ι → ℝ | x < y i}

Tactic:
exact fun y (hle : y i ≤ x) hlt => not_lt_of_ge hle hlt

Premises used: not_lt_of_ge
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
inl : ∀ (h : x ≤ I.lower i), I.splitLower i x ≠ I.splitUpper i x
inr : I.lower i < x → I.splitLower i x ≠ I.splitUpper i x
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rcases le_or_gt x (I.lower i) with h | _

Premises used: le_or_gt, BoxIntegral.Box.lower
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
inl : ⊥ ≠ (↑I : WithBot (Box ι))
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]

Premises used: Iff.mpr, BoxIntegral.Box.splitUpper_eq_self, BoxIntegral.Box.splitLower_eq_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ (↑I : WithBot (Box ι))

Tactic:
WithBot.bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ (↑I : WithBot (Box ι))

Tactic:
exact WithBot.bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
(disjoint_splitLower_splitUpper I i x).ne ?_

Premises used: BoxIntegral.Box.disjoint_splitLower_splitUpper, Disjoint.ne
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
inr : I.splitLower i x ≠ ⊥
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
refine (disjoint_splitLower_splitUpper I i x).ne ?_

Premises used: BoxIntegral.Box.disjoint_splitLower_splitUpper, Disjoint.ne
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : I.lower i < x
inr : ¬I.splitLower i x = ⊥
inr₁ : ¬x ≤ I.lower i
inr₂ inr₃ inr₄ inr₅ : I.lower i < x
⊢ I.splitLower i x ≠ ⊥

Tactic:
rwa [Ne, splitLower_eq_bot, not_le]

Premises used: not_le, Ne, BoxIntegral.Box.splitLower_eq_bot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
simp : ∀ (J : WithBot (Box ι)), J = I.splitLower i x ∨ J = I.splitUpper i x → J ≤ (↑I : WithBot (Box ι))
⊢ ∀ (J : WithBot (Box ι)),
    Membership.mem (γ := Finset (WithBot (Box ι))) {I.splitLower i x, I.splitUpper i x} J → J ≤ (↑I : WithBot (Box ι))

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : WithBot (Box ι))

Tactic:
Box.splitLower_le

Premises used: BoxIntegral.Box.splitLower_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x ≤ (↑I : WithBot (Box ι))

Tactic:
Box.splitUpper_le

Premises used: BoxIntegral.Box.splitUpper_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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 : WithBot (Box ι))

Tactic:
exacts [Box.splitLower_le, Box.splitUpper_le]

Premises used: BoxIntegral.Box.splitUpper_le, BoxIntegral.Box.splitLower_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
simp : ∀ (b : WithBot (Box ι)), b = I.splitUpper i x → I.splitLower i x ≠ b → Disjoint (I.splitLower i x) b
⊢ (↑{I.splitLower i x, I.splitUpper i x} : Set (WithBot (Box ι))).Pairwise Disjoint

Tactic:
simp only [Finset.coe_insert, Finset.coe_singleton, true_and, Set.mem_singleton_iff,
        pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton]

Premises used: Finset.coe_singleton, Set.pairwise_singleton, Set.mem_singleton_iff, Set.pairwise_insert_of_symmetric, symmetric_disjoint, Finset.coe_insert, true_and
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
I.disjoint_splitLower_splitUpper i x

Premises used: BoxIntegral.Box.disjoint_splitLower_splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
I_1 J : Box ι
i_1 : ι
x_1 : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
exact I.disjoint_splitLower_splitUpper i x

Premises used: BoxIntegral.Box.disjoint_splitLower_splitUpper
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ (↑J : WithBot (Box ι)) = I.splitLower i x ∨ (↑J : WithBot (Box ι)) = I.splitUpper i x

Tactic:
simp [split]

Premises used: BoxIntegral.Prepartition.split
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔
    (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | y i ≤ x} ∨
      (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ {y : ι → ℝ | x < y i}

Tactic:
simp [mem_split_iff, ← Box.withBotCoe_inj]

Premises used: BoxIntegral.Prepartition.mem_split_iff, BoxIntegral.Box.withBotCoe_inj
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (split I i x).iUnion = (↑I : Set (ι → ℝ))

Tactic:
simp [split, ← inter_union_distrib_left, ← setOf_or, le_or_gt]

Premises used: BoxIntegral.Prepartition.split, le_or_gt, Set.setOf_or, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (split I i x).IsPartition

Tactic:
isPartition_iff_iUnion_eq.2 <| iUnion_split I i x

Premises used: Iff.mpr, BoxIntegral.Prepartition.isPartition_iff_iUnion_eq, BoxIntegral.Prepartition.iUnion_split
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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)
rw₂ 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)
⊢ ∑ J ∈ (split I i x).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)]

Premises used: Finset.sum_pair, BoxIntegral.Prepartition.split, BoxIntegral.Box.splitLower_ne_splitUpper, BoxIntegral.Prepartition.sum_ofWithBot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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)
rw₂ 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)
⊢ ∑ J ∈ (split I i x).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)]

Premises used: BoxIntegral.Prepartition.split, BoxIntegral.Prepartition.sum_ofWithBot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
⊢ split I i x = ⊤

Tactic:
((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm

Premises used: BoxIntegral.Prepartition.isPartitionTop, BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
Goal:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
refine : ∀ (J : Box ι) (hJ : Membership.mem (γ := Finset (Box ι)) (boxes (I := I) ⊤) J), J ∈ (split I i x).boxes
⊢ split I i x = ⊤

Tactic:
refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm

Premises used: BoxIntegral.Prepartition.isPartitionTop, BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Split
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
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
⊢ J ∈ (split I i x).boxes

Tactic:
rcases mem_top.1 hJ with rfl

Premises used: Iff.mp, BoxIntegral.Prepartition.mem_top, rfl