awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c 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) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c 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 : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hf : ∀ i ∈ π.boxes, i ∉ {J ∈ π.boxes | π.tag J ∉ s} → 0 ≤ HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) i : ℝ)
⊢ LE.le (α := ℝ) (∑ J ∈ π.boxes with π.tag J ∉ s, HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) J : ℝ))
    (∑ J ∈ π.boxes, HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) J : ℝ))
have h : {J ∈ π.boxes | π.tag J ∉ s} ⊆ π.boxes
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c 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) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c 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 : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
⊢ ∑ J ∈ π.boxes, HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) J : ℝ) =
    HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
have rw : ε' * ∑ i ∈ π.boxes, (B : (a : Box ι) → ℝ) i = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
Tactic: rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c 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) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c 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 : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
rw : ε' * ∑ i ∈ π.boxes, (B : (a : Box ι) → ℝ) i = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
⊢ ∑ J ∈ π.boxes, HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) J : ℝ) =
    HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
have rw₁ : HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) I : ℝ) = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
Tactic: rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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.bRiemann = false
B : ι →ᵇᵃ[(↑I : WithTop (Box ι))] ℝ
hB0 : ∀ (J : Box ι), LE.le (α := ℝ) (0 : ℝ) ((B : (a : Box ι) → ℝ) J : ℝ)
g : ι →ᵇᵃ[(↑I : WithTop (Box ι))] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I ∩ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₁ c 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) ≤
                    ε
δ₂ : (c : ℝ≥0) → (x : ι → ℝ) → (ε : ℝ) → { a : ℝ // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0) (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ s : Set (ι → ℝ)) x →
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ Metric.closedBall x (↑(δ₂ c 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 : ℝ)
ε0' : 0 < ε / 2
H0 : 0 < HPow.hPow (α := ℝ) 2 (Fintype.card ι)
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), (↑t : Set (ι → ℝ)) ⊆ s → ∑ i ∈ t, HPow.hPow (α := ℝ) 2 (Fintype.card ι) * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) := fun (c : ℝ≥0) (x : ι → ℝ) ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
rw : ε' * ∑ i ∈ π.boxes, (B : (a : Box ι) → ℝ) i = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
rw₁ : HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) I : ℝ) = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
⊢ ∑ J ∈ π.boxes, HMul.hMul (β := ℝ) ε' ((B : (a : Box ι) → ℝ) J : ℝ) =
    HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
have rw₂ : HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε' = HMul.hMul (α := ℝ) ((B : (a : Box ι) → ℝ) I : ℝ) ε'
Tactic: rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
⊢ [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
have tfae_1_iff_2 : I ≤ J ↔ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
Tactic: tfae_have 1 ↔ 2 := Iff.rfl
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
Goal:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ (↑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
have tfae_2_to_3 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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
⊢ [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
have tfae_3_iff_4 : 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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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 ≤ J, (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)), Icc I.lower I.upper ⊆ Icc J.lower J.upper,
      J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
have tfae_4_to_2 : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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 (ι → ℝ))
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ : Box ι } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
have h₃ : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
Tactic: simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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₁
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ : Box ι } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
have e_lower : l₁ = l₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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₂
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ : Box ι } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
have e_upper : u₁ = u₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
⊢ Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
have intro : ∀ (val : Fintype ι), Bornology.IsBounded.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I : WithBot (Box ι)
⊢ ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = I), (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))
have bot : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = ⊥), (↑J : Set (ι → ℝ)))
  (↑⊥ : Set (ι → ℝ))
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I : WithBot (Box ι)
bot :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) (⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = ⊥), (↑J : Set (ι → ℝ)))
    (↑⊥ : Set (ι → ℝ))
⊢ ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = I), (↑J : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))
have coe : ∀ (a : Box ι),
  ⋃ (J : Box ι), ⋃ (_ : (↑J : WithBot (Box ι)) = (↑a : WithBot (Box ι))), (↑J : Set (ι → ℝ)) =
    (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ))
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : WithBot (Box ι)
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ I ≤ J
have bot : (↑⊥ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ ⊥ ≤ J
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : WithBot (Box ι)
bot : (↑⊥ : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ ⊥ ≤ J
⊢ (↑I : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ I ≤ J
have coe : ∀ (a : Box ι), (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ J
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
J : WithBot (Box ι)
a : Box ι
⊢ (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ J
have coe : (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑⊥ : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ ⊥
Tactic: induction J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
J : WithBot (Box ι)
a : Box ι
coe : (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑⊥ : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ ⊥
⊢ (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ)) ↔ (↑a : WithBot (Box ι)) ≤ J
have coe₁ : ∀ (a_1 : Box ι),
  (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ⊆ (↑(↑a_1 : WithBot (Box ι)) : Set (ι → ℝ)) ↔
    (↑a : WithBot (Box ι)) ≤ (↑a_1 : WithBot (Box ι))
Tactic: induction J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u : ι → ℝ
⊢ 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
have pos : ∀ (h : ∀ (i : ι), l i < u i),
  (↑{ lower := l, upper := u, lower_lt_upper := h : Box ι } : WithBot (Box ι)) = ⊥ ↔ ∃ (i : ι), u i ≤ l i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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
⊢ 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
have neg : ∀ (h : ¬∀ (i : ι), l i < u i), Eq.{u_1 + 1} (α := WithBot (Box ι)) ⊥ ⊥ ↔ ∃ (i : ι), u i ≤ l i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
l u : ι → ℝ
⊢ mk' l u = (↑I : WithBot (Box ι)) ↔ l = I.lower ∧ u = I.upper
have 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
Tactic: obtain ⟨lI, uI, hI⟩ := I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
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
have neg : l = lI → u ≠ uI
Tactic: suffices l = lI → u ≠ uI by simpa
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u : ι → ℝ
⊢ 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))
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))
have 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))
Tactic: rcases not_forall.mp h with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (↑⊥ : Set (ι → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (l i) (u i))
have neg : Ioc (l i) (u i) = ∅
Tactic: rw [coe_bot, univ_pi_eq_empty]