[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
f g : ι →ᵇᵃ[I₀] M
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
g : ι →ᵇᵃ[I₀] M
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), IsPartition π → ∑ Ji in π.boxes, toFun✝ Ji = toFun✝ J
h : { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
toFun✝¹ : Box ι → M
sum_partition_boxes'✝¹ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), IsPartition π → ∑ Ji in π.boxes, toFun✝¹ Ji = toFun✝¹ J
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), IsPartition π → ∑ Ji in π.boxes, toFun✝ Ji = toFun✝ J
h :
  { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ }.toFun =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun
⊢ { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ } =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ J : Box ι
i : ι
f g : ι →ᵇᵃ[I₀] M
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
⊢ ∑ Ji in π.boxes, (↑f + ↑g) Ji = (↑f + ↑g) I
[PROOFSTEP]
simp only [Pi.add_apply, sum_add_distrib, sum_partition_boxes _ hI hπ]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ J : Box ι
i : ι
R : Type ?u.25829
inst✝¹ : Monoid R
inst✝ : DistribMulAction R M
r : R
f : ι →ᵇᵃ[I₀] M
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
⊢ ∑ Ji in π.boxes, (r • ↑f) Ji = (r • ↑f) I
[PROOFSTEP]
simp only [Pi.smul_apply, ← smul_sum, sum_partition_boxes _ hI hπ]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i✝ : ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
i : ι
x : ℝ
⊢ Option.elim' 0 (↑f) (splitLower I i x) + Option.elim' 0 (↑f) (splitUpper I i x) = ↑f I
[PROOFSTEP]
rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
⊢ ι →ᵇᵃ[I₀] M
[PROOFSTEP]
refine' ⟨f, _⟩
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
⊢ ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), IsPartition π → ∑ Ji in π.boxes, f Ji = f J
[PROOFSTEP]
replace hf : ∀ I : Box ι, ↑I ≤ I₀ → ∀ s, (∑ J in (splitMany I s).boxes, f J) = f I
[GOAL]
case hf
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
⊢ ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
[PROOFSTEP]
intro I hI s
[GOAL]
case hf
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
s : Finset (ι × ℝ)
⊢ ∑ J in (splitMany I s).boxes, f J = f I
[PROOFSTEP]
induction' s using Finset.induction_on with a s _ ihs
[GOAL]
case hf.empty
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
⊢ ∑ J in (splitMany I ∅).boxes, f J = f I
[PROOFSTEP]
simp
[GOAL]
case hf.insert
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
⊢ ∑ J in (splitMany I (insert a s)).boxes, f J = f I
[PROOFSTEP]
rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
[GOAL]
case hf.insert
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
⊢ ∑ J in (splitMany I s).boxes, ∑ J' in (split J a.fst a.snd).boxes, f J' = ∑ J in (splitMany I s).boxes, f J
[PROOFSTEP]
refine' Finset.sum_congr rfl fun J' hJ' => _
[GOAL]
case hf.insert
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
⊢ ∑ J' in (split J' a.fst a.snd).boxes, f J' = f J'
[PROOFSTEP]
by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
[GOAL]
case pos
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.snd ∈ Set.Ioo (lower J' a.fst) (upper J' a.fst)
⊢ ∑ J' in (split J' a.fst a.snd).boxes, f J' = f J'
[PROOFSTEP]
rw [sum_split_boxes]
[GOAL]
case pos
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.snd ∈ Set.Ioo (lower J' a.fst) (upper J' a.fst)
⊢ Option.elim' 0 (fun J' => f J') (splitLower J' a.fst a.snd) +
      Option.elim' 0 (fun J' => f J') (splitUpper J' a.fst a.snd) =
    f J'
[PROOFSTEP]
exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
[GOAL]
case neg
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (lower I i) (upper I i) →
          Option.elim' 0 f (splitLower I i x) + Option.elim' 0 f (splitUpper I i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬a ∈ s
ihs : ∑ J in (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : ¬a.snd ∈ Set.Ioo (lower J' a.fst) (upper J' a.fst)
⊢ ∑ J' in (split J' a.fst a.snd).boxes, f J' = f J'
[PROOFSTEP]
rw [split_of_not_mem_Ioo h, top_boxes, Finset.sum_singleton]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
⊢ ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), IsPartition π → ∑ Ji in π.boxes, f Ji = f J
[PROOFSTEP]
intro I hI π hπ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
⊢ ∑ Ji in π.boxes, f Ji = f I
[PROOFSTEP]
have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
Hle : ∀ (J : Box ι), J ∈ π → ↑J ≤ I₀
⊢ ∑ Ji in π.boxes, f Ji = f I
[PROOFSTEP]
rcases hπ.exists_splitMany_le with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
Hle : ∀ (J : Box ι), J ∈ π → ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji in π.boxes, f Ji = f I
[PROOFSTEP]
rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ J : Box ι
i : ι
inst✝ : Fintype ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J in (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
Hle : ∀ (J : Box ι), J ∈ π → ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji in π.boxes, f Ji = ∑ J in π.boxes, ∑ J' in (splitMany J s).boxes, f J'
[PROOFSTEP]
exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ J : Box ι
i : ι
f : ι →ᵇᵃ[I₀] M
g : M →+ N
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : IsPartition π
⊢ ∑ Ji in π.boxes, (↑g ∘ ↑f) Ji = (↑g ∘ ↑f) I
[PROOFSTEP]
simp_rw [comp, ← g.map_sum, f.sum_partition_boxes hI hπ]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
rcases exists_splitMany_inf_eq_filter_of_finite { π₁, π₂ } ((finite_singleton _).insert _) with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} → π ⊓ splitMany I s = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
simp only [inf_splitMany] at hs
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
rcases hs _ (Or.inl rfl), hs _ (Or.inr rfl) with ⟨h₁, h₂⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    π ∈ {π₁, π₂} →
      (biUnion π fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
clear hs
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₁
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
rw [h] at h₁
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in π₁.boxes, ↑f J = ∑ J in π₂.boxes, ↑f J
[PROOFSTEP]
calc
  ∑ J in π₁.boxes, f J = ∑ J in π₁.boxes, ∑ J' in (splitMany J s).boxes, f J' :=
    Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm
  _ = ∑ J in (π₁.biUnion fun J => splitMany J s).boxes, f J := (sum_biUnion_boxes _ _ _).symm
  _ = ∑ J in (π₂.biUnion fun J => splitMany J s).boxes, f J := by rw [h₁, h₂]
  _ = ∑ J in π₂.boxes, ∑ J' in (splitMany J s).boxes, f J' := (sum_biUnion_boxes _ _ _)
  _ = ∑ J in π₂.boxes, f J := Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
⊢ ∑ J in (biUnion π₁ fun J => splitMany J s).boxes, ↑f J = ∑ J in (biUnion π₂ fun J => splitMany J s).boxes, ↑f J
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
case intro.calc_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑J ≤ I₀
case intro.calc_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J✝ : Box ι
i : ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
s : Finset (ι × ℝ)
h₁ : (biUnion π₁ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
h₂ : (biUnion π₂ fun J => splitMany J s) = Prepartition.filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑J ≤ I₀
[PROOFSTEP]
exacts [(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI, (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
⊢ ∀ (I : Box (Fin (n + 1))),
    ↑I ≤ ↑I₀ →
      ∀ {i_1 : Fin (n + 1)} {x : ℝ},
        x ∈ Set.Ioo (lower I i_1) (upper I i_1) →
          Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower I i_1 x) +
              Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitUpper I i_1 x) =
            (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) I
[PROOFSTEP]
intro J hJ j x
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑J ≤ ↑I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (lower J j) (upper J j) →
    Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J j x) +
        Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitUpper J j x) =
      (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
rw [WithTop.coe_le_coe] at hJ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (lower J j) (upper J j) →
    Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J j x) +
        Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitUpper J j x) =
      (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
refine' i.succAboveCases (fun hx => _) (fun j hx => _) j
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (lower J i) (upper J i)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J i x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitUpper J i x) =
    (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, update_same, ← WithBot.some_eq_coe, Option.elim', Box.face,
  (· ∘ ·), update_noteq (Fin.succAbove_ne _ _)]
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (lower J i) (upper J i)
⊢ f x
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x_1 =>
                        lower
                          { lower := J.lower, upper := update J.upper i x,
                            lower_lt_upper := (_ : ∀ (x_2 : Fin (n + 1)), lower J x_2 < update J.upper i x x_2) }
                          (Fin.succAbove i x_1))
                      i_1 <
                    (fun x => upper J (Fin.succAbove i x)) i_1) } -
        f (lower J i)
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x_1 =>
                        lower
                          { lower := J.lower, upper := update J.upper i x,
                            lower_lt_upper := (_ : ∀ (x_2 : Fin (n + 1)), lower J x_2 < update J.upper i x x_2) }
                          (Fin.succAbove i x_1))
                      i_1 <
                    (fun x => upper J (Fin.succAbove i x)) i_1) } +
      (f (upper J i)
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) } -
        f x
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) }) =
    f (upper J i)
        { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
          lower_lt_upper :=
            (_ :
              ∀ (i_1 : Fin n),
                (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) } -
      f (lower J i)
        { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
          lower_lt_upper :=
            (_ :
              ∀ (i_1 : Fin n),
                (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) }
[PROOFSTEP]
abel
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (lower J i) (upper J i)
⊢ f x
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x_1 =>
                        lower
                          { lower := J.lower, upper := update J.upper i x,
                            lower_lt_upper := (_ : ∀ (x_2 : Fin (n + 1)), lower J x_2 < update J.upper i x x_2) }
                          (Fin.succAbove i x_1))
                      i_1 <
                    (fun x => upper J (Fin.succAbove i x)) i_1) } -
        f (lower J i)
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x_1 =>
                        lower
                          { lower := J.lower, upper := update J.upper i x,
                            lower_lt_upper := (_ : ∀ (x_2 : Fin (n + 1)), lower J x_2 < update J.upper i x x_2) }
                          (Fin.succAbove i x_1))
                      i_1 <
                    (fun x => upper J (Fin.succAbove i x)) i_1) } +
      (f (upper J i)
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) } -
        f x
          { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
            lower_lt_upper :=
              (_ :
                ∀ (i_1 : Fin n),
                  (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) }) =
    f (upper J i)
        { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
          lower_lt_upper :=
            (_ :
              ∀ (i_1 : Fin n),
                (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) } -
      f (lower J i)
        { lower := fun x => lower J (Fin.succAbove i x), upper := fun x => upper J (Fin.succAbove i x),
          lower_lt_upper :=
            (_ :
              ∀ (i_1 : Fin n),
                (fun x => lower J (Fin.succAbove i x)) i_1 < (fun x => upper J (Fin.succAbove i x)) i_1) }
[PROOFSTEP]
abel
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
have : (J.face i : WithTop (Box (Fin n))) ≤ I₀.face i := WithTop.coe_le_coe.2 (face_mono hJ i)
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
rw [le_iff_Icc, @Box.Icc_eq_pi _ I₀] at hJ
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑Box.Icc J ⊆ Set.pi Set.univ fun i => Set.Icc (lower I₀ i) (upper I₀ i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) J
[PROOFSTEP]
simp only
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑Box.Icc J ⊆ Set.pi Set.univ fun i => Set.Icc (lower I₀ i) (upper I₀ i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    f (upper J i) (face J i) - f (lower J i) (face J i)
[PROOFSTEP]
rw [hf _ (hJ J.upper_mem_Icc _ trivial), hf _ (hJ J.lower_mem_Icc _ trivial), ← (fb _).map_split_add this j x, ←
  (fb _).map_split_add this j x]
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑Box.Icc J ⊆ Set.pi Set.univ fun i => Set.Icc (lower I₀ i) (upper I₀ i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    Option.elim' 0
          (↑(fb { val := upper J i, property := (_ : upper J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitLower (face J i) j x) +
        Option.elim' 0
          (↑(fb { val := upper J i, property := (_ : upper J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitUpper (face J i) j x) -
      (Option.elim' 0
          (↑(fb { val := lower J i, property := (_ : lower J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitLower (face J i) j x) +
        Option.elim' 0
          (↑(fb { val := lower J i, property := (_ : lower J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitUpper (face J i) j x))
[PROOFSTEP]
have hx' : x ∈ Ioo ((J.face i).lower j) ((J.face i).upper j) := hx
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑Box.Icc J ⊆ Set.pi Set.univ fun i => Set.Icc (lower I₀ i) (upper I₀ i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
hx' : x ∈ Set.Ioo (lower (face J i) j) (upper (face J i) j)
⊢ Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i)) (splitLower J (Fin.succAbove i j) x) +
      Option.elim' 0 (fun J => f (upper J i) (face J i) - f (lower J i) (face J i))
        (splitUpper J (Fin.succAbove i j) x) =
    Option.elim' 0
          (↑(fb { val := upper J i, property := (_ : upper J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitLower (face J i) j x) +
        Option.elim' 0
          (↑(fb { val := upper J i, property := (_ : upper J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitUpper (face J i) j x) -
      (Option.elim' 0
          (↑(fb { val := lower J i, property := (_ : lower J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitLower (face J i) j x) +
        Option.elim' 0
          (↑(fb { val := lower J i, property := (_ : lower J i ∈ (fun i => Set.Icc (lower I₀ i) (upper I₀ i)) i) }))
          (splitUpper (face J i) j x))
[PROOFSTEP]
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, Box.splitLower_def hx', Box.splitUpper_def hx', ←
  WithBot.some_eq_coe, Option.elim', Box.face_mk, update_noteq (Fin.succAbove_ne _ _).symm, sub_add_sub_comm,
  update_comp_eq_of_injective _ (Fin.strictMono_succAbove i).injective j x, ← hf]
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I J✝ : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (lower I₀ i) (upper I₀ i)) → Fin n →ᵇᵃ[↑(face I₀ i)] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (lower I₀ i) (upper I₀ i)) (J : Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J
J : Box (Fin (n + 1))
hJ : ↑Box.Icc J ⊆ Set.pi Set.univ fun i => Set.Icc (lower I₀ i) (upper I₀ i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (lower J (Fin.succAbove i j)) (upper J (Fin.succAbove i j))
this : ↑(face J i) ≤ ↑(face I₀ i)
hx' : x ∈ Set.Ioo (lower (face J i) j) (upper (face J i) j)
⊢ f (upper J i)
          { lower := J.lower ∘ Fin.succAbove i, upper := update (J.upper ∘ Fin.succAbove i) j x,
            lower_lt_upper :=
              (_ : ∀ (i_1 : Fin n), (J.lower ∘ Fin.succAbove i) i_1 < update (J.upper ∘ Fin.succAbove i) j x i_1) } +
        f (upper J i)
          { lower := update (J.lower ∘ Fin.succAbove i) j x, upper := J.upper ∘ Fin.succAbove i,
            lower_lt_upper :=
              (_ : ∀ (i_1 : Fin n), update (J.lower ∘ Fin.succAbove i) j x i_1 < (J.upper ∘ Fin.succAbove i) i_1) } -
      (f (lower J i)
          { lower := J.lower ∘ Fin.succAbove i, upper := update (J.upper ∘ Fin.succAbove i) j x,
            lower_lt_upper :=
              (_ : ∀ (i_1 : Fin n), (J.lower ∘ Fin.succAbove i) i_1 < update (J.upper ∘ Fin.succAbove i) j x i_1) } +
        f (lower J i)
          { lower := update (J.lower ∘ Fin.succAbove i) j x, upper := J.upper ∘ Fin.succAbove i,
            lower_lt_upper :=
              (_ : ∀ (i_1 : Fin n), update (J.lower ∘ Fin.succAbove i) j x i_1 < (J.upper ∘ Fin.succAbove i) i_1) }) =
    f (upper J i)
          { lower := (face J i).lower, upper := update (face J i).upper j x,
            lower_lt_upper := (_ : ∀ (x_1 : Fin n), lower (face J i) x_1 < update (face J i).upper j x x_1) } +
        f (upper J i)
          { lower := update (face J i).lower j x, upper := (face J i).upper,
            lower_lt_upper := (_ : ∀ (x_1 : Fin n), update (face J i).lower j x x_1 < upper (face J i) x_1) } -
      (f (lower J i)
          { lower := (face J i).lower, upper := update (face J i).upper j x,
            lower_lt_upper := (_ : ∀ (x_1 : Fin n), lower (face J i) x_1 < update (face J i).upper j x x_1) } +
        f (lower J i)
          { lower := update (face J i).lower j x, upper := (face J i).upper,
            lower_lt_upper := (_ : ∀ (x_1 : Fin n), update (face J i).lower j x x_1 < upper (face J i) x_1) })
[PROOFSTEP]
simp only [Box.face]


[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ i)
[PROOFSTEP]
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ i)
[PROOFSTEP]
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (↑f) Nat.zero ≤ approx (↑f) (Nat.succ Nat.zero)
[PROOFSTEP]

| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (↑f) Nat.zero ≤ approx (↑f) (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp [approx]
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ ↑f ⊥
[PROOFSTEP]
apply @bot_le _ _ _ (f ⊥)
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
⊢ approx (↑f) (Nat.succ n✝) ≤ approx (↑f) (Nat.succ (Nat.succ n✝))
[PROOFSTEP]

| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
⊢ approx (↑f) (Nat.succ n✝) ≤ approx (↑f) (Nat.succ (Nat.succ n✝))
[PROOFSTEP]
intro
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) (Nat.succ n✝) i✝ ≤ approx (↑f) (Nat.succ (Nat.succ n✝)) i✝
[PROOFSTEP]
apply f.monotone
[GOAL]
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
[PROOFSTEP]
apply i_ih
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (↑f) i ≤ approx (↑f) j
[PROOFSTEP]
induction' j with j ih
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij✝ : i ≤ j
hij : i ≤ Nat.zero
⊢ approx (↑f) i ≤ approx (↑f) Nat.zero
[PROOFSTEP]
cases hij
[GOAL]
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
hij : Nat.zero ≤ j
⊢ approx (↑f) Nat.zero ≤ approx (↑f) Nat.zero
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij✝ : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
hij : i ≤ Nat.succ j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
cases hij
[GOAL]
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j✝ j : ℕ
hij : Nat.succ j ≤ j✝
ih : Nat.succ j ≤ j → approx (↑f) (Nat.succ j) ≤ approx (↑f) j
⊢ approx (↑f) (Nat.succ j) ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
a✝ : Nat.le i j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
exact le_trans (ih ‹_›) (approx_mono' f)
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ b ∈ Part.fix (↑f) a ↔ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
[GOAL]
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ b ∈ Part.fix (↑f) a ↔ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
simp only [Part.fix_def f h₀]
[GOAL]
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a ↔ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a → ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
intro hh
[GOAL]
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ (∃ i, b ∈ approx (↑f) i a) → b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
intro hh
[GOAL]
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
⊢ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
exact ⟨_, hh⟩
[GOAL]
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
have h₁ := Nat.find_spec h₀
[GOAL]
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
h₁ : (approx (↑f) (Nat.find h₀) a).Dom
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
rw [dom_iff_mem] at h₁
[GOAL]
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
h₁ : ∃ y, y ∈ approx (↑f) (Nat.find h₀) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
cases' h₁ with y h₁
[GOAL]
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
y : β a
h₁ : y ∈ approx (↑f) (Nat.find h₀) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
replace h₁ := approx_mono' f _ _ h₁
[GOAL]
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
suffices : y = b
[GOAL]
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
this : y = b
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
subst this
[GOAL]
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
hh : ∃ i, y ∈ approx (↑f) i a
⊢ y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
exact h₁
[GOAL]
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : ∃ i, b ∈ approx (↑f) i a
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
⊢ y = b
[PROOFSTEP]
cases' hh with i hh
[GOAL]
case this.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
i : ℕ
hh : b ∈ approx (↑f) i a
⊢ y = b
[PROOFSTEP]
revert h₁
[GOAL]
case this.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
⊢ y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a → y = b
[PROOFSTEP]
generalize succ (Nat.find h₀) = j
[GOAL]
case this.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
⊢ y ∈ approx (↑f) j a → y = b
[PROOFSTEP]
intro h₁
[GOAL]
case this.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
⊢ y = b
[PROOFSTEP]
wlog case : i ≤ j
[GOAL]
case this.intro.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b
[PROOFSTEP]
cases' le_total i j with H H <;> [skip; symm]
[GOAL]
case this.intro.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b
[PROOFSTEP]
cases' le_total i j with H H
[GOAL]
case this.intro.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b
[PROOFSTEP]
skip
[GOAL]
case this.intro.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y = b
[PROOFSTEP]
symm
[GOAL]
case this.intro.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b
[PROOFSTEP]
apply_assumption
[GOAL]
case this.intro.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b = y
[PROOFSTEP]
apply_assumption
[GOAL]
case this.intro.inr.inl.h₀
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ ∃ i, (approx (↑?this.intro.inr.inl.f) i a).Dom
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.hh
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ b ∈ approx ↑f ?this.intro.inr.inl.i a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.h₁
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y ∈ approx ↑f ?this.intro.inr.inl.j a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.case
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ i ≤ j
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.h₀
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ ∃ i, (approx (↑?this.intro.inr.inr.f) i a).Dom
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.hh
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y ∈ approx ↑f ?this.intro.inr.inr.i a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.h₁
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b ∈ approx ↑f ?this.intro.inr.inr.j a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.case
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ j ≤ i
[PROOFSTEP]
assumption
[GOAL]
α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
case : i ≤ j
⊢ y = b
[PROOFSTEP]
replace hh := approx_mono f case _ _ hh
[GOAL]
α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
i j : ℕ
h₁ : y ∈ approx (↑f) j a
case : i ≤ j
hh : b ∈ approx (↑f) j a
⊢ y = b
[PROOFSTEP]
apply Part.mem_unique h₁ hh
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (↑f) i a).Dom
⊢ b ∈ Part.fix (↑f) a ↔ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
simp only [fix_def' (⇑f) h₀, not_exists, false_iff_iff, not_mem_none]
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (↑f) i a).Dom
⊢ ∀ (x : ℕ), ¬b ∈ approx (↑f) x a
[PROOFSTEP]
simp only [dom_iff_mem, not_exists] at h₀
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), ¬x_1 ∈ approx (↑f) x a
⊢ ∀ (x : ℕ), ¬b ∈ approx (↑f) x a
[PROOFSTEP]
intro
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), ¬x_1 ∈ approx (↑f) x a
x✝ : ℕ
⊢ ¬b ∈ approx (↑f) x✝ a
[PROOFSTEP]
apply h₀
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ b ∈ Part.fix (↑f) a
[PROOFSTEP]
rw [mem_iff f]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
exact ⟨_, hh⟩
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
by_cases hh : ∃ i b, b ∈ approx f i x
[GOAL]
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∃ i b, b ∈ approx (↑f) i x
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
rcases hh with ⟨i, b, hb⟩
[GOAL]
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (↑f) i x
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
exists i
[GOAL]
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
intro b' h'
[GOAL]
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (↑f) i x
b' : β x
h' : b' ∈ Part.fix (↑f) x
⊢ b' ∈ approx (↑f) i x
[PROOFSTEP]
have hb' := approx_le_fix f i _ _ hb
[GOAL]
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (↑f) i x
b' : β x
h' : b' ∈ Part.fix (↑f) x
hb' : b ∈ Part.fix (↑f) x
⊢ b' ∈ approx (↑f) i x
[PROOFSTEP]
obtain rfl := Part.mem_unique h' hb'
[GOAL]
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : b' ∈ Part.fix (↑f) x
hb : b' ∈ approx (↑f) i x
hb' : b' ∈ Part.fix (↑f) x
⊢ b' ∈ approx (↑f) i x
[PROOFSTEP]
exact hb
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ¬∃ i b, b ∈ approx (↑f) i x
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
simp only [not_exists] at hh
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), ¬x_2 ∈ approx (↑f) x_1 x
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
exists 0
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), ¬x_2 ∈ approx (↑f) x_1 x
⊢ Part.fix (↑f) x ≤ approx (↑f) 0 x
[PROOFSTEP]
intro b' h'
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), ¬x_2 ∈ approx (↑f) x_1 x
b' : β x
h' : b' ∈ Part.fix (↑f) x
⊢ b' ∈ approx (↑f) 0 x
[PROOFSTEP]
simp only [mem_iff f] at h'
[GOAL]
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), ¬x_2 ∈ approx (↑f) x_1 x
b' : β x
h' : ∃ i, b' ∈ approx (↑f) i x
⊢ b' ∈ approx (↑f) 0 x
[PROOFSTEP]
cases' h' with i h'
[GOAL]
case neg.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), ¬x_2 ∈ approx (↑f) x_1 x
b' : β x
i : ℕ
h' : b' ∈ approx (↑f) i x
⊢ b' ∈ approx (↑f) 0 x
[PROOFSTEP]
cases hh _ _ h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ ↑f x
[PROOFSTEP]
simp only [(· ∈ ·), forall_exists_index]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ ∀ (x_1 : ℕ), x = ↑(approxChain f) x_1 → x ≤ ↑f x
[PROOFSTEP]
rintro i rfl
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑f (↑(approxChain f) i)
[PROOFSTEP]
apply approx_mono'
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f = ωSup (approxChain f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f ≤ ωSup (approxChain f)
[PROOFSTEP]
intro x
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
cases' exists_fix_le_approx f x with i hx
[GOAL]
case a.intro
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
trans approx f i.succ x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ approx (↑f) (Nat.succ i) x
[PROOFSTEP]
trans
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ?m.11190
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ?m.11190 ≤ approx (↑f) (Nat.succ i) x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part (β x)
[PROOFSTEP]
apply hx
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) i x ≤ approx (↑f) (Nat.succ i) x
[PROOFSTEP]
apply approx_mono' f
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
apply le_ωSup_of_le i.succ
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ↑(Chain.map (approxChain f) (Pi.evalOrderHom x)) (Nat.succ i)
[PROOFSTEP]
dsimp [approx]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ↑f (approx (↑f) i) x ≤ ↑(approxChain f) (Nat.succ i) x
[PROOFSTEP]
rfl
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ↑f
[PROOFSTEP]
apply ωSup_le _ _ _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ Part.fix ↑f
[PROOFSTEP]
simp only [Fix.approxChain, OrderHom.coe_mk]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ),
    ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ Part.fix ↑f
[PROOFSTEP]
intro y x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
y : ℕ
x : α✝
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } y x ≤ Part.fix (↑f) x
[PROOFSTEP]
apply approx_le_fix f
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ Part.fix ↑f ≤ X
[PROOFSTEP]
rw [fix_eq_ωSup f]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ωSup (approxChain f) ≤ X
[PROOFSTEP]
apply ωSup_le _ _ _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ X
[PROOFSTEP]
simp only [Fix.approxChain, OrderHom.coe_mk]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
induction i with
| zero => dsimp [Fix.approx]; apply bot_le
| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
induction i with
| zero => dsimp [Fix.approx]; apply bot_le
| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } Nat.zero ≤ X
[PROOFSTEP]

| zero => dsimp [Fix.approx]; apply bot_le
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } Nat.zero ≤ X
[PROOFSTEP]
dsimp [Fix.approx]
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } 0 ≤ X
[PROOFSTEP]
apply bot_le
[GOAL]
case succ
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ X
[PROOFSTEP]

| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
case succ
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ X
[PROOFSTEP]
trans f X
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ ↑f X
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑f X ≤ X
[PROOFSTEP]
apply f.monotone i_ih
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑f X ≤ X
[PROOFSTEP]
apply hX
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Part.fix ↑f = ↑f (Part.fix ↑f)
[PROOFSTEP]
rw [fix_eq_ωSup f, hc]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) = ωSup (Chain.map (approxChain f) f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) ≤ ωSup (Chain.map (approxChain f) f)
[PROOFSTEP]
apply ωSup_le_ωSup_of_le _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ approxChain f ≤ Chain.map (approxChain f) f
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) j
[PROOFSTEP]
exists i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) i
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
x : α✝
⊢ ↑(approxChain f) i x ≤ ↑(Chain.map (approxChain f) f) i x
[PROOFSTEP]
apply le_f_of_mem_approx _ ⟨i, rfl⟩
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (Chain.map (approxChain f) f) ≤ ωSup (approxChain f)
[PROOFSTEP]
apply ωSup_le_ωSup_of_le _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Chain.map (approxChain f) f ≤ approxChain f
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(Chain.map (approxChain f) f) i ≤ ↑(approxChain f) j
[PROOFSTEP]
exists i.succ
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) = ωSup (Chain.map x✝ (toUnitMono f))
[PROOFSTEP]
ext ⟨⟩ : 1
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) PUnit.unit = ωSup (Chain.map x✝ (toUnitMono f)) PUnit.unit
[PROOFSTEP]
dsimp [OmegaCompletePartialOrder.ωSup]
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑f (Part.ωSup (Chain.map x✝ (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map (Chain.map x✝ (toUnitMono f)) (Pi.evalOrderHom PUnit.unit))
[PROOFSTEP]
erw [hc, Chain.map_comp]
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
⊢ Part.fix ↑(toUnitMono f) () = ↑f (Fix.fix ↑f)
[PROOFSTEP]
rw [Part.fix_eq (to_unit_cont f hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
⊢ ↑(toUnitMono f) (Part.fix ↑(toUnitMono f)) () = ↑f (Fix.fix ↑f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
⊢ ↑(monotoneCurry α β γ) (ωSup c) = ωSup (Chain.map c (monotoneCurry α β γ))
[PROOFSTEP]
ext x y
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ↑(monotoneCurry α β γ) (ωSup c) x y = ωSup (Chain.map c (monotoneCurry α β γ)) x y
[PROOFSTEP]
dsimp [curry, ωSup]
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (Chain.map c (evalOrderHom { fst := x, snd := y })) =
    ωSup (Chain.map (Chain.map (Chain.map c (monotoneCurry α β γ)) (evalOrderHom x)) (evalOrderHom y))
[PROOFSTEP]
rw [map_comp, map_comp]
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (Chain.map c (evalOrderHom { fst := x, snd := y })) =
    ωSup (Chain.map c (OrderHom.comp (OrderHom.comp (evalOrderHom y) (evalOrderHom x)) (monotoneCurry α β γ)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ ↑(monotoneUncurry α β γ) (ωSup c) = ωSup (Chain.map c (monotoneUncurry α β γ))
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ↑(monotoneUncurry α β γ) (ωSup c) { fst := x, snd := y } =
    ωSup (Chain.map c (monotoneUncurry α β γ)) { fst := x, snd := y }
[PROOFSTEP]
dsimp [uncurry, ωSup]
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map (Chain.map c (evalOrderHom x)) (evalOrderHom y)) =
    ωSup (Chain.map (Chain.map c (monotoneUncurry α β γ)) (evalOrderHom { fst := x, snd := y }))
[PROOFSTEP]
rw [map_comp, map_comp]
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map c (OrderHom.comp (evalOrderHom y) (evalOrderHom x))) =
    ωSup (Chain.map c (OrderHom.comp (evalOrderHom { fst := x, snd := y }) (monotoneUncurry α β γ)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
⊢ fix ↑_f = ↑_f (fix ↑_f)
[PROOFSTEP]
dsimp [fix]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
⊢ curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
conv =>
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry))
[PROOFSTEP]
erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]


[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
[PROOFSTEP]
simp [← pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq x fun x => Seq.seq (pure f) fun x => y) = Seq.seq (Seq.seq (pure fun x => x ∘ f) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [seq_assoc, ← comp_map, (· ∘ ·)]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq ((fun x x_1 => x (f x_1)) <$> x) fun x => y) =
    Seq.seq (Seq.seq (pure fun x x_1 => x (f x_1)) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ (f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
[PROOFSTEP]
simp only [← pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ (Seq.seq (pure f) fun x_1 => Seq.seq x fun x => y) = Seq.seq (Seq.seq (pure fun x => f ∘ x) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [seq_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : α → m β
f : β → γ
⊢ f <$> (x >>= g) = do
    let a ← x
    f <$> g a
[PROOFSTEP]
rw [← bind_pure_comp, bind_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : α → m β
f : β → γ
⊢ (do
      let x ← x
      let a ← g x
      pure (f a)) =
    do
    let a ← x
    f <$> g a
[PROOFSTEP]
simp [bind_pure_comp]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ f <$> x >>= g = x >>= g ∘ f
[PROOFSTEP]
rw [← bind_pure_comp, bind_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
[PROOFSTEP]
simp [pure_bind, (· ∘ ·)]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, ← bind_pure_comp, bind_assoc, map_bind, pure_bind]
[GOAL]
α✝ β γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, map_bind, ← bind_pure_comp, bind_assoc, pure_bind]
[GOAL]
α✝ β γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, map_bind, ← bind_pure_comp, bind_assoc, pure_bind, bind_pure]
[GOAL]
α β γ : Type u
F : Type → Type v
inst✝ : Alternative F
h : Decidable True
⊢ guard True = pure ()
[PROOFSTEP]
simp [guard, if_pos]
[GOAL]
α β γ : Type u
F : Type → Type v
inst✝ : Alternative F
h : Decidable False
⊢ guard False = failure
[PROOFSTEP]
simp [guard, if_neg not_false]
[GOAL]
α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
⊢ ∀ {α : Type u} (x : e ⊕ α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inl
α β γ : Type u
e : Type v
α✝ : Type u
val✝ : e
⊢ id <$> inl val✝ = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr
α β γ : Type u
e : Type v
α✝ : Type u
val✝ : α✝
⊢ id <$> inr val✝ = inr val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : e
⊢ (h✝ ∘ g✝) <$> inl val✝ = h✝ <$> g✝ <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr val✝ = h✝ <$> g✝ <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : e
⊢ (SeqLeft.seqLeft (inl val✝) fun x => y✝) = Seq.seq (Function.const β✝ <$> inl val✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : α✝
⊢ (SeqLeft.seqLeft (inr val✝) fun x => y✝) = Seq.seq (Function.const β✝ <$> inr val✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : e
⊢ (SeqRight.seqRight (inl val✝) fun x => y✝) = Seq.seq (Function.const α✝ id <$> inl val✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : α✝
⊢ (SeqRight.seqRight (inr val✝) fun x => y✝) = Seq.seq (Function.const α✝ id <$> inr val✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ val✝ : e
⊢ (SeqRight.seqRight (inl val✝¹) fun x => inl val✝) = Seq.seq (Function.const α✝ id <$> inl val✝¹) fun x => inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : e
val✝ : β✝
⊢ (SeqRight.seqRight (inl val✝¹) fun x => inr val✝) = Seq.seq (Function.const α✝ id <$> inl val✝¹) fun x => inr val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : α✝
val✝ : e
⊢ (SeqRight.seqRight (inr val✝¹) fun x => inl val✝) = Seq.seq (Function.const α✝ id <$> inr val✝¹) fun x => inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : α✝
val✝ : β✝
⊢ (SeqRight.seqRight (inr val✝¹) fun x => inr val✝) = Seq.seq (Function.const α✝ id <$> inr val✝¹) fun x => inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (g : α → β) (x : e ⊕ α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
g✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : α → β) (x : e ⊕ α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
val✝ : e
⊢ (do
      let a ← inl val✝
      pure (f✝ a)) =
    f✝ <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
val✝ : α✝
⊢ (do
      let a ← inr val✝
      pure (f✝ a)) =
    f✝ <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : e ⊕ (α → β)) (x : e ⊕ α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : e ⊕ (α✝ → β✝)
x✝ : e ⊕ α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    Seq.seq f✝ fun x => x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
val✝ : e
⊢ (do
      let x ← inl val✝
      x <$> x✝) =
    Seq.seq (inl val✝) fun x => x✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
val✝ : α✝ → β✝
⊢ (do
      let x ← inr val✝
      x <$> x✝) =
    Seq.seq (inr val✝) fun x => x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : α) (f : α → e ⊕ β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → e ⊕ β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (x : e ⊕ α) (f : α → e ⊕ β) (g : β → e ⊕ γ), x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
val✝ : e
⊢ inl val✝ >>= f✝ >>= g✝ = inl val✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
val✝ : α✝
⊢ inr val✝ >>= f✝ >>= g✝ = inr val✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x => b) = (fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b
[PROOFSTEP]
simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map]
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x => b) = Seq.seq (((fun x => (fun p => f p.fst p.snd) ∘ x) ∘ Prod.mk) <$> a) fun x => b
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ ((fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => f a b) <$> b) fun x => a
[PROOFSTEP]
rw [@CommApplicative.commutative_prod m h]
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ ((fun p => f p.fst p.snd) <$> Seq.seq ((fun b a => (a, b)) <$> b) fun x => a) =
    Seq.seq ((fun b a => f a b) <$> b) fun x => a
[PROOFSTEP]
simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map, (· ∘ ·)]