[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
⊢ Henstock ≤ Riemann
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
⊢ Henstock ≤ McShane
[PROOFSTEP]
trivial
[GOAL]
ι✝ : Type u_1
inst✝ : Fintype ι✝
I J : Box ι✝
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ : IntegrationParams
ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ RCond l r
[PROOFSTEP]
simp [RCond, hl]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
wlog hc : c₁ ≤ c₂ with H
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
H :
  ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {J : Box ι} {c : ℝ≥0} {c₁ c₂ : ℝ≥0} {r : (ι → ℝ) → ↑(Set.Ioi 0)}
    {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π : TaggedPrepartition I} {π₁ π₂ : TaggedPrepartition I} {l : IntegrationParams}
    {l₁ l₂ : IntegrationParams},
    MemBaseSet l I c₁ r₁ π₁ →
      MemBaseSet l I c₂ r₂ π₂ →
        TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂ →
          c₁ ≤ c₂ →
            ∃ π,
              Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
                (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧
                  (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
hc : ¬c₁ ≤ c₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
simpa [hU, _root_.and_comm] using @H _ _ I J c c₂ c₁ r r₂ r₁ π π₂ π₁ _ l₂ l₁ h₂ h₁ hU.symm (le_of_not_le hc)
[GOAL]
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
by_cases hD : (l.bDistortion : Prop)
[GOAL]
case pos
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : l.bDistortion = true
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
rcases h₁.4 hD with ⟨π, hπU, hπc⟩
[GOAL]
case pos.intro.intro
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : l.bDistortion = true
π : Prepartition I
hπU : Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁
hπc : Prepartition.distortion π ≤ c₁
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
exact ⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩
[GOAL]
case neg
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : ¬l.bDistortion = true
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
exact ⟨π₁.toPrepartition.compl, π₁.toPrepartition.iUnion_compl, fun h => (hD h).elim, fun h => (hD h).elim⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ₁ : MemBaseSet l I c r₁ π₁
hle : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : Prepartition.iUnion π₂ = ↑I \ TaggedPrepartition.iUnion π₁
hc : l.bDistortion = true → Prepartition.distortion π₂ ≤ c
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion ⊥ = ↑I \ TaggedPrepartition.iUnion (unionComplToSubordinate π₁ π₂ hU r₂) ∧
    Prepartition.distortion ⊥ ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
⊢ MemBaseSet l I c r (TaggedPrepartition.filter π p)
[PROOFSTEP]
refine'
  ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1, fun hD =>
    (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => _⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
set π₂ := π.filter fun J => ¬p J
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
have : Disjoint π₁.iUnion π₂.iUnion := by simpa [hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
⊢ Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
[PROOFSTEP]
simpa [hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
refine' ⟨π₁.disjUnion π₂.toPrepartition this, _, _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ Prepartition.iUnion (Prepartition.disjUnion π₁ π₂.toPrepartition this) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by simp [*]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this✝ : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
this :
  ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ Prepartition.iUnion (Prepartition.disjUnion π₁ π₂.toPrepartition this✝) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
simp [*]
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
have h : (π.filter p).iUnion ⊆ π.iUnion := biUnion_subset_biUnion_left (Finset.filter_subset _ _)
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
⊢ ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.refine'_1.h
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ↔
    x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
fconstructor
[GOAL]
case intro.intro.refine'_1.h.mp
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) →
    x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
[GOAL]
case intro.intro.refine'_1.h.mp.inl.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxπ : ¬x ∈ TaggedPrepartition.iUnion π
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
case intro.intro.refine'_1.h.mp.inr.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxπ : x ∈ TaggedPrepartition.iUnion π
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
[GOAL]
case intro.intro.refine'_1.h.mpr
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) →
    x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
rintro ⟨hxI, hxp⟩
[GOAL]
case intro.intro.refine'_1.h.mpr.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
by_cases hxπ : x ∈ π.iUnion
[GOAL]
case pos
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
hxπ : x ∈ TaggedPrepartition.iUnion π
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
case neg
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
hxπ : ¬x ∈ TaggedPrepartition.iUnion π
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ Prepartition.distortion (Prepartition.disjUnion π₁ π₂.toPrepartition this) ≤ c
[PROOFSTEP]
have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this✝ : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
this : distortion (TaggedPrepartition.filter π fun J => ¬p J) ≤ c
⊢ Prepartition.distortion (Prepartition.disjUnion π₁ π₂.toPrepartition this✝) ≤ c
[PROOFSTEP]
simpa [hc]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
⊢ MemBaseSet l I c r (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
refine'
  ⟨TaggedPrepartition.isSubordinate_biUnionTagged.2 fun J hJ => (h J hJ).1, fun hH =>
    TaggedPrepartition.isHenstock_biUnionTagged.2 fun J hJ => (h J hJ).2 hH, fun hD => _, fun hD => _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ distortion (Prepartition.biUnionTagged π πi) ≤ c
[PROOFSTEP]
rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∀ (b : Box ι), b ∈ π.boxes → distortion (πi b) ≤ c
[PROOFSTEP]
exact fun J hJ => (h J hJ).3 hD
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
refine' ⟨_, _, hc hD⟩
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π) = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ↑I \ Prepartition.iUnion (Prepartition.biUnion π fun J => (πi J).toPrepartition) =
    ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ l₁ l₂ : IntegrationParams
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ toFilteriUnion l I π₁ = toFilteriUnion l I π₂
[PROOFSTEP]
simp only [toFilteriUnion, toFilterDistortioniUnion, h]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ HasBasis (toFilteriUnion l I π₀) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    HasBasis (toFilterDistortioniUnion l I c π₀) (RCond l) fun r =>
      {π | MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
⊢ HasBasis (toFilteriUnion l I π₀) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
simpa only [setOf_and, setOf_exists] using hasBasis_iSup this
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ HasBasis (toFilteriUnion l I ⊤) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ IsPartition π}
[PROOFSTEP]
simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using l.hasBasis_toFilteriUnion I ⊤
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ HasBasis (toFilter l I) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r => {π | ∃ c, MemBaseSet l I c (r c) π}
[PROOFSTEP]
simpa only [setOf_exists] using hasBasis_iSup (l.hasBasis_toFilterDistortion I)
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
⊢ Tendsto (↑(embedBox I J h)) (toFilteriUnion l I ⊤) (toFilteriUnion l J (Prepartition.single J I h))
[PROOFSTEP]
simp only [toFilteriUnion, tendsto_iSup]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I i ⊤)
      (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c (Prepartition.single J I h))
[PROOFSTEP]
intro c
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
⊢ Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤)
    (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c (Prepartition.single J I h))
[PROOFSTEP]
set π₀ := Prepartition.single J I h
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤) (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c π₀)
[PROOFSTEP]
refine' le_iSup_of_le (max c π₀.compl.distortion) _
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Filter.map (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤) ≤
    toFilterDistortioniUnion l J (max c (Prepartition.distortion (Prepartition.compl π₀))) π₀
[PROOFSTEP]
refine'
  ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => _
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
⊢ ∃ ia,
    RCond l ia ∧
      ∀ (x : TaggedPrepartition I),
        x ∈ {π | MemBaseSet l I c ia π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion ⊤} →
          ↑(embedBox I J h) x ∈
            {π |
              MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
                TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
refine' ⟨r, hr, fun π hπ => _⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : π ∈ {π | MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion ⊤}
⊢ ↑(embedBox I J h) π ∈
    {π |
      MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
        TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
⊢ ↑(embedBox I J h) π ∈
    {π |
      MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
        TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
refine' ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑J \ TaggedPrepartition.iUnion (↑(embedBox I J h) π) ∧
      Prepartition.distortion π' ≤ max c (Prepartition.distortion (Prepartition.compl π₀))
[PROOFSTEP]
refine' ⟨_, π₀.iUnion_compl.trans _, le_max_right _ _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ ↑J \ Prepartition.iUnion π₀ = ↑J \ TaggedPrepartition.iUnion (↑(embedBox I J h) π)
[PROOFSTEP]
congr 1
[GOAL]
case refine'_1.e_a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion π₀ = TaggedPrepartition.iUnion (↑(embedBox I J h) π)
[PROOFSTEP]
exact (Prepartition.iUnion_single h).trans hπ.2.symm
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
⊢ TaggedPrepartition.iUnion (↑(embedBox I J h) π) = Prepartition.iUnion π₀
[PROOFSTEP]
exact hπ.2.trans (Prepartition.iUnion_single _).symm
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ π.toPrepartition ≤ π₀ ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
[PROOFSTEP]
rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : IsHenstock π
hr : IsSubordinate π r
hd : distortion π = Prepartition.distortion π₀
hU : TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
⊢ ∃ π, MemBaseSet l I c r π ∧ π.toPrepartition ≤ π₀ ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
[PROOFSTEP]
refine' ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, _, hc₂⟩⟩, ⟨hle, hU⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : IsHenstock π
hr : IsSubordinate π r
hd : distortion π = Prepartition.distortion π₀
hU : TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π₀) = ↑I \ TaggedPrepartition.iUnion π
[PROOFSTEP]
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Box.distortion I ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
rw [← Prepartition.distortion_top] at hc
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ Prepartition.distortion (Prepartition.compl ⊤) ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : Prepartition.distortion (Prepartition.compl ⊤) ≤ c
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ NeBot (toFilterDistortion l I (Box.distortion I))
[PROOFSTEP]
simpa using (l.toFilterDistortioniUnion_neBot' I ⊤).mono inf_le_left


[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
        map_one' :=
          (_ :
            (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        y✝
[PROOFSTEP]
simp only [FreeMonoid.toList_mul, flip, unop_op, List.foldl_append, op_inj]
[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ (op fun a => List.foldl f (List.foldl f a (↑FreeMonoid.toList x✝)) (↑FreeMonoid.toList y✝)) =
    (op fun a => List.foldl f a (↑FreeMonoid.toList x✝)) * op fun a => List.foldl f a (↑FreeMonoid.toList y✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
        map_one' :=
          (_ :
            (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        y✝
[PROOFSTEP]
apply unop_injective
[GOAL]
case a
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ unop
      (OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x✝ * y✝)) =
    unop
      (OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y✝)
[PROOFSTEP]
funext
[GOAL]
case a.h
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ unop
      (OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x✝¹ * y✝))
      x✝ =
    unop
      (OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x✝¹ *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y✝)
      x✝
[PROOFSTEP]
apply List.foldlM_append
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
        map_one' :=
          (_ :
            (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        y✝
[PROOFSTEP]
funext
[GOAL]
case h
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ OneHom.toFun
      { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
        map_one' :=
          (_ :
            (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
      (x✝¹ * y✝) x✝ =
    (OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          x✝¹ *
        OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          y✝)
      x✝
[PROOFSTEP]
apply List.foldrM_append
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 : Type ?u.11080} (x : α_1), (fun x => ↑f) α_1 (pure x) = pure x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.11080
x✝ : α✝
⊢ (fun x => ↑f) α✝ (pure x✝) = pure x✝
[PROOFSTEP]
simp only [map_one, pure]
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 β_1 : Type ?u.11080} (x : Const α (α_1 → β_1)) (y : Const α α_1),
    (fun x => ↑f) β_1 (Seq.seq x fun x => y) = Seq.seq ((fun x => ↑f) (α_1 → β_1) x) fun x => (fun x => ↑f) α_1 y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ β✝ : Type ?u.11080
x✝ : Const α (α✝ → β✝)
y✝ : Const α α✝
⊢ (fun x => ↑f) β✝ (Seq.seq x✝ fun x => y✝) = Seq.seq ((fun x => ↑f) (α✝ → β✝) x✝) fun x => (fun x => ↑f) α✝ y✝
[PROOFSTEP]
simp only [Seq.seq, map_mul]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
⊢ ↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = foldlM.mk ∘ flip f
[PROOFSTEP]
ext1 x
[GOAL]
case h
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x
[PROOFSTEP]
simp [(· ∘ ·), foldlM.ofFreeMonoid, foldlM.mk, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f
[PROOFSTEP]
ext
[GOAL]
case h
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝
[PROOFSTEP]
simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (foldMap FreeMonoid.of xs) =
    ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs)))
[PROOFSTEP]
simp only [List.reverse_reverse]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs))) =
    ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs))))
[PROOFSTEP]
simp only [List.foldr_eta]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs)))) =
    List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) [])
[PROOFSTEP]
simp [flip, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []) = toList xs
[PROOFSTEP]
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ List.reverse (unop (foldMap (↑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []) = toList xs
[PROOFSTEP]
simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of, Function.comp_apply]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs
[PROOFSTEP]
simp only [foldMap, traverse_map, Function.comp]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)
[PROOFSTEP]
rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop (↑(Foldl.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
[PROOFSTEP]
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get, FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)
[PROOFSTEP]
change _ = Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs) _
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = ↑(Foldr.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
[PROOFSTEP]
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free, foldr.ofFreeMonoid_comp_of]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs
[PROOFSTEP]
simp only [toList_spec, Free.map_eq_map, foldMap_hom, foldMap_map, FreeMonoid.ofList_toList, FreeMonoid.map_of, (· ∘ ·)]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : α → γ → α
a : α
l : t β
⊢ foldl f a (g <$> l) = foldl (fun x y => f x (g y)) a l
[PROOFSTEP]
simp only [foldl, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l
[PROOFSTEP]
simp only [foldr, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : List α
⊢ toList xs = xs
[PROOFSTEP]
simp only [toList_spec, foldMap, traverse]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : List α
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case nil => rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
[PROOFSTEP]
case nil => rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case cons _ _ ih => conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case cons _ _ ih => conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = List.length (toList xs)
[PROOFSTEP]
unfold length
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = List.length (toList xs)
[PROOFSTEP]
rw [foldl_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = List.length (toList xs)
[PROOFSTEP]
generalize toList xs = ys
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys
[PROOFSTEP]
rw [← Nat.add_zero ys.length]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys + 0
[PROOFSTEP]
generalize 0 = n
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = List.length ys + n
[PROOFSTEP]
induction' ys with _ _ ih generalizing n
[GOAL]
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n✝ n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = List.length [] + n
[PROOFSTEP]
simp
[GOAL]
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
[PROOFSTEP]
simp_arith [ih]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop (↑(foldlM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
[PROOFSTEP]
simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f), foldlm.ofFreeMonoid_comp_of, foldlM.get,
  FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ unop (↑(foldlM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x = List.foldlM f x (toList xs)
[PROOFSTEP]
simp [foldlM.ofFreeMonoid, unop_op, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)
[PROOFSTEP]
change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = ↑(foldrM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
[PROOFSTEP]
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f), foldrm.ofFreeMonoid_comp_of, foldrM.get,
  FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun x y => f x (g y)) a l
[PROOFSTEP]
simp only [foldlm, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l
[PROOFSTEP]
simp only [foldrm, foldMap_map, (· ∘ ·), flip]


[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
let p := fun i : ℕ => (Fix.approx f i x).Dom
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
have : p (Nat.find h') := Nat.find_spec h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
generalize hk : Nat.find h' = k
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
replace hk : Nat.find h' = k + (@Upto.zero p).val := hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
rw [hk] at this
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
revert hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
dsimp [Part.fix]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x) =
      Fix.approx f (Nat.succ k) x
[PROOFSTEP]
rw [assert_pos h']
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x =
      Fix.approx f (Nat.succ k) x
[PROOFSTEP]
revert this
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
⊢ p (k + ↑Upto.zero) →
    Nat.find h' = k + ↑Upto.zero →
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x =
        Fix.approx f (Nat.succ k) x
[PROOFSTEP]
generalize Upto.zero = z
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) →
    Nat.find h' = k + ↑z →
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
        Fix.approx f (Nat.succ k) x
[PROOFSTEP]
intro _this hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
    Fix.approx f (Nat.succ k) x
[PROOFSTEP]
suffices : ∀ x', WellFounded.fix (Part.fix.proof_1 f x h') (fixAux f) z x' = Fix.approx f (succ k) x'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
this :
  ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
    Fix.approx f (Nat.succ k) x
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
exact this _
[GOAL]
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
induction k generalizing z with
| zero =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext x : 1
  rw [assert_neg]
  rfl
  rw [Nat.zero_add] at _this
  simpa only [not_not, Coe]
| succ n n_ih =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext : 1
  have hh : ¬(Fix.approx f z.val x).Dom := by
    apply Nat.find_min h'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
induction k generalizing z with
| zero =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext x : 1
  rw [assert_neg]
  rfl
  rw [Nat.zero_add] at _this
  simpa only [not_not, Coe]
| succ n n_ih =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext : 1
  have hh : ¬(Fix.approx f z.val x).Dom := by
    apply Nat.find_min h'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]

| zero =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext x : 1
  rw [assert_neg]
  rfl
  rw [Nat.zero_add] at _this
  simpa only [not_not, Coe]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]
intro x'
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
    Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]
rw [Fix.approx, WellFounded.fix_eq, fixAux]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ f
      (fun x_1 =>
        assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
            x_1)
      x' =
    f (Fix.approx f Nat.zero) x'
[PROOFSTEP]
congr
[GOAL]
case this.zero.e_a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ (fun x_1 =>
      assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
          x_1) =
    Fix.approx f Nat.zero
[PROOFSTEP]
ext x : 1
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ (assert (¬(Fix.approx f (↑z) x✝).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x => (Fix.approx f x x✝).Dom)) (fixAux f) (Upto.succ z h) x) =
    Fix.approx f Nat.zero x
[PROOFSTEP]
rw [assert_neg]
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ none = Fix.approx f Nat.zero x
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
rfl
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
rw [Nat.zero_add] at _this
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p ↑z
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
simpa only [not_not, Coe]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]

| succ n n_ih =>
  intro x'
  rw [Fix.approx, WellFounded.fix_eq, fixAux]
  congr
  ext : 1
  have hh : ¬(Fix.approx f z.val x).Dom := by
    apply Nat.find_min h'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]
intro x'
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
    Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]
rw [Fix.approx, WellFounded.fix_eq, fixAux]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ f
      (fun x_1 =>
        assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
            x_1)
      x' =
    f (Fix.approx f (n + 1)) x'
[PROOFSTEP]
congr
[GOAL]
case this.succ.e_a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ (fun x_1 =>
      assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
          x_1) =
    Fix.approx f (n + 1)
[PROOFSTEP]
ext : 1
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
have hh : ¬(Fix.approx f z.val x).Dom := by
  apply Nat.find_min h'
  rw [hk, Nat.succ_add, ← Nat.add_succ]
  apply Nat.lt_of_succ_le
  apply Nat.le_add_left
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ¬(Fix.approx f (↑z) x).Dom
[PROOFSTEP]
apply Nat.find_min h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ↑z < Nat.find h'
[PROOFSTEP]
rw [hk, Nat.succ_add, ← Nat.add_succ]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ↑z < n + Nat.succ ↑z
[PROOFSTEP]
apply Nat.lt_of_succ_le
[GOAL]
case h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ Nat.succ ↑z ≤ n + Nat.succ ↑z
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
rw [succ_add_eq_succ_add] at _this hk
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (n + Nat.succ ↑z)
hk : Nat.find h' = n + Nat.succ ↑z
x' x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = none
[PROOFSTEP]
dsimp [Part.fix]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ (assert (∃ i, (Fix.approx f i x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x) =
    none
[PROOFSTEP]
rw [assert_neg h']