import breen_deligne.constants
import system_of_complexes.completion
import thm95.homotopy
import thm95.col_exact


noncomputable theory

universe variable u

open_locale nnreal -- enable the notation `ℝ≥0` for the nonnegative real numbers.


open polyhedral_lattice opposite
open thm95.universal_constants system_of_double_complexes category_theory breen_deligne
open ProFiltPseuNormGrpWithTinv (of)

section

variables (r r' : ℝ≥0) [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r < 1)] [fact (r' < 1)]
variables (BD : package)
variables (V : SemiNormedGroup.{u}) [normed_with_aut r V]
variables (κ κ' : ℕ → ℝ≥0) [BD.data.very_suitable r r' κ] [package.adept BD κ κ']
variables (M : ProFiltPseuNormGrpWithTinv.{u} r')
variables (m : ℕ)
variables (Λ : PolyhedralLattice.{u})

include BD κ κ' r r' M V

def thm95.IH (m : ℕ) : Prop := ∀ Λ : PolyhedralLattice.{u},
  ​((BD.data.system κ r V r').obj (op $ Hom Λ M)).is_weak_bounded_exact
    (k κ' m) (K r r' BD κ' m) m (c₀ r r' BD κ κ' m Λ)

omit BD κ κ' r r' M V

lemma NSC_row_exact (IH : ∀ m' < m, thm95.IH r r' BD V κ κ' M m')
  (h0m : 0 < m) (i : ℕ) (hi : i ≤ m + 1) :
  ((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row i).is_weak_bounded_exact
    (k₁ κ' m) (K₁ r r' BD κ' m) (m - 1) (c₀ r r' BD κ κ' m Λ) :=
begin
  haveI h0m_ : fact (0 < m) := ⟨h0m⟩
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
i:ℕ
hi:i ≤ m + 1
h0m_:fact (0 < m)
((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row i).is_weak_bounded_exact (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
  have hm' : m - 1 < m := nat.pred_lt h0m.ne'
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
i:ℕ
hi:i ≤ m + 1
h0m_:fact (0 < m)
hm':m - 1 < m
((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row i).is_weak_bounded_exact (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
  rcases i with (i|i|i)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row 0).is_weak_bounded_exact (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row 1).is_weak_bounded_exact (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
((thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)).row i.succ.succ).is_weak_bounded_exact (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
  { rw thm95.double_complex.row_zero
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k₁ κ' m) (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
  have := (IH (m-1) hm' Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k₁ κ' m) (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
    refine (IH (m-1) hm' Λ).of_le BD.data.system_admissible _ _ le_rfl _
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (c₀ r r' BD κ κ' (m - 1) Λ ≤ c₀ r r' BD κ κ' m Λ),
    swap 3
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (c₀ r r' BD κ κ' (m - 1) Λ ≤ c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:0 ≤ m + 1
this:((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥M))).is_weak_bounded_exact (k κ' (m - 1)) (K r r' BD κ' (m - 1))
  (m - 1)
  (c₀ r r' BD κ κ' (m - 1) Λ)
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m),
    { apply c₀_mono, },
    all_goals { apply_instance } apply_instance } },
  { rw thm95.double_complex.row_one
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
((BD.data.system κ r V r').obj
   (op (Hom ↥((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk 0)) ↥M))).is_weak_bounded_exact
  (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
    refine (IH (m-1) hm' _).of_le BD.data.system_admissible _ _ le_rfl _
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact
  (c₀ r r' BD κ κ' (m - 1) ((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk 0)) ≤
     c₀ r r' BD κ κ' m Λ),
    swap 3
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact
  (c₀ r r' BD κ κ' (m - 1) ((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk 0)) ≤
     c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m),
    { apply c₀_pred_le
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
hi:1 ≤ m + 1
0 < m, exact h0m },
    all_goals { apply_instance } apply_instance } },
  { rw thm95.double_complex.row
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
((system_of_complexes.rescale_functor (i + 2)).obj
   ((BD.data.system κ r V r').obj
      (op
         (Hom ↥((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk (i + 1)))
            ↥M)))).is_weak_bounded_exact
  (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
    apply system_of_complexes.rescale_is_weak_bounded_exact
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
((BD.data.system κ r V r').obj
   (op (Hom ↥((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk (i + 1))) ↥M))).is_weak_bounded_exact
  (k₁ κ' m)
  (K₁ r r' BD κ' m)
  (m - 1)
  (c₀ r r' BD κ κ' m Λ),
    refine (IH (m-1) hm' _).of_le BD.data.system_admissible _ _ le_rfl _
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact
  (c₀ r r' BD κ κ' (m - 1) ((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk (i + 1))) ≤
     c₀ r r' BD κ κ' m Λ),
    swap 3
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact
  (c₀ r r' BD κ κ' (m - 1) ((Λ.cosimplicial (N r r' BD κ' m)).obj (simplex_category.mk (i + 1))) ≤
     c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact (k κ' (m - 1) ≤ k₁ κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
fact (K r r' BD κ' (m - 1) ≤ K₁ r r' BD κ' m),
    { apply c₀_pred_le_of_le
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
h0m:0 < m
h0m_:fact (0 < m)
hm':m - 1 < m
i:ℕ
hi:i.succ.succ ≤ m + 1
i + 2 ≤ m + 1, exact hi },
    all_goals { apply_instance } apply_instance } }
end
.

def NSC (IH : ∀ m' < m, thm95.IH r r' BD V κ κ' M m')
  [pseudo_normed_group.splittable (Λ →+ M) (N r r' BD κ' m) (lem98.d Λ (N r r' BD κ' m))] :
  normed_spectral_conditions (thm95.double_complex BD.data κ r r' V Λ M (N r r' BD κ' m)) m
    (k₁ κ' m) (K₁ r r' BD κ' m) (k' κ' m) (ε r r' BD κ' m) (c₀ r r' BD κ κ' m Λ) (H r r' BD κ' m) :=
{ row_exact := NSC_row_exact _ _ _ _ _ _ _ _ _ IH,
  col_exact :=
  begin
    let N := N r r' BD κ' m
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
∀ (j : ℕ),
  j ≤ m →
  ((thm95.double_complex BD.data κ r r' V Λ M (thm95.universal_constants.N r r' BD κ' m)).col
     j).is_weak_bounded_exact
    (k₁ κ' m)
    (K₁ r r' BD κ' m)
    m
    (c₀ r r' BD κ κ' m Λ),
    intros j hj
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
((thm95.double_complex BD.data κ r r' V Λ M (thm95.universal_constants.N r r' BD κ' m)).col
   j).is_weak_bounded_exact
  (k₁ κ' m)
  (K₁ r r' BD κ' m)
  m
  (c₀ r r' BD κ κ' m Λ),
    refine thm95.col_exact BD.data κ r r' V Λ M N j (lem98.d Λ N) (k₁_sqrt κ' m) m _ _
      (k₁ κ' m) (K₁ r r' BD κ' m) (le_of_eq _) _ _ (c₀ r r' BD κ κ' m Λ) ⟨le_rfl⟩ infer_instance ⟨le_rfl⟩
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
lem98.d ↥Λ N ≤
  (k₁_sqrt κ' m - 1) * (r' * (κ j * c₀ r r' BD κ κ' m Λ)) / ↑(thm95.universal_constants.N r r' BD κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
k₁_sqrt κ' m * k₁_sqrt κ' m = k₁ κ' m
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
↑m + 2 + (r + 1) / (r * (1 - r)) * (↑m + 2) ^ 2 ≤ K₁ r r' BD κ' m,
    { apply c₀_spec
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
j ≤ m, assumption', },
    { ext
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
↑(k₁_sqrt κ' m * k₁_sqrt κ' m) = ↑(k₁ κ' m), delta k₁_sqrt
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
↑(⟨real.sqrt ↑(k₁ κ' m), _⟩ * ⟨real.sqrt ↑(k₁ κ' m), _⟩) = ↑(k₁ κ' m), dsimp
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
V:SemiNormedGroup
_inst_6:normed_with_aut r V
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
M:ProFiltPseuNormGrpWithTinv r'
m:ℕ
Λ:PolyhedralLattice
IH:∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' M m'
_inst_9:pseudo_normed_group.splittable (↥Λ →+ ↥M) (thm95.universal_constants.N r r' BD κ' m)
  (lem98.d ↥Λ (thm95.universal_constants.N r r' BD κ' m))
N:ℕ := thm95.universal_constants.N r r' BD κ' m
j:ℕ
hj:j ≤ m
real.sqrt ↑(k₁ κ' m) * real.sqrt ↑(k₁ κ' m) = ↑(k₁ κ' m), simp only [real.mul_self_sqrt, nnreal.zero_le_coe], },
    { apply K₁_spec }
  end,
  htpy := NSC_htpy BD r r' V κ κ' M m Λ,
  admissible := thm95.double_complex_admissible _ }

include BD κ κ' r r' m

/-- A variant of Theorem 9.5 in [Analytic] using weak bounded exactness. -/
theorem thm95' : ∀ (Λ : PolyhedralLattice.{0}) (S : Type) [fintype S]
  (V : SemiNormedGroup.{0}) [normed_with_aut r V],
  ​((BD.data.system κ r V r').obj (op $ Hom Λ (Mbar r' S))).is_weak_bounded_exact
    (k κ' m) (K r r' BD κ' m) m (c₀ r r' BD κ κ' m Λ) :=
begin
  apply nat.strong_induction_on m; clear m
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
∀ (n : ℕ),
  (∀ (m : ℕ),
     m < n →
     ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
     [_inst_10 : normed_with_aut r V],
       ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m)
         m
         (c₀ r r' BD κ κ' m Λ)) →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' n) (K r r' BD κ' n) n
      (c₀ r r' BD κ κ' n Λ),
  introsI m IH Λ S _S_fin V _V_r
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
  (c₀ r r' BD κ κ' m Λ),
  haveI : pseudo_normed_group.splittable
    (Λ →+ (of r' (Mbar r' S))) (N r r' BD κ' m) (lem98.d Λ (N r r' BD κ' m)) :=
    lem98 Λ S (N r r' BD κ' m)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m) (lem98.d ↥Λ (N r r' BD κ' m))
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
  (c₀ r r' BD κ κ' m Λ),
  let cond := NSC.{0} r r' BD V κ κ' (of r' $ Mbar r' S) m Λ _
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m)
  (lem98.d ↥Λ (N r r' BD κ' m))
cond:(thm95.double_complex BD.data κ r r' V Λ (of r' (Mbar r' S)) (N r r' BD κ' m)).normed_spectral_conditions m
(k₁ κ' m)
(K₁ r r' BD κ' m)
(k' κ' m)
(ε r r' BD κ' m)
(c₀ r r' BD κ κ' m Λ)
↑(H r r' BD κ' m) :=
NSC r r' BD V κ κ' (of r' (Mbar r' S)) m Λ ?m_1
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
  (c₀ r r' BD κ κ' m Λ)
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m) (lem98.d ↥Λ (N r r' BD κ' m))
∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' (of r' (Mbar r' S)) m',
  swap
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m) (lem98.d ↥Λ (N r r' BD κ' m))
∀ (m' : ℕ), m' < m → thm95.IH r r' BD V κ κ' (of r' (Mbar r' S)) m'
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m)
  (lem98.d ↥Λ (N r r' BD κ' m))
cond:(thm95.double_complex BD.data κ r r' V Λ (of r' (Mbar r' S)) (N r r' BD κ' m)).normed_spectral_conditions m
(k₁ κ' m)
(K₁ r r' BD κ' m)
(k' κ' m)
(ε r r' BD κ' m)
(c₀ r r' BD κ κ' m Λ)
↑(H r r' BD κ' m) :=
NSC r r' BD V κ κ' (of r' (Mbar r' S)) m Λ ?m_1
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
  (c₀ r r' BD κ κ' m Λ),
  { introsI m' hm' Λ
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m)
  (lem98.d ↥Λ (N r r' BD κ' m))
m':ℕ
hm':m' < m
Λ:PolyhedralLattice
((BD.data.system κ r V r').obj (op (Hom ↥Λ ↥(of r' (Mbar r' S))))).is_weak_bounded_exact (k κ' m')
  (K r r' BD κ' m')
  m'
  (c₀ r r' BD κ κ' m' Λ),
    apply IH
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
IH:∀ (m_1 : ℕ),
  m_1 < m →
  ∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
  [_inst_10 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m_1)
      (K r r' BD κ' m_1)
      m_1
      (c₀ r r' BD κ κ' m_1 Λ)
Λ:PolyhedralLattice
S:Type
_S_fin:fintype S
V:SemiNormedGroup
_V_r:normed_with_aut r V
_inst:pseudo_normed_group.splittable (↥Λ →+ ↥(of r' (Mbar r' S))) (N r r' BD κ' m)
  (lem98.d ↥Λ (N r r' BD κ' m))
m':ℕ
hm':m' < m
Λ:PolyhedralLattice
m' < m, assumption },
  exact normed_spectral cond
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
∀ (Λ : PolyhedralLattice) (S : Type) [_inst_9 : fintype S] (V : SemiNormedGroup)
[_inst_10 : normed_with_aut r V],
  ((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
    (c₀ r r' BD κ κ' m Λ)end

omit BD κ κ' r r' m

/-- Theorem 9.5 in [Analytic] -/
theorem thm95 (Λ : PolyhedralLattice.{0}) (S : Type) [fintype S]
  (V : SemiNormedGroup.{0}) [normed_with_aut r V] :
  ((BD.data.system κ r V r').obj (op $ Hom Λ (Mbar r' S))).is_bounded_exact
    (k κ' m ^ 2) (K r r' BD κ' m + 1) m (c₀ r r' BD κ κ' m Λ) :=
begin
  refine system_of_complexes.is_weak_bounded_exact.strong_of_complete
    _ (thm95' r r' BD κ κ' m Λ S V) _ 1 zero_lt_one
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
Λ:PolyhedralLattice
S:Type
_inst_9:fintype S
V:SemiNormedGroup
_inst_10:normed_with_aut r V
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).admissible,
  apply data.system_admissible
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
BD:package
κ, κ':ℕ → ℝ≥0
_inst_7:BD.data.very_suitable r r' κ
_inst_8:package.adept BD κ κ'
m:ℕ
Λ:PolyhedralLattice
S:Type
_inst_9:fintype S
V:SemiNormedGroup
_inst_10:normed_with_aut r V
((BD.data.system κ r V r').obj (op (Hom ↥Λ (Mbar r' S)))).is_bounded_exact (k κ' m ^ 2) (K r r' BD κ' m + 1) m
  (c₀ r r' BD κ κ' m Λ)end

end



/- ===
Once we have determined the final shape of the statement,
we can update the proof `thm95' → first_target`, and then delete the theorem below.
Now I just want flexibility in changing `thm95`
and not be troubled with fixing the proof of the implication.
=== -/

/-- Theorem 9.5 in [Analytic] -/
theorem thm95'' (BD : package)
  (r r' : ℝ≥0) [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r < 1)] [fact (r' < 1)]
  (κ : ℕ → ℝ≥0) [BD.data.very_suitable r r' κ] [∀ (i : ℕ), fact (0 < κ i)] :
  ∀ m : ℕ,
  ∃ (k K : ℝ≥0) [fact (1 ≤ k)],
  ∀ (Λ : Type) [polyhedral_lattice Λ],
  ∃ c₀ : ℝ≥0,
  ∀ (S : Type) [fintype S],
  ∀ (V : SemiNormedGroup.{0}) [normed_with_aut r V],
    by exactI system_of_complexes.is_weak_bounded_exact
    (​(BD.data.system κ r V r').obj (op $ Hom Λ (Mbar r' S))) k K m c₀ :=
begin
  intro m
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
m:ℕ
∃ (k K : ℝ≥0) [_inst_8 : fact (1 ≤ k)],
  ∀ (Λ : Type) [_inst_9 : polyhedral_lattice Λ],
    ∃ (c₀ : ℝ≥0),
      ∀ (S : Type) [_inst_10 : fintype S] (V : SemiNormedGroup) [_inst_11 : normed_with_aut r V],
        ((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact k K m c₀,
  let κ' := package.κ' BD κ
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
m:ℕ
κ':ℕ → ℝ≥0 := BD.κ' κ
∃ (k K : ℝ≥0) [_inst_8 : fact (1 ≤ k)],
  ∀ (Λ : Type) [_inst_9 : polyhedral_lattice Λ],
    ∃ (c₀ : ℝ≥0),
      ∀ (S : Type) [_inst_10 : fintype S] (V : SemiNormedGroup) [_inst_11 : normed_with_aut r V],
        ((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact k K m c₀,
  haveI _inst_κ' : package.adept BD κ κ' := package.κ'_adept BD κ
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
m:ℕ
κ':ℕ → ℝ≥0 := BD.κ' κ
_inst_κ':package.adept BD κ κ'
∃ (k K : ℝ≥0) [_inst_8 : fact (1 ≤ k)],
  ∀ (Λ : Type) [_inst_9 : polyhedral_lattice Λ],
    ∃ (c₀ : ℝ≥0),
      ∀ (S : Type) [_inst_10 : fintype S] (V : SemiNormedGroup) [_inst_11 : normed_with_aut r V],
        ((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact k K m c₀,
  refine ⟨(k κ' m), (K r r' BD κ' m), infer_instance, λ Λ _inst_Λ, _⟩
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
m:ℕ
κ':ℕ → ℝ≥0 := BD.κ' κ
_inst_κ':package.adept BD κ κ'
Λ:Type
_inst_Λ:polyhedral_lattice Λ
∃ (c₀ : ℝ≥0),
  ∀ (S : Type) [_inst_10 : fintype S] (V : SemiNormedGroup) [_inst_11 : normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
      c₀,
  refine ⟨c₀ r r' BD κ κ' m (@PolyhedralLattice.of Λ _inst_Λ), λ S _inst_S V _inst_V, _⟩
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
m:ℕ
κ':ℕ → ℝ≥0 := BD.κ' κ
_inst_κ':package.adept BD κ κ'
Λ:Type
_inst_Λ:polyhedral_lattice Λ
S:Type
_inst_S:fintype S
V:SemiNormedGroup
_inst_V:normed_with_aut r V
((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact (k κ' m) (K r r' BD κ' m) m
  (c₀ r r' BD κ κ' m (PolyhedralLattice.of Λ)),
  apply thm95'
BD:package
r, r':ℝ≥0
_inst_1:fact (0 < r)
_inst_2:fact (0 < r')
_inst_3:fact (r < r')
_inst_4:fact (r < 1)
_inst_5:fact (r' < 1)
κ:ℕ → ℝ≥0
_inst_6:BD.data.very_suitable r r' κ
_inst_7:∀ (i : ℕ), fact (0 < κ i)
∀ (m : ℕ),
  ∃ (k K : ℝ≥0) [_inst_8 : fact (1 ≤ k)],
    ∀ (Λ : Type) [_inst_9 : polyhedral_lattice Λ],
      ∃ (c₀ : ℝ≥0),
        ∀ (S : Type) [_inst_10 : fintype S] (V : SemiNormedGroup) [_inst_11 : normed_with_aut r V],
          ((BD.data.system κ r V r').obj (op (Hom Λ (Mbar r' S)))).is_weak_bounded_exact k K m c₀end