awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ↔ I = J

Tactic:
simp only [Subset.antisymm_iff, ← le_antisymm_iff, withBotCoe_subset_iff]

Premises used: Set.Subset.antisymm_iff, BoxIntegral.Box.withBotCoe_subset_iff, le_antisymm_iff
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
pos :
  ∀ (h : ∀ (i : ι), l i < u i),
    (↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) = ⊥ ↔ ∃ (i : ι), u i ≤ l i
neg : ∀ (h : ¬∀ (i : ι), l i < u i), Eq.{u_1 + 1} (α := WithBot (Box ι)) ⊥ ⊥ ↔ ∃ (i : ι), u i ≤ l i
⊢ Eq.{u_1 + 1} (α := WithBot (Box ι))
      (if h : ∀ (i : ι), l i < u i then (↑{ lower := l, upper := u, lower_lt_upper := h } : WithBot (Box ι)) else ⊥) ⊥ ↔
    ∃ (i : ι), u i ≤ l i

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ (↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) = ⊥ ↔ ∃ (i : ι), u i ≤ l i

Tactic:
simpa using h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ Eq.{u_1 + 1} (α := WithBot (Box ι)) ⊥ ⊥ ↔ ∃ (i : ι), u i ≤ l i

Tactic:
simpa using h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
l u : ι → ℝ
obtain :
  ∀ (lI uI : ι → ℝ) (hI : ∀ (i : ι), lI i < uI i),
    mk' l u = (↑{ lower := lI, upper := uI, lower_lt_upper := hI } : WithBot (Box ι)) ↔
      l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
        u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
⊢ mk' l u = (↑I : WithBot (Box ι)) ↔ l = I.lower ∧ u = I.upper

Tactic:
obtain ⟨lI, uI, hI⟩ := I
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
pos :
  ∀ (h : ∀ (i : ι), l i < u i),
    (↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) =
        (↑{ lower := lI, upper := uI, lower_lt_upper := hI } : WithBot (Box ι)) ↔
      l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
        u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
neg :
  ∀ (h : ¬∀ (i : ι), l i < u i),
    ⊥ = (↑{ lower := lI, upper := uI, lower_lt_upper := hI : Box ι } : WithBot (Box ι)) ↔
      l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
        u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
⊢ (if h : ∀ (i : ι), l i < u i then (↑{ lower := l, upper := u, lower_lt_upper := h } : WithBot (Box ι)) else ⊥) =
      (↑{ lower := lI, upper := uI, lower_lt_upper := hI : Box ι } : WithBot (Box ι)) ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ∀ (i : ι), l i < u i
⊢ (↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) =
      (↑{ lower := lI, upper := uI, lower_lt_upper := hI } : WithBot (Box ι)) ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
this : l = lI → u ≠ uI
⊢ ⊥ = (↑{ lower := lI, upper := uI, lower_lt_upper := hI : Box ι } : WithBot (Box ι)) ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
simpa
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
neg : l = lI → u ≠ uI
⊢ ⊥ = (↑{ lower := lI, upper := uI, lower_lt_upper := hI : Box ι } : WithBot (Box ι)) ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
suffices l = lI → u ≠ uI by simpa
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
hI : ∀ (i : ι), l i < u i
⊢ False

Tactic:
h hI
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
hI : ∀ (i : ι), l i < u i
⊢ False

Tactic:
exact h hI
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
pos :
  ∀ (h : ∀ (i : ι), l i < u i),
    (↑(↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) : Set (ι → ℝ)) =
      Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i)
neg :
  ∀ (h : ¬∀ (i : ι), l i < u i),
    Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ))
    (↑(if h : ∀ (i : ι), l i < u i then (↑{ lower := l, upper := u, lower_lt_upper := h } : WithBot (Box ι)) else ⊥) :
      Set (ι → ℝ))
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ (↑(↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) : Set (ι → ℝ)) =
    Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i)

Tactic:
coe_eq_pi _

Premises used: BoxIntegral.Box.toSet, setOf, BoxIntegral.Box.coe_eq_pi, BoxIntegral.Box.withBotToSet
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ (↑(↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) : Set (ι → ℝ)) =
    Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i)

Tactic:
exact coe_eq_pi _

Premises used: BoxIntegral.Box.coe_eq_pi
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
neg :
  ∀ (i : ι) (hi : ¬l i < u i),
    Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))

Tactic:
rcases not_forall.mp h with ⟨i, hi⟩

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
neg : Ioc (l i) (u i) = ∅
rw : ι
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))

Tactic:
rw [coe_bot, univ_pi_eq_empty]

Premises used: BoxIntegral.Box.coe_bot, Set.univ_pi_eq_empty
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l i) (u i) = ∅

Tactic:
Ioc_eq_empty hi

Premises used: Set.Ioc_eq_empty
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : WithBot (Box ι)
bot : (↑(⊥ ⊓ J) : Set (ι → ℝ)) = (↑⊥ : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
coe :
  ∀ (a : Box ι),
    (↑((↑a : WithBot (Box ι)) ⊓ J) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
⊢ (↑(I ⊓ J) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))

Tactic:
induction I
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
J : WithBot (Box ι)
⊢ ∅ = (↑⊥ : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
J : WithBot (Box ι)
a : Box ι
coe : (↑((↑a : WithBot (Box ι)) ⊓ ⊥) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑⊥ : Set (ι → ℝ))
coe₁ :
  ∀ (a_1 : Box ι),
    (↑((↑a : WithBot (Box ι)) ⊓ (↑a_1 : WithBot (Box ι))) : Set (ι → ℝ)) =
      (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑(↑a_1 : WithBot (Box ι)) : Set (ι → ℝ))
⊢ (↑((↑a : WithBot (Box ι)) ⊓ J) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))

Tactic:
induction J
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
a : Box ι
⊢ ∅ = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑⊥ : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
a a_1 : Box ι
⊢ (↑(mk' (a.lower ⊔ a_1.lower) (a.upper ⊓ a_1.upper)) : Set (ι → ℝ)) =
    (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑(↑a_1 : WithBot (Box ι)) : Set (ι → ℝ))

Tactic:
simp only [coe_eq_pi, ← pi_inter_distrib, Ioc_inter_Ioc, Pi.sup_apply, Pi.inf_apply, coe_mk',
    coe_coe]

Premises used: BoxIntegral.Box.coe_coe, BoxIntegral.Box.coe_mk', Set.Ioc_inter_Ioc, Pi.sup_apply, BoxIntegral.Box.coe_eq_pi, Pi.inf_apply, Set.pi_inter_distrib
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
rw : (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
⊢ I ⊓ J ≤ I

Tactic:
rw [← withBotCoe_subset_iff, coe_inf]

Premises used: BoxIntegral.Box.coe_inf, BoxIntegral.Box.withBotCoe_subset_iff
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
rw : (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ I ⊓ J ≤ J

Tactic:
rw [← withBotCoe_subset_iff, coe_inf]

Premises used: BoxIntegral.Box.coe_inf, BoxIntegral.Box.withBotCoe_subset_iff
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : I ≤ J₁
h₂ : I ≤ J₂
simp :
  ∀ (h₁ : (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ))) (h₂ : (↑I : Set (ι → ℝ)) ⊆ (↑J₂ : Set (ι → ℝ))),
    (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))
⊢ I ≤ J₁ ⊓ J₂

Tactic:
simp only [← withBotCoe_subset_iff, coe_inf] at *

Premises used: BoxIntegral.Box.coe_inf, BoxIntegral.Box.withBotCoe_subset_iff
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ))
h₂ : (↑I : Set (ι → ℝ)) ⊆ (↑J₂ : Set (ι → ℝ))
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))

Tactic:
subset_inter h₁ h₂

Premises used: Set.subset_inter
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I_1 J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ))
h₂ : (↑I : Set (ι → ℝ)) ⊆ (↑J₂ : Set (ι → ℝ))
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))

Tactic:
exact subset_inter h₁ h₂

Premises used: Set.subset_inter
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : WithBot (Box ι)
simp : (↑I : Set (ι → ℝ)) ⊓ (↑J : Set (ι → ℝ)) ≤ ⊥ ↔ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑⊥ : Set (ι → ℝ))
⊢ Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ)) ↔ Disjoint I J

Tactic:
simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]

Premises used: BoxIntegral.Box.coe_inf, BoxIntegral.Box.withBotCoe_subset_iff, disjoint_iff_inf_le
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ⊓ (↑J : Set (ι → ℝ)) ≤ ⊥ ↔ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑⊥ : Set (ι → ℝ))

Tactic:
rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ Disjoint (↑I : WithBot (Box ι)) (↑J : WithBot (Box ι)) ↔ Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ))

Tactic:
disjoint_withBotCoe.symm

Premises used: BoxIntegral.Box.disjoint_withBotCoe, BoxIntegral.Box.toSet, setOf, BoxIntegral.Box.withBotToSet, Iff.symm
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
rw : ¬Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
rw₁ rw₂ : ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
⊢ ¬Disjoint (↑I : WithBot (Box ι)) (↑J : WithBot (Box ι)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty

Tactic:
rw [disjoint_coe, Set.not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter, BoxIntegral.Box.disjoint_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
l u : Fin (n + 1) → ℝ
h : ∀ (i : Fin (n + 1)), l i < u i
i : Fin (n + 1)
⊢ { lower := l, upper := u, lower_lt_upper := h : Box (Fin (n + 1)) }.face i =
    { lower := l ∘ i.succAbove, upper := u ∘ i.succAbove, lower_lt_upper := ⋯ }

Tactic:
rfl

Premises used: BoxIntegral.Box.face, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
I J : Box (Fin (n + 1))
h : I ≤ J
i : Fin (n + 1)
⊢ I.face i ≤ J.face i

Tactic:
fun _ hx _ ↦ Ioc_subset_Ioc ((le_iff_bounds.1 h).1 _) ((le_iff_bounds.1 h).2 _) (hx _)

Premises used: Fin.succAbove, Set.Mem, BoxIntegral.Box.le_iff_bounds, And.right, Set.Ioc_subset_Ioc, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Monotone (β := Box (Fin n)) fun (I : Box (Fin (n + 1))) ↦ I.face i

Tactic:
fun _ _ h ↦ face_mono h i

Premises used: BoxIntegral.Box.face_mono, Set.Mem, Monotone
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Icc (I.lower i) (I.upper i)
⊢ MapsTo (α := (j : Fin n) → ℝ) (β := (j : Fin (n + 1)) → ℝ) (i.insertNth (α := fun (j : Fin (n + 1)) ↦ ℝ) x)
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
fun _ hy ↦ Fin.insertNth_mem_Icc.2 ⟨hx, hy⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.Icc, Set.MapsTo, Fin.insertNth_mem_Icc, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : (j : Fin n) → ℝ
hy : y ∈ (↑(I.face i) : Set (Fin n → ℝ))
simp_rw :
  x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) x y ∈ (↑I : Set (Fin (n + 1) → ℝ))

Tactic:
simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same,
    Fin.insertNth_apply_succAbove]

Premises used: Fin.insertNth_apply_succAbove, BoxIntegral.Box.mem_coe, Fin.insertNth_apply_same, BoxIntegral.Box.mem_def, Fin.forall_iff_succAbove
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : (j : Fin n) → ℝ
hy : y ∈ (↑(I.face i) : Set (Fin n → ℝ))
⊢ x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))

Tactic:
⟨hx, hy⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : (j : Fin n) → ℝ
hy : y ∈ (↑(I.face i) : Set (Fin n → ℝ))
⊢ x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))

Tactic:
exact ⟨hx, hy⟩
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
n : ℕ
f : (Fin (n + 1) → ℝ) → X
I : Box (Fin (n + 1))
h : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
i : Fin (n + 1)
x : ℝ
hx : x ∈ Icc (I.lower i) (I.upper i)
⊢ ContinuousOn (f ∘ i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) x)
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))

Tactic:
h.comp (continuousOn_const.finInsertNth i continuousOn_id) (I.mapsTo_insertNth_face_Icc hx)

Premises used: continuousOn_const, ContinuousOn.comp, BoxIntegral.Box.mapsTo_insertNth_face_Icc, continuousOn_id, ContinuousOn.finInsertNth
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I ⊆ (↑I : Set (ι → ℝ))

Tactic:
fun _ hx i ↦ Ioo_subset_Ioc_self (hx i trivial)

Premises used: trivial, Set.Mem, BoxIntegral.Box.toSet, setOf, Set.Subset, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Subset (α := Set (ι → ℝ)) ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))

Tactic:
I.Ioo_subset_coe.trans coe_subset_Icc

Premises used: BoxIntegral.Box.Ioo_subset_coe, HasSubset.Subset.trans, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
J : ℕ → Box ι
hJ : Monotone J
hl : Tendsto (lower ∘ J) atTop (𝓝 I.lower)
hu : Tendsto (upper ∘ J) atTop (𝓝 I.upper)
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (n : ℕ), (Box.Ioo : (a : Box ι) → Set (ι → ℝ)) (J n))
    ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
have hl' : ∀ i, Antitone fun n ↦ (J n).lower i :=
    fun i ↦ (monotone_eval i).comp_antitone (antitone_lower.comp_monotone hJ)
  have hu' : ∀ i, Monotone fun n ↦ (J n).upper i :=
    fun i ↦ (monotone_eval i).comp (monotone_upper.comp hJ)
  calc
    ⋃ n, Box.Ioo (J n) = pi univ fun i ↦ ⋃ n, Ioo ((J n).lower i) ((J n).upper i) :=
      iUnion_univ_pi_of_monotone fun i ↦ (hl' i).Ioo (hu' i)
    _ = Box.Ioo I :=
      pi_congr rfl fun i _ ↦
        iUnion_Ioo_of_mono_of_isGLB_of_isLUB (hl' i) (hu' i)
          (isGLB_of_tendsto_atTop (hl' i) (tendsto_pi_nhds.1 hl _))
          (isLUB_of_tendsto_atTop (hu' i) (tendsto_pi_nhds.1 hu _))

Premises used: Function.monotone_eval, Trans.trans, Antitone.comp_monotone, Monotone.comp, tendsto_pi_nhds, iUnion_Ioo_of_mono_of_isGLB_of_isLUB, BoxIntegral.Box.monotone_upper, Set.pi_congr, Iff.mp, Set.iUnion_univ_pi_of_monotone, isLUB_of_tendsto_atTop, Monotone.comp_antitone, Antitone.Ioo, rfl, isGLB_of_tendsto_atTop, BoxIntegral.Box.antitone_lower
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
choose :
  ∀ (a b : (i : ι) → ℕ → ℝ) (ha_anti : ∀ (i : ι), StrictAnti (a i)) (hb_mono : ∀ (i : ι), StrictMono (b i))
    (ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i))
    (hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)) (hab : ∀ (i : ι) (k l : ℕ), a i k < b i l)
    (ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i)))
    (hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))),
    ∃ (J : ℕ →o Box ι),
      (∀ (n : ℕ),
          Subset (α := Set (ι → ℝ))
            ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
            ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
        Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
          Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)
⊢ ∃ (J : ℕ →o Box ι),
    (∀ (n : ℕ),
        Subset (α := Set (ι → ℝ))
          ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
          ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
      Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
        Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)

Tactic:
choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto using
    fun i ↦ exists_seq_strictAnti_strictMono_tendsto (I.lower_lt_upper i)

Premises used: exists_seq_strictAnti_strictMono_tendsto, BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
a b : (i : ι) → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))
⊢ ∃ (J : ℕ →o Box ι),
    (∀ (n : ℕ),
        Subset (α := Set (ι → ℝ))
          ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
          ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
      Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
        Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)

Tactic:
⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
        le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
      fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
      tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩

Premises used: Iff.mpr, StrictMono.monotone, BoxIntegral.Box.le_iff_bounds, flip, tendsto_pi_nhds, And.right, And.left, LT.lt.trans_le, And.intro, Exists.intro, OrderHom.mk, BoxIntegral.Box.mk, LE.le.trans_lt, StrictAnti.antitone
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
a b : (i : ι) → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))
⊢ ∃ (J : ℕ →o Box ι),
    (∀ (n : ℕ),
        Subset (α := Set (ι → ℝ))
          ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
          ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
      Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
        Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)

Tactic:
exact
    ⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
        le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
      fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
      tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
simp :
  Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (i : ι) ↦
      (Finset.sup Finset.univ fun (b : ι) ↦
          HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
            ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) /
        HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)
          ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0))
    (Finset.sup Finset.univ fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0)
        (Finset.sup Finset.univ fun (b : ι) ↦ (Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
        ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0))
⊢ I.distortion = J.distortion

Tactic:
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]

Premises used: BoxIntegral.Box.distortion, nndist_pi_def, map_div₀, Real.nndist_eq'