awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l ≤ Henstock
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
H₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    ε
H₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
A : l.bHenstock = true
⊢ ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (l.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)

Tactic:
simpa only [A, true_imp_iff] using H₂

Premises used: true_imp_iff
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
H :
  ∀ (x : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                  ((g : (a : Box ι) → F) J : F) ≤
                HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)
⊢ ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ ∅ : Set (ι → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x δ →
              (McShane.bHenstock = true →
                  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x) →
                (McShane.bDistortion = true → J.distortion ≤ c) →
                  dist.{w} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f x) : F)
                      ((g : (a : Box ι) → F) J : F) ≤
                    HMul.hMul (β := ℝ) ε ((B : (a : Box ι) → ℝ) J : ℝ)

Tactic:
simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, diff_empty] using H

Premises used: Bool.coe_sort_false, Set.diff_empty, true_imp_iff, false_imp_iff, BoxIntegral.IntegrationParams.McShane
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ I.lower ≤ I.upper

Tactic:
fun i ↦ (I.lower_lt_upper i).le

Premises used: LT.lt.le, BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
i : ι
⊢ I.lower i ≠ I.upper i

Tactic:
(I.lower_lt_upper i).ne

Premises used: BoxIntegral.Box.lower_lt_upper, LT.lt.ne
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l u x : ι → ℝ
H : ∀ (i : ι), l i < u i
⊢ x ∈ { lower := l, upper := u, lower_lt_upper := H : Box ι } ↔ ∀ (i : ι), x i ∈ Ioc (l i) (u i)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ x ∈ (↑I : Set (ι → ℝ)) ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, BoxIntegral.Box.toSet, Iff.rfl, setOf
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ x ∈ I ↔ ∀ (i : ι), x i ∈ Ioc (I.lower i) (I.upper i)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
x : ι → ℝ
I : Box ι
⊢ Membership.mem (γ := Set ((i : ι) → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))
      x ↔
    x ∈ I

Tactic:
mem_univ_pi

Premises used: Set.mem_univ_pi
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (↑I : Set (ι → ℝ)) = Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)

Tactic:
Set.ext fun _ ↦ mem_univ_Ioc.symm

Premises used: Set.ext, Iff.symm, BoxIntegral.Box.mem_univ_Ioc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ I.upper ∈ I

Tactic:
fun i ↦ right_mem_Ioc.2 <| I.lower_lt_upper i

Premises used: Iff.mpr, Set.right_mem_Ioc, BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ ∃ (x : ι → ℝ), x ∈ I

Tactic:
⟨_, I.upper_mem⟩

Premises used: Exists.intro, BoxIntegral.Box.upper_mem
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (↑I : Set (ι → ℝ)).Nonempty

Tactic:
I.exists_mem

Premises used: Set.Mem, BoxIntegral.Box.toSet, setOf, Set.Nonempty, BoxIntegral.Box.exists_mem
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (↑I : Set (ι → ℝ)) ≠ ∅

Tactic:
I.nonempty_coe.ne_empty

Premises used: Set.Nonempty.ne_empty, BoxIntegral.Box.nonempty_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ ∅ ≠ (↑I : Set (ι → ℝ))

Tactic:
I.coe_ne_empty.symm

Premises used: Ne.symm, BoxIntegral.Box.coe_ne_empty
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J ↔ ∀ x ∈ I, x ∈ J

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
h_1 : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
h : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) := h_1
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h

Premises used: closure_mono, closure_pi_set, BoxIntegral.Box.coe_eq_pi, BoxIntegral.Box.lower_ne_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
tfae_have 2 → 3
  | h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

Tactic:
3 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

Tactic:
tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper

Premises used: Set.Icc_subset_Icc_iff, BoxIntegral.Box.lower_le_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ ∀ (a : J.lower ≤ I.lower ∧ I.upper ≤ J.upper), (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
4 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ ∀ (a : J.lower ≤ I.lower ∧ I.upper ≤ J.upper), (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))

Tactic:
tfae_have 4 → 2
  | h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
tfae_2_to_3 : ∀ (a : (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))), Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : ∀ (a : J.lower ≤ I.lower ∧ I.upper ≤ J.upper), (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
⊢ [I ≤ J, (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)), Icc I.lower I.upper ⊆ Icc J.lower J.upper,
      J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

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

Tactic:
Iff.rfl

Premises used: Set.Mem, BoxIntegral.Box.toSet, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

Tactic:
(le_TFAE I J).out 0 3

Premises used: BoxIntegral.Box.le_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h :
  (↑{ lower := l₁, upper := u₁, lower_lt_upper := h₁ : Box ι } : Set (ι → ℝ)) =
    (↑{ lower := l₂, upper := u₂, lower_lt_upper := h₂ } : Set (ι → ℝ))
⊢ (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁

Tactic:
simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h

Premises used: BoxIntegral.Box.le_iff_bounds, Set.Subset.antisymm_iff, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
e_lower : l₁ = l₂
e_upper : u₁ = u₂
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ : Box ι } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }

Tactic:
congr
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂

Tactic:
le_antisymm h.2.1 h.1.1

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ u₁ = u₂

Tactic:
le_antisymm h.1.2 h.2.2

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂

Tactic:
exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2]

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ (↑I : Set (ι → ℝ)) = (↑J : Set (ι → ℝ)) ↔ I = J

Tactic:
injective_coe.eq_iff

Premises used: Function.Injective.eq_iff, BoxIntegral.Box.injective_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
H : ∀ (x : ι → ℝ), x ∈ I ↔ x ∈ J
⊢ I = J

Tactic:
injective_coe <| Set.ext H

Premises used: Set.ext, BoxIntegral.Box.injective_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
h : Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ))
⊢ I ≠ J

Tactic:
mt coe_inj.2 <| h.ne I.coe_ne_empty

Premises used: Iff.mpr, BoxIntegral.Box.coe_inj, mt, BoxIntegral.Box.coe_ne_empty, Disjoint.ne
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I = Icc I.lower I.upper

Tactic:
rfl

Premises used: setOf, Set.Icc, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) I.upper

Tactic:
right_mem_Icc.2 I.lower_le_upper

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, Set.Icc, BoxIntegral.Box.lower_le_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) I.lower

Tactic:
left_mem_Icc.2 I.lower_le_upper

Premises used: Iff.mpr, Set.Mem, setOf, Set.Icc, Set.left_mem_Icc, BoxIntegral.Box.lower_le_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ IsCompact.{u_1} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
isCompact_Icc

Premises used: setOf, CompactIccSpace.isCompact_Icc, Set.Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ Eq (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Icc (I.lower i) (I.upper i) : Set ((i : ι) → ℝ))

Tactic:
(pi_univ_Icc _ _).symm

Premises used: setOf, Set.Icc, Eq.symm, Set.pi_univ_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : Box ι
⊢ I ≤ J ↔
    Subset (α := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
      ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))

Tactic:
(le_TFAE I J).out 0 2

Premises used: BoxIntegral.Box.le_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
⊢ Antitone (β := ι → ℝ) fun (I : Box ι) ↦ I.lower

Tactic:
fun _ _ H ↦ (le_iff_bounds.1 H).1

Premises used: BoxIntegral.Box.le_iff_bounds, Antitone, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
⊢ Monotone (β := ι → ℝ) fun (I : Box ι) ↦ I.upper

Tactic:
fun _ _ H ↦ (le_iff_bounds.1 H).2

Premises used: BoxIntegral.Box.le_iff_bounds, Monotone, And.right, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (↑I : Set (ι → ℝ)) ⊆ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I

Tactic:
fun _ hx ↦ ⟨fun i ↦ (hx i).1.le, fun i ↦ (hx i).2⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Subset, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
intro : ∀ (val : Fintype ι), Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
⊢ Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
val : Fintype ι
⊢ Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
Metric.isBounded_Icc _ _

Premises used: setOf, Set.Icc, Metric.isBounded_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
val : Fintype ι
⊢ Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
exact Metric.isBounded_Icc _ _

Premises used: Metric.isBounded_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
⊢ Bornology.IsBounded (↑I : Set (ι → ℝ))

Tactic:
Bornology.IsBounded.subset I.isBounded_Icc coe_subset_Icc

Premises used: BoxIntegral.Box.isBounded_Icc, Bornology.IsBounded.subset, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ)) ∅

Tactic:
rfl

Premises used: BoxIntegral.Box.withBotToSet, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (↑(↑I : WithBot (Box ι)) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))

Tactic:
rfl

Premises used: BoxIntegral.Box.toSet, setOf, BoxIntegral.Box.withBotToSet, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
⊢ (match (motive := Option (Box ι) → Bool) ⊥ with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty.{u_1} (α := ι → ℝ) (↑⊥ : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : Box ι
⊢ (match (motive := Option (Box ι) → Bool) (↑I : WithBot (Box ι)) with
      | some val => true
      | none => false) =
      true ↔
    (↑(↑I : WithBot (Box ι)) : Set (ι → ℝ)).Nonempty

Tactic:
simp [I.nonempty_coe]

Premises used: BoxIntegral.Box.nonempty_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I : WithBot (Box ι)
bot :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = ⊥), (↑J : Set (ι → ℝ)))
    (↑⊥ : Set (ι → ℝ))
coe :
  ∀ (a : Box ι),
    ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = (↑a : WithBot (Box ι))), (↑J : Set (ι → ℝ)) =
      (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ))
⊢ ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = I), (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))

Tactic:
induction I
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = ⊥), (↑J : Set (ι → ℝ)))
    (↑⊥ : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
a : Box ι
⊢ ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = (↑a : WithBot (Box ι))), (↑J : Set (ι → ℝ)) =
    (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
I J : WithBot (Box ι)
bot : (↑⊥ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ ⊥ ≤ J
coe : ∀ (a : Box ι), (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ J
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ I ≤ J

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

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

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

Tactic:
simp [subset_empty_iff]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
a a_1 : Box ι
⊢ (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑(↑a_1 : WithBot (Box ι)) : Set (ι → ℝ)) ↔
    (↑a : WithBot (Box ι)) ≤ (↑a_1 : WithBot (Box ι))

Tactic:
simp [le_def]

Premises used: BoxIntegral.Box.le_def