/-
Copyright (c) 2019 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl

Giry monad: `measure` is a monad in the category of `measurable_space` and `measurable` functions.
-/
import measure_theory.integration data.sum
noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

open classical set lattice filter

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ε : Type*}

namespace measure_theory

namespace measure

variables [measurable_space α] [measurable_space β]

/-- Measurability structure on `measure`: Measures are measurable w.r.t. all projections -/
instance : measurable_space (measure α) :=
⨆ (s : set α) (hs : is_measurable s), (borel ennreal).comap (λμ, μ s)

lemma measurable_coe {s : set α} (hs : is_measurable s) : measurable (λμ : measure α, μ s) :=
measurable_space.comap_le_iff_le_map.1 $ le_supr_of_le s $ le_supr_of_le hs $ le_refl _

lemma measurable_of_measurable_coe (f : β → measure α)
  (h : ∀(s : set α) (hs : is_measurable s), measurable (λb, f b s)) :
  measurable f :=
supr_le $ assume s, supr_le $ assume hs, measurable_space.comap_le_iff_le_map.2 $
  by rw [measurable_space.map_comp]; exact h s hs

lemma measurable_map (f : α → β) (hf : measurable f) :
  measurable (λμ : measure α, μ.map f) :=
measurable_of_measurable_coe _ $ assume s hs,
  suffices measurable (λ (μ : measure α), μ (f ⁻¹' s)),
    by simpa [map_apply, hs, hf],
  measurable_coe (hf.preimage hs)

lemma measurable_dirac :
  measurable (measure.dirac : α → measure α) :=
measurable_of_measurable_coe _ $ assume s hs,
  begin
    simp [hs, lattice.supr_eq_if],
    exact measurable_const.if hs measurable_const
  end

lemma measurable_integral (f : α → ennreal) (hf : measurable f) :
  measurable (λμ : measure α, μ.integral f) :=
suffices measurable (λμ : measure α,
  (⨆n:ℕ, @simple_func.integral α { μ := μ } (simple_func.eapprox f n)) : _ → ennreal),
begin
  convert this,
  funext μ,
  exact @lintegral_eq_supr_eapprox_integral α {μ := μ} f hf
end,
measurable.supr $ assume n,
  begin
    dunfold simple_func.integral,
    refine measurable_finset_sum (simple_func.eapprox f n).range _,
    assume i,
    refine ennreal.measurable_mul measurable_const _,
    exact measurable_coe ((simple_func.eapprox f n).preimage_measurable _)
  end

/-- Monadic join on `measure` in the category of measurable spaces and measurable
functions. -/
def join (m : measure (measure α)) : measure α :=
measure.of_measurable
  (λs hs, m.integral (λμ, μ s))
  (by simp [integral])
  begin
    assume f hf h,
    simp [measure_Union h hf],
    apply lintegral_tsum,
    assume i, exact measurable_coe (hf i)
  end

@[simp] lemma join_apply {m : measure (measure α)} :
  ∀{s : set α}, is_measurable s → join m s = m.integral (λμ, μ s) :=
measure.of_measurable_apply

lemma measurable_join : measurable (join : measure (measure α) → measure α) :=
measurable_of_measurable_coe _ $ assume s hs,
  by simp [hs]; exact measurable_integral _ (measurable_coe hs)

lemma integral_join {m : measure (measure α)} {f : α → ennreal} (hf : measurable f) :
  integral (join m) f = integral m (λμ, integral μ f) :=
begin
  transitivity,
  apply lintegral_eq_supr_eapprox_integral,
  { exact hf },
  have : ∀n x,
    @volume α { μ := join m} (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}) =
    m.integral (λμ, @volume α { μ := μ } ((⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}))) :=
    assume n x, join_apply (simple_func.measurable_sn _ _),
  conv {
    to_lhs,
    congr,
    funext,
    rw [simple_func.integral] },
  simp [this],
  transitivity,
  have : ∀(s : ℕ → finset ennreal) (f : ℕ → ennreal → measure α → ennreal)
    (hf : ∀n r, measurable (f n r)) (hm : monotone (λn μ, (s n).sum (λ r, r * f n r μ))),
    (⨆n:ℕ, (s n).sum (λr, r * integral m (f n r))) =
    integral m (λμ, ⨆n:ℕ, (s n).sum (λr, r * f n r μ)),
  { assume s f hf hm,
    symmetry,
    transitivity,
    apply lintegral_supr,
    { exact assume n,
        measurable_finset_sum _ (assume r, ennreal.measurable_mul measurable_const (hf _ _)) },
    { exact hm },
    congr, funext n,
    transitivity,
    apply lintegral_finset_sum,
    { exact assume r, ennreal.measurable_mul measurable_const (hf _ _) },
    congr, funext r,
    apply lintegral_const_mul,
    exact hf _ _ },
  specialize this (λn, simple_func.range (simple_func.eapprox f n)),
  specialize this
    (λn r μ, @volume α { μ := μ } (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {r})),
  refine this _ _; clear this,
  { assume n r,
    apply measurable_coe,
    exact simple_func.measurable_sn _ _ },
  { change monotone (λn μ, @simple_func.integral α {μ := μ} (simple_func.eapprox f n)),
    assume n m h μ,
    apply simple_func.integral_le_integral,
    apply simple_func.monotone_eapprox,
    assumption },
  congr, funext μ,
  symmetry,
  apply lintegral_eq_supr_eapprox_integral,
  exact hf
end

/-- Monadic bind on `measure`, only works in the category of measurable spaces and measurable
functions. When the function `f` is not measurable the result is not well defined. -/
def bind (m : measure α) (f : α → measure β) : measure β := join (map f m)

@[simp] lemma bind_apply {m : measure α} {f : α → measure β} {s : set β}
  (hs : is_measurable s) (hf : measurable f) : bind m f s = m.integral (λa, f a s) :=
by rw [bind, join_apply hs, integral_map (measurable_coe hs) hf]

lemma measurable_bind' {g : α → measure β} (hg : measurable g) : measurable (λm, bind m g) :=
measurable.comp (measurable_map _ hg) measurable_join

lemma integral_bind {m : measure α} {g : α → measure β} {f : β → ennreal}
  (hg : measurable g) (hf : measurable f) :
  integral (bind m g) f = integral m (λa, integral (g a) f) :=
begin
  transitivity,
  exact integral_join hf,
  exact integral_map (measurable_integral _ hf) hg
end

lemma bind_bind {γ} [measurable_space γ] {m : measure α} {f : α → measure β} {g : β → measure γ}
  (hf : measurable f) (hg : measurable g) :
  bind (bind m f) g = bind m (λa, bind (f a) g) :=
measure.ext $ assume s hs,
begin
  rw [bind_apply hs hg, bind_apply hs (hf.comp $ measurable_bind' hg), integral_bind hf],
  { congr, funext a,
    exact (bind_apply hs hg).symm },
  exact hg.comp (measurable_coe hs)
end

lemma bind_dirac {f : α → measure β} (hf : measurable f) (a : α) : bind (dirac a) f = f a :=
measure.ext $ assume s hs, by rw [bind_apply hs hf, integral_dirac a (hf.comp (measurable_coe hs))]

lemma dirac_bind {m : measure α} : bind m dirac = m :=
measure.ext $ assume s hs,
begin
  rw [bind_apply hs measurable_dirac],
  simp [dirac_apply _ hs],
  transitivity,
  apply lintegral_supr_const,
  assumption,
  exact one_mul _
end

end measure

end measure_theory


import analysis.inner_product_space.pi_L2
import topology.paracompact

--OUTPUT 1
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$.
  assume h1 : (is_open_cover (euclidean_space ℝ (fin n))),
  let A := is_open_cover_iff.mp h1,
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$.
  -- First, we define a collection of pen balls.
  -- Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$
  -- centered at 0.
  let B0 : set (euclidean_space ℝ (fin n)) := set.univ,
  have h2 : ∀ (m : ℕ), ∃ (B : set (euclidean_space ℝ (fin n))), is_open B ∧ ∀ (x : euclidean_space ℝ (fin n)), x ∈ B ↔ ∀ (i : fin n), abs (x.val i) < m, from
  begin
    assume m : ℕ,
    use {x : euclidean_space ℝ (fin n) | ∀ (i : fin n), abs (x.val i) < m},
    obviously,
  end,
  have h3 : ∀ (m : ℕ), is_open (some (h2 m)), from
  begin
    assume m : ℕ,
    have h4 : ∃ (B : set (euclidean_space ℝ (fin n))), is_open B ∧ ∀ (x : euclidean_space ℝ (fin n)), x ∈ B ↔ ∀ (i : fin n), abs (x.val i) < m, from h2 m,
    show is_open (some (h2 m)), from classical.some_spec h4,
  end,
  have h5 : ∀ (m : ℕ), ∀ (x : euclidean_space ℝ (fin n)), x ∈ some (h2 m) ↔ ∀ (i : fin n), abs (x.val i) < m, from
  begin
    assume m : ℕ,
    assume x : euclidean_space ℝ (fin n),
    have h6 : ∃ (B : set (euclidean_space ℝ (fin n))), is_open B ∧ ∀ (x : euclidean_space ℝ (fin n)), x ∈ B ↔ ∀ (i : fin n), abs (x.val i) < m, from h2 m,
    show x ∈ some (h2 m) ↔ ∀ (i : fin n), abs (x.val i) < m, from classical.some_spec h6,
  end,
  let B : ℕ → set (euclidean_space ℝ (fin n)) := λ m, some (h2 m),
  -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem,
  -- so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$,
  -- and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$).
  let Cm : ℕ → set (set (euclidean_space ℝ (fin n))) := λ m,
    begin
      let Bm : set (euclidean_space ℝ (fin n)) := B m,
      let Bm_bar : set (euclidean_space ℝ (fin n)) :=
        {x : euclidean_space ℝ (fin n) | ∃ (m : ℕ), x ∈ B m},
      have h6 : compact Bm_bar, from
        compact_def.compact_univ.mono
        (by intros x hx; exact ⟨0, by simp [h5] at hx; exact hx⟩),
      let A' : set (euclidean_space ℝ (fin n)) := {x : euclidean_space ℝ (fin n) | ∃ (U : set (euclidean_space ℝ (fin n))), (U ∈ A) ∧ (x ∈ U)},
      have h7 : ∀ (m : ℕ), Bm_bar ⊆ A', from
      begin
        assume m : ℕ,
        assume x : euclidean_space ℝ (fin n),
        assume hx : x ∈ Bm_bar,
        have h8 : ∃ (m : ℕ), x ∈ B m, from hx,
        have h9 : ∃ (m : ℕ), ∀ (i : fin n), abs (x.val i) < m, from
        begin
          assume m : ℕ,
          assume h : x ∈ B m,
          show ∀ (i : fin n), abs (x.val i) < m, from h,
        end,
        have h10 : ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m, from
        begin
          assume m : ℕ,
          assume h : ∀ (i : fin n), abs (x.val i) < m,
          show ∃ (i : fin n), abs (x.val i) < m, from
            begin
              use (0 : fin n),
              show abs (x.val (0 : fin n)) < m, from h (0 : fin n),
            end,
        end,
        have h11 : ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m, from
        begin
          assume m : ℕ,
          assume h : ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m,
          show ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m, from
            begin
              use m,
              use (0 : fin n),
              show abs (x.val (0 : fin n)) < m ∧ ∀ (i : fin n), abs (x.val i) < m, from
                begin
                  split,
                  show abs (x.val (0 : fin n)) < m, from (some h).right.left,
                  show ∀ (i : fin n), abs (x.val i) < m, from
                    begin
                      assume i : fin n,
                      show abs (x.val i) < m, from (some h).right.right,
                    end,
                end,
            end,
        end,
        have h12 : ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m, from
        begin
          assume m : ℕ,
          assume h : ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m,
          show ∃ (m : ℕ), ∃ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m ∧ ∀ (i : fin n), abs (x.val i) < m, from
            begin
              use m,
              use (0 : fin n),
              show abs (x.val (0 : fin n)) < m ∧ ∀ (i : fin n), abs (x.val i) < m ∧
end --Needs more than 2000 tokens!

--OUTPUT 2
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$
  assume A : set (opens (euclidean_space ℝ (fin n))),
  have h1 : is_open_cover A, from sorry,
  have h2 : is_open_cover (A ∩ (set.Ico (0 : ℝ^(fin n)) (1 : ℝ^(fin n)))), from sorry,
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$
  have h3 : paracompact_space (euclidean_space ℝ (fin 1)), from paracompact_space_euclidean_space 1,
  have h4 : is_open_cover (h3.paracompact_refinement A), from h3.paracompact_refinement_is_open_cover A,

  -- let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$ centered at 0
  have h5 : ∃ m : ℕ, ∀ x : ℝ^(fin n), ∀ B : set (euclidean_space ℝ (fin n)), B ∈ h3.paracompact_refinement A → (∃ y : ℝ^(fin 1), y ∈ B) → x ∈ B → ∥x∥ ≤ m, from sorry,
  have h6 : ∃ m : ℕ, ∀ x : ℝ^(fin n), ∀ B : set (euclidean_space ℝ (fin n)), B ∈ h3.paracompact_refinement A → (∃ y : ℝ^(fin 1), y ∈ B) → x ∈ B → ∥x∥ ≤ m + 1, from sorry,
  have h7 :  ∀ B : set (euclidean_space ℝ (fin n)), B ∈ h3.paracompact_refinement A → (∃ y : ℝ^(fin 1), y ∈ B) → ∃ m : ℕ, ∀ x : ℝ^(fin n), x ∈ B → ∥x∥ ≤ m, from sorry,

  -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem, so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$, and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$). So $\mathcal{C} = \bigcup_{m = 0}^{\infty} \mathcal{C}_m$ is an open refinement of $\mathcal{A}$.
  -- Note that $\mathcal{C}$ covers $\mathbb{R}^n$ since for any $x \in \mathbb{R}^n$, there is a smallest $m \in \mathbb{N}$ such that $x \in \Bar{B_{m}}$ (namely, some $m$ where $\rVert x \lVert \leq m \leq \rVert x \lVert + 1$), and so $x$ is an element of $\mathcal{C}_m$.
  -- Now collection $\mathcal{C}$ is locally finite since for given $x \in \mathbb{R}^n$, neighborhood $B_m$ intersects only finitely many elements of $\mathcal{C}$, namely those elements in collection $\mathcal{C}_1 \cup \mathcal{C}_2 \cup \cdots \mathcal{C}_m$. So $\mathcal{C}$ is a locally finite open refinement of $\mathcal{A}$ that covers $\mathbb{R}^n$, hence $\mathbb{R}^n$ is paracompact.
  show paracompact_space (euclidean_space ℝ (fin n)), from sorry,
end

--OUTPUT 3
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$.
  assume A : set (euclidean_space ℝ (fin n)),
  assume hA : is_open_cover A,
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$.
  let C := ⋃ (m : ℕ), (⋃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A) (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), set.inter_subset_left (set.inter_subset_right (set.inter_subset_left (set.diff_subset_iff.mpr (begin
    show (set.diff_eq_empty (b ∩ {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m}, {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1})),
    assume x : euclidean_space ℝ (fin n),
    assume hx : x ∈ b ∩ {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m},
    have h2 : x ∈ b, from hx.left,
    have h3 : x ∈ {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m}, from hx.right,
    have h4 : ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m), from h3,
    have h5 : ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1), from by {
      have h6 : ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m, from h4.right.right,
      have h7 : ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1, from by {
        have h8 : dist x b ≤ m - 1, from le_of_lt (begin
          show dist x b < m - 1 + 1,
          rw ← add_one,
          rw add_comm,
          apply nat.lt_succ_iff.mpr,
          apply h6.right,
        end),
        use b,
        split,
        exact h6.left,
        exact h8,
      },
      use h4.left,
      use h4.right.left,
      exact h7,
    },
    have h8 : x ∈ {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1}, from h5,
    show x ∈ b ∩ {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1}, from ⟨h2,h8⟩,
  end)) h1) h) h),
  have hC : is_open_cover C, from by {
    have h3 : ∀ m : ℕ, ∀ a : euclidean_space ℝ (fin n), ∀ h : a ∈ A, ∀ b : euclidean_space ℝ (fin n), ∀ h1 : b ∈ A, is_open (set.inter (set.inter (set.inter (set.diff b {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m}) {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1}) (set.inter b a))),
    have h4 : ∀ m : ℕ, is_open (⋃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A) (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), set.inter (set.inter (set.inter (set.diff b {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m}) {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1}) (set.inter b a))),
    have h5 : is_open (⋃ (m : ℕ), (⋃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A) (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), set.inter (set.inter (set.inter (set.diff b {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m}) {x : euclidean_space ℝ (fin n) | ∃ (a : euclidean_space ℝ (fin n)) (h : a ∈ A ∧ ∃ (b : euclidean_space ℝ (fin n)) (h1 : b ∈ A), dist x b ≤ m - 1}) (set.inter b a)))),
    show is_open_cover C, from by {
      apply is_open_cover.union h5,
      have h6 : ∀ m : ℕ, is_open_cover (⋃ (a : euclidean_space ℝ (fin n)) (
end --Needs more than 2000 tokens!

--OUTPUT 4
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$.
  assume A : set (euclidean_space ℝ (fin n)),
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$.
  obtain ⟨C,hC⟩ : ∃ C : set (euclidean_space ℝ (fin n)),
    locally_finite_open_refinement A C ∧ covers (euclidean_space ℝ (fin n)) C, from by {
      -- First, we define a collection of pen balls.
      have B : set (euclidean_space ℝ (fin n)), from by {
        -- Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$
        -- centered at 0.
        have B0 : set (euclidean_space ℝ (fin n)), from by {
          use ∅, use ⟨0,by apply zero_lt_one⟩, obviously, },
        have Bm : Π m : ℕ, set (euclidean_space ℝ (fin n)), from by {
          assume (m : ℕ),
          use {x : euclidean_space ℝ (fin n) | ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0),
          use m, use ⟨0,by apply zero_lt_one⟩,
          use (0 : euclidean_space ℝ (fin n)), use ⟨rfl,rfl⟩, obviously, },
        have B : set (euclidean_space ℝ (fin n)), from by {
          use {x | ∃ m : ℕ, x ∈ Bm m}, use B0, obviously, },
        show set (euclidean_space ℝ (fin n)), from B, },
      -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem, so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$, and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$).
      have Cm : Π m : ℕ, set (euclidean_space ℝ (fin n)), from by {
        assume (m : ℕ),
        have hBm : is_open Bm m, from by {
          use {x : euclidean_space ℝ (fin n) | ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0),
          use m, use ⟨0,by apply zero_lt_one⟩,
          use (0 : euclidean_space ℝ (fin n)), use ⟨rfl,rfl⟩, obviously, },
        have hBm_bar : compact (bar Bm m), from by {
          use Bm m, use hBm,
          -- Let $U_i$ be open in $\mathcal{A}$.
          assume U : set (euclidean_space ℝ (fin n)),
          assume hU : is_open U,
          assume hU_cover : ∀ x ∈ bar Bm m, x ∈ U,
          -- Then $U_i$ is open in $\mathbb{R}^n$, and $U_i$ covers $\Bar{B_m}$, so $U_i$ contains a finite subcovering by Heine-Borel.
          have hU_open : ∀ x ∈ U, ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from by {
            assume (x : euclidean_space ℝ (fin n)) (hx : x ∈ U),
            have hx_dist : ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from by {
              have hx_cover : x ∈ bar Bm m, from by {
                use Bm m, use hBm,
                apply hU_cover, exact hx, },
              have hx_mem : x ∈ Bm m, from by {
                have hx_mem : ∃ m : ℕ, x ∈ Bm m, from by {
                  use m, exact hx_cover, },
                cases hx_mem with m hx_mem,
                show x ∈ Bm m, from hx_mem, },
              have hx_dist : ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from by {
                have hx_dist : ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from by {
                  have hx_dist : ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from by {
                    cases hx_mem with r hr hx_mem,
                    cases hx_mem with hx_mem x0,
                    cases hx_mem with hx_mem hx_mem_eq,
                    use r, use hr, use ⟨x0, hx_mem_eq, hx_mem⟩, },
                  show ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from hx_dist, },
                show ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from hx_dist, },
              show ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from hx_dist, },
            show ∃ (r : ℝ) (h : 0 < r) (h2 : ∃ (x0 : euclidean_space ℝ (fin n)), x0 = (0 : euclidean_space ℝ (fin n)) ∧ r = dist x x0), from hx_dist, },
          have hU_cover : ∀ x ∈ bar Bm m, ∃ (r :
end --Needs more than 2000 tokens!

--OUTPUT 5
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$
  assume (A : set (euclidean_space ℝ (fin n))) (hA : is_open_cover A),

  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$
  have h1 : ∃ (C : set (euclidean_space ℝ (fin n))) (hC : is_open_refinement C A),
    (∀ (x : euclidean_space ℝ (fin n)), (∃ (m : ℕ), ∀ (y : euclidean_space ℝ (fin n)),
    (y ∈ C) → (dist x y < m) → (dist x y = 0)) → (∃ (m : ℕ), ∃ (z : euclidean_space ℝ (fin n)),
    (x ∈ z) ∧ (z ∈ C) ∧ (∀ (y : euclidean_space ℝ (fin n)), (y ∈ C) → (dist x y < m) → (dist x y = 0)))),
  {
    -- First, we define a collection of pen balls.
    -- Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$
    -- centered at 0.
    let B : ℕ → set (euclidean_space ℝ (fin n)) := λ (m : ℕ), {x : euclidean_space ℝ (fin n) | ∃ (e : fin n),
      dist x (0 : euclidean_space ℝ (fin n)) < m},
    have hB0 : B 0 = ∅, from eq.refl (B 0),
    have hBm : ∀ (m : ℕ), B m = {x : euclidean_space ℝ (fin n) | ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m},
    from by {
      assume m : ℕ,
      have h1 : ∀ (x : euclidean_space ℝ (fin n)), (∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m) →
        x ∈ B m, from
        assume (x : euclidean_space ℝ (fin n)) (hx : ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m),
        have h1 : ∀ (y : euclidean_space ℝ (fin n)), (y ∈ B m) → (∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m),
        from by {
          assume (y : euclidean_space ℝ (fin n)) (hy : y ∈ B m),
          have h1 : ∃ (e : fin n), dist y (0 : euclidean_space ℝ (fin n)) < m, from by {exact hy,},
          from h1,
        },
        have h2 : ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {exact hx,},
        show x ∈ B m, from by {
          apply set.mem_of_mem_image (λ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m),
          apply exists.intro m,
          apply exists.intro h2,
          apply exists.intro rfl,
        },
      have h2 : ∀ (x : euclidean_space ℝ (fin n)), (x ∈ B m) → (∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m),
      from by {
        assume (x : euclidean_space ℝ (fin n)) (hx : x ∈ B m),
        have h1 : ∀ (y : euclidean_space ℝ (fin n)), (y ∈ B m) → (∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m),
        from by {
          assume (y : euclidean_space ℝ (fin n)) (hy : y ∈ B m),
          have h1 : ∃ (e : fin n), dist y (0 : euclidean_space ℝ (fin n)) < m, from by {exact hy,},
          show ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {
            have h2 : ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {exact hx,},
            show ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {exact h2,},
          },
        },
        have h2 : ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {exact hx,},
        show ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m, from by {exact h2,},
      },
      show B m = {x : euclidean_space ℝ (fin n) | ∃ (e : fin n), dist x (0 : euclidean_space ℝ (fin n)) < m}, from
        set.ext h1 h2,
    },

    -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem, so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$, and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$).
    have hBm_bar : ∀ (m : ℕ), is_compact (closure (B m)), from by {
      assume m : ℕ,
      have h1 : ∃ (hBm : set (euclidean_space ℝ (fin n))), ((B m) = hBm) ∧ is_compact (closure hBm), from by {
        have h1 : ∃ (hBm : set (euclidean_space ℝ (fin n))), ((B m) = hBm) ∧
          (∀ (x : euclidean_space ℝ (fin n)), ∀ (y : euclidean_space ℝ (fin n)),
          (y ∈ closure hBm) → (dist x y < m) → (dist x y = 0)), from by {
          have h1 : ∃ (hBm : set (euclidean_space ℝ (fin n))), ((B m) = hBm) ∧
            (∀ (x : euclidean_space ℝ (fin n)), ∀ (y : euclidean_space ℝ (fin n)),
            (y ∈ hBm) → (dist x y < m) → (dist x y = 0)), from by {
            have hBm : set (euclidean_space ℝ (fin n)) := B m,
            have h1 : ∀ (x : euclidean_space ℝ (fin n)), ∀ (y : euclidean_space ℝ (fin n)),
              (y ∈ hBm) → (dist x y < m) → (dist x y = 0), from by {
              assume (x : euclidean_space ℝ (fin n
end --Needs more than 2000 tokens!

--OUTPUT 6
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$.
  assume (U : set (euclidean_space ℝ (fin n))) (hU : (⋃₀ U) = ⊤),
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$.
  have h1 : ∃ (V : set (euclidean_space ℝ (fin n))) (hV : (⋃₀ V) = ⊤) (hV_lf : locally_finite V),
    from by {
      -- First, we define a collection of pen balls.
      -- Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$ centered at 0.
      let B_0 : set (euclidean_space ℝ (fin n)) := {(0 : ℝ^(fin n))},
      let B_m : set (euclidean_space ℝ (fin n)) := {x : ℝ^(fin n) | ∃ n : ℕ, n < m ∧ ∃ (y : ℝ^(fin n)), y = x},

      -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem,
      -- so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$, and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$).
      let C_0 : set (euclidean_space ℝ (fin n)) := {(0 : ℝ^(fin n))},
      let C_m : set (euclidean_space ℝ (fin n)) := {x : ℝ^(fin n) | ∃ n : ℕ, n < m ∧ x ∈ ⋃₀ (U ∩ (⊤ \ B_m))},

      -- So $\mathcal{C} = \bigcup_{m = 0}^{\infty} \mathcal{C}_m$ is an open refinement of $\mathcal{A}$.
      let C : set (euclidean_space ℝ (fin n)) := ⋃₀ (C_0 ∪ C_1 ∪ C_2 ∪ C_3 ∪ C_4),
      have h2 : (⋃₀ C) = ⊤, from by {unfold C, apply set.sUnion_union, apply set.sUnion_union, exact hU},
      have h3 : locally_finite C, from by {
        unfold C, unfold C_0, unfold C_1, unfold C_2, unfold C_3, unfold C_4,
        unfold B_0, unfold B_1, unfold B_2, unfold B_3, unfold B_4,
        have h4 : ∀ (x : ℝ^(fin n)), finite {y : ℝ^(fin n) | ∃ n : ℕ, n < 1 ∧ y ∈ ⋃₀ (U ∩ (⊤ \ B_1))}, from by {
            assume x : ℝ^(fin n),
            have h5 : compact (⋃₀ (U ∩ (⊤ \ B_1))), from by {unfold B_1, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx, apply set.compact_Union, intros x hx
end --Needs more than 2000 tokens!

--OUTPUT 7
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$
  assume (A : set (euclidean_space ℝ (fin n))),
  assume hA : is_open_cover A,
  -- We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$
  let B0 : set (euclidean_space ℝ (fin n)) := ∅,
  let Bm : ℕ → set (euclidean_space ℝ (fin n)) := λ m : ℕ, {x ∈ euclidean_space ℝ (fin n) | ∃ (y : euclidean_space ℝ (fin n)),
    x = y ∧ ∀ i : fin n, abs (y.val i) ≤ m},
  let Bmbar : ℕ → set (euclidean_space ℝ (fin n)) := λ m : ℕ, {x ∈ euclidean_space ℝ (fin n) | ∃ (y : euclidean_space ℝ (fin n)),
    x = y ∧ ∀ i : fin n, abs (y.val i) ≤ m},
  let Cm : ℕ → set (euclidean_space ℝ (fin n)) := λ m : ℕ, {x ∈ euclidean_space ℝ (fin n) | ∃ (A' ∈ A),
    ∃ (B ∈ Bmbar m) ∩ (euclidean_space ℝ (fin n) \ Bm (m-1)), x ∈ A' ∩ B},
  let C : set (euclidean_space ℝ (fin n)) := {x ∈ euclidean_space ℝ (fin n) | ∃ (m : ℕ) (x' ∈ Cm m), x = x'},
  have h1 : (∀ (m : ℕ), Bm m ∈ opens (euclidean_space ℝ (fin n))), from assume m : ℕ, by {
    use Bm m,
      -- Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem
    have h1 : is_compact (Bmbar m), from by {
      -- Let $B_{m + 1} = \bigcup_{r = 0}^{m + 1} B_r$
      let Bmplus1 : set (euclidean_space ℝ (fin n)) := {x ∈ euclidean_space ℝ (fin n) | ∃ (m' : ℕ) (y : euclidean_space ℝ (fin n)),
        x = y ∧ m' ≤ m + 1 ∧ ∀ i : fin n, abs (y.val i) ≤ m'},
      have h1 : Bmbar m = Bmplus1, from set.ext $ assume x : euclidean_space ℝ (fin n), by {
        split; assume hx : x ∈ Bmbar m,
        -- Then $x \in B_m$
        show x ∈ Bmplus1, from by {
          -- So there exists $y \in \mathbb{R}^n$ such that $x = y$ and $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
          have h1 : ∃ (y : euclidean_space ℝ (fin n)), x = y ∧ ∀ i : fin n, abs (y.val i) ≤ m, from hx,
          obtain ⟨y, h2, h3⟩ : ∃ (y : euclidean_space ℝ (fin n)), x = y ∧ ∀ i : fin n, abs (y.val i) ≤ m, from h1,
          -- Then $x \in B_{m + 1}$
          show x ∈ Bmplus1, from by {
            -- Hence $m \in \mathbb{N}$ and $y \in \mathbb{R}^n$ and $x = y$ and $m \leq m + 1$ and $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
            use m, use y, split, exact h2, split, exact nat.le_add_right m 1, exact h3,
          },
        },
        -- Then $x \in B_{m + 1}$
        show x ∈ Bmbar m, from by {
          -- Hence $m' \in \mathbb{N}$ and $y \in \mathbb{R}^n$ and $x = y$ and $m' \leq m + 1$ and $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m'$
          obtain ⟨m', y, h1, h2, h3⟩ : ∃ (m' : ℕ) (y : euclidean_space ℝ (fin n)), x = y ∧ m' ≤ m + 1 ∧ ∀ i : fin n, abs (y.val i) ≤ m', from hx,
          -- Then $x \in B_m$
          show x ∈ Bmbar m, from by {
            -- Hence $y \in \mathbb{R}^n$ and $x = y$ and $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
            use y, split, exact h1, exact h3,
          },
        },
      },
      have h2 : is_compact Bmplus1, from by apply_instance,
      show is_compact (Bmbar m), from by {
        rw h1,
        exact h2,
      },
    },
    have h2 : Bmbar m = closure (Bm m), from set.ext $ assume x : euclidean_space ℝ (fin n), by {
      split; assume hx : x ∈ Bmbar m,
      -- Then $x \in \Bar{B_m}$
      show x ∈ closure (Bm m), from by {
        -- Hence there exists $y \in \mathbb{R}^n$ such that $x = y$ and $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
        obtain ⟨y, h1, h2⟩ : ∃ (y : euclidean_space ℝ (fin n)), x = y ∧ ∀ i : fin n, abs (y.val i) ≤ m, from hx,
        -- Then $x \in \Bar{B_m}$
        show x ∈ closure (Bm m), from by {
          -- Then $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
          have h3 : ∀ (i : fin n), abs (y.val i) ≤ m, from h2,
          -- Then $\forall i \in \set{x_1, x_2, \ldots, x_n} : \lVert y \lVert \leq m$
          have h4 : ∀ (i : fin n), abs (y.val i) < m + 1, from assume i : fin n, by {
            -- Hence $\lVert y \lVert \leq m$
            have h4 : abs (y.val i) ≤ m, from h3 i,
            -- Then $\lVert y \lVert < m + 1$
            have h5 : m < m + 1, from by norm_num,
            show abs (y.val i) < m + 1, from lt_of_le_of_lt h4 h5,
          },
          -- Then $y \in B
end --Needs more than 2000 tokens!

--OUTPUT 8
theorem ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
begin
  -- $\mathcal{A}$ is an open covering of $\mathbb{R}^n$
  assume (A : set (euclidean_space ℝ (fin n))) (hA : is_open_cover A),
  -- we construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$
  have h1 : ∃ C : set (euclidean_space ℝ (fin n)),
    (∀x : euclidean_space ℝ (fin n), ∃ U : set (euclidean_space ℝ (fin n)), x ∈ U ∧ U ∈ C) ∧
    (∀ x : euclidean_space ℝ (fin n), ∃ (U : set (euclidean_space ℝ (fin n))) (V : set (euclidean_space ℝ (fin n))),
      x ∈ U ∧ U ∈ C ∧ x ∈ V ∧ V ∈ C → U = V), from
  begin
    -- $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$ centered at 0
    let B_0 : set (euclidean_space ℝ (fin n)) := {x : euclidean_space ℝ (fin n) | x = (0 : euclidean_space ℝ (fin n))},
    let B_m : set (euclidean_space ℝ (fin n)) := {x : euclidean_space ℝ (fin n) | ∃ (r : ℝ) (h : 0 < r), ∀ i : fin n, abs (x.val i) < r},
    have h1 : ∀ m : ℕ, B_m ⊆ set.univ, from assume (m : ℕ), by {
      assume x : euclidean_space ℝ (fin n),
      assume h1 : x ∈ B_m,
      show x ∈ set.univ, from by {rw set.univ_def,},
    },
    have h2 : ∀ m : ℕ, is_open (B_m), from assume (m : ℕ), by {
      apply is_open_ball,
    },
    have h3 : ∀ m : ℕ, is_open (set.univ \ B_m), from assume (m : ℕ), by {
      apply is_open_compl,
      apply h2,
    },
    have h4 : ∀ m : ℕ, ∃ C_m : set (euclidean_space ℝ (fin n)), (∀x : euclidean_space ℝ (fin n), ∃ U : set (euclidean_space ℝ (fin n)), x ∈ U ∧ U ∈ C_m) ∧ (∀ x : euclidean_space ℝ (fin n), ∃ (U : set (euclidean_space ℝ (fin n))) (V : set (euclidean_space ℝ (fin n)), x ∈ U ∧ U ∈ C_m ∧ x ∈ V ∧ V ∈ C_m → U = V), from assume (m : ℕ), by {
      -- $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem, so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$
      have h4 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h5 : is_closed (set.closure (B_m)), from compact_iff_closed_of_open.mpr (compact_of_is_open (h2 m)),
      have h6 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h7 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h8 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h9 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h10 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h11 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h12 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h13 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h14 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h15 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h16 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h17 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h18 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h19 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h20 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h21 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h22 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h23 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h24 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h25 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h26 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h27 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),
      have h28 : is_compact (set.closure (B_m)), from compact_iff_closed_of_open.mp (compact_of_is_open (h2 m)),

end --Needs more than 2000 tokens!

/- FEW SHOT PROMPTS TO CODEX(START)
/--`theorem`
Power Set is Closed under Intersection
Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
`proof`
Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.
{{qed}}
-/
theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ 𝒫 S, (A ∩ B) ∈ 𝒫 S :=
begin
  -- $A$ and $B$ are sets. $A$ and $B$ belong to power set of $S$
  assume (A : set α) (hA : A ∈ 𝒫 S) (B : set α) (hB : B ∈ 𝒫 S),
  -- Then $A ⊆ S$ and $B ⊆ S$, by power set definition
  have h1 : (A ⊆ S) ∧ (B ⊆ S), from by {split,apply set.subset_of_mem_powerset,exact hA,apply set.subset_of_mem_powerset,exact hB},
  -- Then $(A ∩ B) ⊆ A$, by intersection of set is a subset
  have h2 : (A ∩ B) ⊆ A, from by apply set.inter_subset_left,
  -- Then $(A ∩ B) ⊆ S$, by subset relation is transitive
  have h3 : (A ∩ B) ⊆ S, from by {apply set.subset.trans h2 h1.left},
  -- Hence $(A ∩ B) ∈  𝒫 S$, by power set definition
  show (A ∩ B) ∈  𝒫 S, from by {apply set.mem_powerset h3},
end

/--`theorem`
Square of Sum
 :$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$
`proof`
Follows from the distribution of multiplication over addition:

{{begin-eqn}}
{{eqn | l = \left({x + y}\right)^2
      | r = \left({x + y}\right) \cdot \left({x + y}\right)
}}
{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x^2 + 2xy + y^2
      | c =
}}
{{end-eqn}}
{{qed}}
-/
theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2) :=
begin
  -- expand the power
  calc (x + y)^2 = (x+y)*(x+y) : by rw sq
  -- distributive property of multiplication over addition gives:
  ... = x*(x+y) + y*(x+y) : by rw add_mul
  -- applying the above property further gives:
  ... = x*x + x*y + y*x + y*y : by {rw [mul_comm x (x+y),mul_comm y (x+y)], rw [add_mul,add_mul], ring}
  -- rearranging the terms using commutativity and adding gives:
  ... = x^2 + 2*x*y + y^2 : by {repeat {rw ← sq}, rw mul_comm y x, ring}
end

/--`theorem`
Identity of Group is Unique
Let $\struct {G, \circ}$ be a group. Then there is a unique identity element $e \in G$.
`proof`
From Group has Latin Square Property, there exists a unique $x \in G$ such that:
:$a x = b$

and there exists a unique $y \in G$ such that:
:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:
:$a x = a$

and there exists a unique $y \in G$ such that:
:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.
{{qed}}
-/
theorem group_identity_unique {G : Type*} [group G] : ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a :=
begin
  -- Group has Latin Square Property
  have h1 : ∀ a b : G, ∃! x : G, a * x = b, from by {
    assume a b : G, use a⁻¹ * b, obviously, },
  have h2 : ∀ a b : G, ∃! y : G, y * a = b, from by {
    assume a b : G, use b * a⁻¹, obviously, },

  -- Setting $b = a$, this becomes:
  have h3 : ∀ a : G, ∃! x : G, a * x = a, from
    assume a : G, h1 a a,
  have h4 : ∀ a : G, ∃! y : G, y * a = a, from
    assume a : G, h2 a a,

  -- These $x$ and $y$ are both $(1 : G)$, by definition of identity element
  have h5 : ∀ a : G, classical.some (h3 a).exists = (1 : G), from assume a :G,
    exists_unique.unique (h3 a) (classical.some_spec (exists_unique.exists (h3 a)))
    (mul_one a),
  have h6 : ∀ a : G, classical.some (h4 a).exists = (1 : G), from assume a : G,
    exists_unique.unique (h4 a) (classical.some_spec (exists_unique.exists (h4 a))) (one_mul a),

  show ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a, from by {
    use (1 : G),
    have h7 : ∀ e : G, (∀ a : G, e * a = a ∧ a * e = a) → e = 1, from by {
      assume (e : G) (hident : ∀ a : G, e * a = a ∧ a * e = a),
      have h8 : ∀ a : G, e = classical.some (h3 a).exists, from assume (a : G),
        exists_unique.unique (h3 a) (hident a).right
        (classical.some_spec (exists_unique.exists (h3 a))),
      have h9 : ∀ a : G, e = classical.some (h4 a).exists, from assume (a : G),
        exists_unique.unique (h4 a) (hident a).left
        (classical.some_spec (exists_unique.exists (h4 a))),
      show e = (1 : G), from eq.trans (h9 e) (h6 _),
    },
    exact ⟨by obviously, h7⟩,
  }
end

/--`theorem`
\mathbb{R}^n is paracompact
$\mathbb{R}^n$ is paracompact for all $n$.
`proof`
Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$. We now construct a locally finite open refinement $\mathcal{C}$ of $\mathcal{A}$ that covers $\mathbb{R}^n$. First, we define a collection of pen balls. Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball of radius $m$
centered at 0. Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel theorem, so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$, and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open subset of an element of $\mathcal{A}$). So $\mathcal{C} = \bigcup_{m = 0}^{\infty} \mathcal{C}_m$ is an open refinement of $\mathcal{A}$. Note that $\mathcal{C}$ covers $\mathbb{R}^n$ since for any $x \in \mathbb{R}^n$, there is a smallest $m \in \mathbb{N}$ such that $x \in \Bar{B_{m}}$ (namely, some $m$ where $\rVert x \lVert \leq m \leq \rVert x \lVert + 1$), and so $x$ is an element of $\mathcal{C}_m$. Now collection $\mathcal{C}$ is locally finite since for given $x \in \mathbb{R}^n$, neighborhood $B_m$ intersects only finitely many elements of $\mathcal{C}$, namely those elements in collection $\mathcal{C}_1 \cup \mathcal{C}_2 \cup \cdots \mathcal{C}_m$. So $\mathcal{C}$ is a locally finite open refinement of $\mathcal{A}$ that covers $\mathbb{R}^n$, hence $\mathbb{R}^n$ is paracompact.

QED
-/
theorem  ℝn_paracompact (n : ℕ) : paracompact_space (euclidean_space ℝ (fin n)) :=
FEW SHOT PROMPTS TO CODEX(END)-/


text:
import Mathlib.Tactic.HigherOrder

namespace HigherOrderTest

@[higher_order map_comp_pure]
theorem map_pure' {f : Type u → Type v} [Applicative f] [LawfulApplicative f]
  {α β : Type u} (g : α → β) (x : α) : g <$> (pure x : f α) = pure (g x) := map_pure g x

example {f : Type u → Type v} [Applicative f] [LawfulApplicative f]
    {α β : Type u} (g : α → β) : Functor.map g ∘ (pure : α → f α) = pure ∘ g := by
  apply map_comp_pure

end HigherOrderTest

author: leanprover-community


text:
import .datatypes .blackboard .proof_reconstruction .reconstruction_theorems .radicals .proof_trace

-- TODO: maybe more of this can move to datatypes

namespace polya

meta def approx_prec := 100

private meta def round_rat_to_prec_over (q : ℚ) (prec : ℕ) : ℚ :=
let z' := ((q.num.nat_abs*prec)/q.denom) + 1 in
rat.mk_nat (if q.num > 0 then z' else -z') prec

-- if pf is an inequality, returns a new, implied inequality where the denominator of coeff is at most prec
meta def prod_form_comp_data.round (pfcd : prod_form_comp_data) (prec : ℕ) : prod_form_comp_data :=
if (pfcd.pfc.pf.coeff.denom ≤ prec) || (pfcd.pfc.c = spec_comp.eq) then pfcd
else let ncoeff := round_rat_to_prec_over pfcd.pfc.pf.coeff prec in
⟨{pfcd.pfc with pf := {pfcd.pfc.pf with coeff := ncoeff}}, prod_form_proof.adhoc _ pfcd.prf.sketch (tactic.fail "pfcd.round not implemented yet"), pfcd.elim_list ⟩

private meta def σ := hash_map expr sign_data × hash_map expr (λ e, ineq_info e rat_one)
meta def mul_state := state σ
meta instance mul_state.monad : monad mul_state := state_t.monad
meta instance mul_state.monad_state : monad_state σ mul_state := state_t.monad_state
private meta def inh_sd (e : expr) : inhabited (sign_data e) := ⟨⟨gen_comp.ne, sign_proof.adhoc _ _ (tactic.failed) (tactic.failed)⟩⟩
local attribute [instance] inh_sd

open hash_map

private meta def si (e : expr) : mul_state (sign_data e) :=
(λ hm : σ, hm.1.ifind e) <$> get

private meta def si' (e : expr) : mul_state (option (sign_data e)) :=
(λ hm : σ, hm.1.find e) <$> get

private meta def oi (e : expr) : mul_state (ineq_info e rat_one) :=
(λ hm : σ, hm.2.ifind e) <$> get

-- returns true if the mul_state implies coeff*e c 1
private meta def implies_one_comp (coeff : ℚ) (e : expr) (c : comp) : mul_state bool :=
do ii ← oi e,
   return $ ii.implies_ineq $ ineq.of_comp_and_slope c (slope.some coeff)

private meta def find_comp {lhs rhs} (ii : ineq_info lhs rhs) (m : ℚ) : option gen_comp :=
if ii.implies_eq m then
  some (gen_comp.eq)
else if ii.implies_ineq (ineq.of_comp_and_slope comp.ge (slope.some m)) then
   some (if ii.implies_ineq $ ineq.of_comp_and_slope comp.gt (slope.some m) then gen_comp.gt else gen_comp.ge)
else if ii.implies_ineq (ineq.of_comp_and_slope comp.le (slope.some m)) then
   some (if ii.implies_ineq $ ineq.of_comp_and_slope comp.lt (slope.some m) then gen_comp.lt else gen_comp.le)
else none

-- returns the known comparisons of e with 1 and -1
meta def oc (e : expr) : mul_state (option gen_comp × option gen_comp) :=
do ii ← oi e,
return (find_comp ii 1, find_comp ii (-1))

meta def is_ge_one (e : expr) : mul_state bool :=
do (c, _) ← oc e,
match c with
| some c' := return c'.is_greater_or_eq
| none := return ff
end

meta def is_le_one (e : expr) : mul_state bool :=
do (c, _) ← oc e,
match c with
| some c' := return c'.is_less_or_eq
| none := return ff
end

meta def is_le_neg_one (e : expr) : mul_state bool :=
do (_, c) ← oc e,
match c with
| some c' := return c'.is_less_or_eq
| none := return ff
end

meta def is_ge_neg_one (e : expr) : mul_state bool :=
do (_, c) ← oc e,
match c with
| some c' := return c'.is_greater_or_eq
| none := return ff
end

meta def is_pos_le_one (e : expr) : mul_state bool :=
do ⟨c, _⟩ ← si e,
match c with
| gen_comp.gt := is_le_one e --bnot <$> is_ge_one e
| _ := return ff
end

meta def is_neg_ge_neg_one (e : expr) : mul_state bool :=
do ⟨c, _⟩ ← si e,
match c with
| gen_comp.lt := is_ge_neg_one e-- bnot <$> is_le_neg_one e
| _ := return ff
end

private meta def all_signs : mul_state (hash_map expr sign_data) :=
prod.fst <$> get

section sign_inference

meta def sign_of_term (pf : prod_form) (e : expr) : mul_state (option gen_comp) :=
match pf.exps.find e with
| some z :=
  do opt  ← si' e,
  match opt with
  | some ⟨gen_comp.lt, _⟩ := return $ some $ if z % 2 = 0 then gen_comp.gt else gen_comp.lt
  | some ⟨gen_comp.le, _⟩ := return $ some $ if z % 2 = 0 then gen_comp.ge else gen_comp.le
  | some ⟨gen_comp.eq, _⟩ := return $ if z > 0 then some gen_comp.eq else none
  | some ⟨c, _⟩ := return $ some c -- gt, ge, ne
  | _ := return none
  end
| none := return none
end

meta def sign_of_prod (l : list gen_comp) : option gen_comp :=
l.mfoldl gen_comp.prod gen_comp.gt

-- get_remaining_sign g s returns the unique g' such that gen_comp.prod g g' = s
meta def get_remaining_sign_aux : gen_comp → spec_comp → option gen_comp
| gen_comp.gt s := s.to_gen_comp
| gen_comp.ge spec_comp.lt := none
| gen_comp.ge s := s.to_gen_comp
| gen_comp.eq _ := none
| gen_comp.le spec_comp.lt := none
| gen_comp.le s := s.to_gen_comp.reverse
| gen_comp.lt s := s.to_gen_comp.reverse
| gen_comp.ne s := none

meta def get_remaining_sign : gen_comp → gen_comp → option gen_comp
| a gen_comp.gt := gen_comp.reverse <$> (get_remaining_sign_aux a spec_comp.lt)
| a gen_comp.ge := gen_comp.reverse <$> (get_remaining_sign_aux a spec_comp.le)
| gen_comp.gt gen_comp.ne := gen_comp.ne
| gen_comp.lt gen_comp.ne := gen_comp.ne
| gen_comp.ne gen_comp.ne := gen_comp.ne
| _ gen_comp.ne := none
| a b := get_remaining_sign_aux a b.to_spec_comp

/-meta def get_unknown_sign_data : prod_form_comp_data → mul_state (option (Σ e, sign_data e))
| ⟨⟨prod_f, c⟩, prf, _⟩ :=
do sds ← prod_f.exps.keys.mmap (sign_of_term prod_f),
   let known_signs := (sds.bfilter option.is_some),
   if known_signs.length = 1 then
     match sign_of_prod (known_signs.map option.iget) with
     | some ks :=
       match get_remaining_sign ks c with
       | some c' :=
         let i := sds.index_of none,
             e := prod_f.exps.keys.inth i,
             pfe := sign_proof.adhoc e c' (tactic.fail "unfinished adhoc") in
         return $ some ⟨e, ⟨_, pfe⟩⟩
         -- e has sign ks
       | none := return none
       end
     | none := return none
     end
   else return none-/

private meta def reduce_sig_opt_list {α} {β : α → Type} : list (Σ a : α, option (β a)) → list (Σ a : α, (β a))
| [] := []
| (⟨a, none⟩::t) := reduce_sig_opt_list t
| (⟨a, some b⟩::t) := ⟨a, b⟩::reduce_sig_opt_list t

private lemma aux_sign_infer_tac_lemma (P : Prop) : P := sorry

-- TODO
private meta def aux_sign_infer_tac (e : expr) (pf : prod_form) (sds : hash_map expr sign_data) (c : gen_comp) : tactic expr :=
let sds' : list ((Σ e, (sign_data e))) := reduce_sig_opt_list $ pf.exps.keys.map (λ e, sigma.mk e (sds.find e)) in
do --sds ← pf.exps.keys.mmap $ λ e, sigma.mk e <$> (si e),
   sds'.mmap (λ a, a.snd.prf.reconstruct),
   tp ← c.to_function e `(0 : ℚ),
   tactic.mk_app ``aux_sign_infer_tac_lemma [tp]

-- TODO : used when only one sign in the middle is unknown
-- proves e C 0 when pf is the prod form of whole
private meta def aux_sign_infer_tac_2 (e whole : expr) (sd : sign_data whole) (pf : prod_form)  (sds : hash_map expr sign_data)  (c : gen_comp) : tactic expr :=
let sds' : list ((Σ e, (sign_data e))) := reduce_sig_opt_list $ pf.exps.keys.map (λ e, sigma.mk e (sds.find e)) in
do --sds ← pf.exps.keys.mmap $ λ e, sigma.mk e <$> (si e),
   sds'.mmap (λ a, a.snd.prf.reconstruct),
   sd.prf.reconstruct,
   tp ← c.to_function e `(0 : ℚ),
   tactic.mk_app ``aux_sign_infer_tac_lemma [tp]

/--
 Assumes known_signs.length = pf.length
-/
meta def infer_expr_sign_data_aux (e : expr) (pf : prod_form) (known_signs : list gen_comp) : mul_state (option Σ e', sign_data e') :=
  let prod_sign :=
    (if pf.coeff < 0 then gen_comp.reverse else id) <$> sign_of_prod known_signs in
  match prod_sign with
  | some ks :=
    do sis ← all_signs,
    let pfe  := sign_proof.adhoc e ks (do s ← format_sign e ks, return ⟨s, "inferred from other sign data", []⟩) (aux_sign_infer_tac e pf sis ks) in
--(do s ← tactic.pp e, sf ← tactic.pp ks, tactic.fail $ "unfinished adhoc -- infer-expr-sign-data-aux: 0 "  ++ sf.to_string ++ s.to_string)
    return $ some ⟨e, ⟨_, pfe⟩⟩
  | none := return none
  end

/--
 Infers the sign of an expression when the sign of subexpressions is known.
-/
meta def infer_expr_sign_data (e : expr) (pf : prod_form) : mul_state (option Σ e', sign_data e') :=
do sds ← pf.exps.keys.mmap (sign_of_term pf),
   let known_signs := sds.reduce_option,
   if pf.exps.keys.length = known_signs.length then
    infer_expr_sign_data_aux e pf known_signs
   else return none

private meta def recheck_known_signs_aux (ks : list gen_comp) (es : gen_comp)  (flip_coeff : bool) (i : ℕ): option gen_comp :=
if i ≥ ks.length then none else
let ks' := ks.remove_nth i,
    prod_sign := (if flip_coeff then gen_comp.reverse else id) <$> sign_of_prod ks' in
match prod_sign with
| some sn := get_remaining_sign sn es
| none := none
end

/--
 if we know the sign of e and all of its components, recalculate the sign of each component to check.
-/
meta def recheck_known_signs (e : expr) (sd : option (sign_data e)) (pf : prod_form) (ks : list gen_comp) (flip_coeff : bool) : mul_state (list Σ e', sign_data e') :=
match sd with
| none := return []
| some ⟨es, p⟩ := list.reduce_option <$>
((list.range ks.length).mmap $ λ i,
  match recheck_known_signs_aux ks es flip_coeff i with
  | some c :=
   do sis ← all_signs,
   let e' := pf.exps.keys.inth i,
   let pfe := sign_proof.adhoc e' c (do s ← format_sign e' c, return ⟨s, "inferred from other sign data", []⟩) (aux_sign_infer_tac_2 e' e ⟨es, p⟩ pf sis c),
   return $ some ⟨e', ⟨_, pfe⟩⟩
  | none := return none
  end)
end

/--
 Tries to infer sign data of variables in expression when the sign of the whole expression is known.
-/
meta def get_unknown_sign_data (e : expr) (sd : option (sign_data e)) (pf : prod_form) : mul_state (list Σ e', sign_data e') :=
do sds ← pf.exps.keys.mmap (sign_of_term pf),
   let known_signs := sds.reduce_option,
   let num_vars := pf.exps.keys.length,
   if (known_signs.length = num_vars - 1) && sd.is_some then
     let prod_sign :=
      (if pf.coeff < 0 then gen_comp.reverse else id) <$> sign_of_prod known_signs in
     match prod_sign with
     | some ks :=
       match get_remaining_sign ks sd.iget.c with
       | some c' :=
         do sis ← all_signs,
         let i := sds.index_of none,
         let e' := pf.exps.keys.inth i,
         let sd' := sd.iget,
         let pfe := sign_proof.adhoc e' c' (do s ← format_sign e' c', return ⟨s, "inferred from other sign data", []⟩) (aux_sign_infer_tac_2 e' e sd' pf sis c'),
-- (tactic.fail "unfinished adhoc -- get-unknown-sign-data"),
         return $ [⟨e', ⟨_, pfe⟩⟩]
         -- e has sign ks
       | none := return []
       end
     | none := return []
     end
   else if known_signs.length = num_vars then
     /-let prod_sign :=
      (if pf.coeff < 0 then gen_comp.reverse else id) <$> sign_of_prod (known_signs.map option.iget) in
     match prod_sign with
     | some ks :=
       if sd.c.implies ks then return none else
         let pfe := sign_proof.adhoc e ks (tactic.fail "unfinished adhoc") in
         return $ some ⟨e, ⟨_, pfe⟩⟩
     | none := return none
     end-/
     do k1 ← infer_expr_sign_data_aux e pf known_signs,
        k2 ← recheck_known_signs e sd pf known_signs (pf.coeff < 0),
        match k1 with
        | some k1' := return $ k1'::k2
        | none := return k2
        end
   else return []

end sign_inference

section sfcd_to_ineq

/- -- assumes lhs < rhs as exprs. cl*lhs + cr*rhs R 0 ==> ineq_data
private meta def mk_ineq_data_of_lhs_rhs (lhs rhs : expr) (cl cr : ℚ) (c : comp) {s} (pf : sum_form_proof s) :
        Σ l r, ineq_data l r :=
let c' := if cl > 0 then c else c.reverse,
    iq := ineq.of_comp_and_slope (c') (slope.some (-cr/cl)) in
⟨lhs, rhs, ⟨iq, ineq_proof.of_sum_form_proof lhs rhs iq pf⟩⟩ --_ _ _ (iq.to_expr lhs rhs pf)⟩⟩ -- TODO
--⟨lhs, rhs, ⟨iq, ineq_proof.hyp _ _ _ ```(0)⟩⟩ -- TODO

-/

-- assuming 1 r coeff*lhs^el*rhs^er, finds r' such that 1 r coeff*|lhs|^el*|rhs|^er
/-private meta def get_abs_val_comp (lhs rhs : expr) (el er : ℤ)  (coeff : ℚ) : spec_comp → mul_state comp
| spec_comp.lt := _
| spec_comp.le := _
| spec_comp.eq := _
-/

-- is_junk_comp c lhss rhss checks to see if lhs c rhs is of the form pos > neg, neg < pos, etc
-- we can assume the gen_comps are strict.
private meta def is_junk_comp : comp → gen_comp → gen_comp → bool
| comp.gt gen_comp.gt gen_comp.lt := tt
| comp.ge gen_comp.gt gen_comp.lt := tt
| comp.le gen_comp.lt gen_comp.gt := tt
| comp.lt gen_comp.lt gen_comp.gt := tt
| _ _ _ := ff

-- none if can never lower. some tt if can always lower. some ff if can only lower by even number
private meta def can_lower (e : expr) (ei : ℤ) : mul_state (option bool) :=
do iplo ← is_pos_le_one e,
   if iplo then return $ some tt else  do
   ingno ← is_neg_ge_neg_one e,
   if ingno && (ei % 2 = 0) then return $ some ff else do
   ilno ← is_le_neg_one e,
   if ilno && (ei % 2 = 1) then return $ some ff
   else return none

private meta def can_raise (e : expr) (ei : ℤ) : mul_state (option bool) :=
do igo ← is_ge_one e,
   if igo then return $ some tt else  do
   ilno ← is_le_neg_one e,
   if ilno && (ei % 2 = 0) then return $ some ff else do
   ingno ← is_neg_ge_neg_one e,
   if ingno && (ei % 2 = 1) then return $ some ff
   else return none

private meta def can_change_aux (diff_even : bool) : option bool → bool
| (some tt) := tt
| (some ff) := diff_even
| none := ff

private meta def can_change (ob : option bool) (el er : ℤ) : bool :=
can_change_aux ((el - er) % 2 = 0) ob

-- assuming cmpl and cmpr are the signs of lhs and rhs, tries to find el', er' such that lhs^el*rhs^er ≤ lhs^el'*rhs^er'
private meta def balance_coeffs : expr → expr → ℤ → ℤ → mul_state (list (ℤ × ℤ)) | lhs rhs el er:=
if el = (/-trace_val-/ ("el, -er", lhs, rhs, el, -er)).2.2.2.2 then return $ [(el, er)] else
if (/-trace_val-/ ("el.nat_abs", el.nat_abs)).2 ≤ er.nat_abs then
  do cll ← /-trace_val <$> -/can_lower lhs el, crl ← /-trace_val <$>-/ can_raise lhs el, clr ← /-trace_val <$> -/can_lower rhs er, crr ← /-trace_val <$>-/ can_raise rhs er,
  return $
   if (el < 0) && (er > 0) then
    (guard (can_change clr el er) >> return (el, -el)) <|> (guard (can_change cll el er) >> return (-er, er))
   else if (el > 0) && (er < 0) then
    (guard (can_change crr el er) >> return (el, -el)) <|> (guard (can_change crl el er) >> return (-er, er))
   else if (el > 0) && (er > 0) then
    (guard (can_change clr el er) >> return (el, -el)) <|> (guard (can_change cll el er) >> return (-er, er))
   else if (el < 0) && (er < 0) then
    (guard (can_change crr el er) >> return (el, -el)) <|> (guard (can_change crl el er) >> return (-er, er))
  else []
else do pro ← balance_coeffs rhs lhs er el,
return $ pro.map (λ p, (p.2, p.1))

/-return $ match clr, crl with
| some br, some bl := if br then el else if (er - el) % 2 = 0 then el else if bl then er else none
| some br, none := if br || ((er - el)%2 = 0) then some el else none
| none, some bl := if bl || ((er - el)%2 = 0) then some er else none
| none, none := none
end
else do cll ← can_lower lhs el, crr ← can_raise rhs er,
return $ match cll, crr with
| some bl, some br := if bl then er else if (el - er) % 2 = 0 then er else if br then el else none
| some bl, none := if bl || ((el - er) % 2 = 0) then some er else none
| none, some br := if br || ((el - er) % 2 = 0) then some el else none
| none, none := none
end-/

-- assumes lhs > rhs as exprs, and el = -er. 1 R coeff*lhs^el*rhs^er ==> ineq
private meta def mk_ineq_of_balanced_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) (c : spec_comp) : mul_state ineq :=
if (el % 2 = 0) && (coeff < 0) then -- todo: this is a contradiction
  do ⟨cmpl, _⟩ ← si lhs, return $ (/-trace_val-/ ("GOT A CONTRADICTION HERE", ineq.of_comp_and_slope cmpl.to_comp.reverse (slope.some 0))).2
else
-- know: 1 c | (root coeff |el|)*lhs^(sign el)*rhs^(sign er) |
do ⟨cmpl, _⟩ ← si lhs, ⟨cmpr, _⟩ ← si rhs,
let coeff_comp := if coeff < 0 then comp.lt else comp.gt,
let prod_sign := (cmpl.to_comp.prod cmpr.to_comp).prod coeff_comp,
let exp_val := el.nat_abs,
--if prod_sign.is_greater then
-- know: 1 c (root coeff exp_val)*lhs^(sign el)*rhs^(sign er)
  if cmpl.is_greater then -- lhs > 0
    let c' := c.to_comp,
      m  := (if prod_sign.is_greater then (1 : ℚ) else -1) * nth_root_approx approx_dir.over coeff exp_val approx_prec in return $ /-trace_val $-/
     if el < 0 then ineq.of_comp_and_slope c' (slope.some m)
    else ineq.of_comp_and_slope c'.reverse (slope.some (1/m))
  else -- x < 0
    let c' := c.to_comp.reverse,
        m  :=  (if prod_sign.is_greater then (1 : ℚ) else -1) * nth_root_approx approx_dir.under coeff exp_val approx_prec in return $
    if el < 0 then ineq.of_comp_and_slope c' (slope.some m)
    else  ineq.of_comp_and_slope c'.reverse (slope.some (1/m))
/-else
-- know: 1 c -(root coeff exp_val)*lhs^(sign el)*rhs^(sign er)
  if cmpl.is_greater then -- lhs > 0
    let c' := c.to_comp,
        m  := nth_root_approx approx_dir.over coeff exp_val approx_prec in
    if el < 0 then return $ ineq.of_comp_and_slope c' (slope.some (-m))
    else return $ ineq.of_comp_and_slope c'.reverse (slope.some (-1/m))
  else
    let c' := c.to_comp.reverse,
        m  := nth_root_approx approx_dir.under coeff exp_val approx_prec-/
/-if el < 0 then
 let c' := if cmpl.is_less then c.to_comp.reverse else c.to_comp,
     el' := -el in -- lhs^el' c' coeff * rhs^er
 -/

/-if (coeff < 0) && (exp % 2 = 0) then -- 1 ≤ neg. impossible. todo: create contr
  return none
else if coeff < 0 then
  return none
else if exp > 0 then
  let nexp := exp.nat_abs,
      coeff_root_approx := nth_root_approx'' approx_dir.over coeff nexp approx_prec in
  return none
else
  return none-/

-- assumes lhs > rhs as exprs. 1 R coeff* lhs^el * rhs^er ==> ineq_data
private meta def mk_ineq_of_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) (c : spec_comp) :
        mul_state (list ineq) :=
do ⟨cmpl, _⟩ ← si lhs, ⟨cmpr, _⟩ ← si rhs,
let cmpl' := cmpl.pow el,
let cmpr' := cmpr.pow er,
if is_junk_comp (if cmpl' = gen_comp.gt then c.to_comp else c.to_comp.reverse) cmpl' (if coeff > 0 then cmpr' else cmpr'.reverse) then return [] else
do ncs ← balance_coeffs lhs rhs el er,
   ncs.mmap $ λ p, do t ← mk_ineq_of_balanced_lhs_rhs coeff lhs rhs p.1 p.2 c, return (/-trace_val-/ ("got from mk_ineq", ncs.length, lhs, rhs, el, er, p.1, p.2, t)).2.2.2.2.2.2.2.2
/-match ncs with
| none := return none
| some (el', er') := some <$> mk_ineq_of_balanced_lhs_rhs coeff lhs rhs (trace_val ("calling mk_ineq", lhs, rhs, el, er, el')).2.2.2.2.2 er' c
end-/

-- assumes lhs > rhs as exprs. 1 R coeff* lhs^el * rhs^er ==> ineq_data
/-private meta def mk_ineq_of_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) (c : spec_comp) :
        mul_state (option ineq) :=
do ⟨cmpl, _⟩ ← si lhs, ⟨cmpr, _⟩ ← si rhs,
let cmpl' := cmpl.pow el,
let cmpr' := cmpr.pow er,
if is_junk_comp (if cmpl' = gen_comp.gt then c.to_comp else c.to_comp.reverse) cmpl' (if coeff > 0 then cmpr' else cmpr'.reverse) then return none else
   if cmpl = gen_comp.gt then -- lhs^(-el) c coeff*rhs^(er)
     if (el = -1) && (er = 1) then return $ some $ ineq.of_comp_and_slope c.to_comp (slope.some coeff)
     else if (el = 1) && (er = -1) then return $ some $ ineq.of_comp_and_slope c.to_comp.reverse (slope.some (1/coeff))
     else if (el = -1) && (er > 0) then -- lhs c coeff*rhs^er

     else return none
   else if cmpl = gen_comp.lt then -- lhs^(-el) -c coeff*rhs^(er)
     if (el = -1) && (er = 1) then return $ some $ ineq.of_comp_and_slope c.to_comp.reverse (slope.some coeff)
     else if (el = 1) && (er = -1) then return $ some $ ineq.of_comp_and_slope c.to_comp (slope.some (1/coeff))
     else if el = -1 then
       return none
     else return none
   else return none-/

-- assumes lhs > rhs as exprs. 1 = coeff* lhs^el * rhs^er ==> eq_data (coeff)
-- TODO
private meta def mk_eq_of_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) :
        mul_state (option ℚ) :=
do ⟨cmpl, _⟩ ← si lhs, ⟨cmpr, _⟩ ← si rhs,
--   if cmpl = gen_comp.gt then -- lhs^(-el) c coeff*rhs^(er)
     if (el = -1) && (er = 1) then return $ some coeff
     else if (el = 1) && (er = -1) then return $ some (1/coeff)
     else return none
--   else  -- lhs^(-el)
--     return none -- TODO

section

private lemma mk_ineq_proof_of_lhs_rhs_aux (P : Prop) {sp old : Prop} (p' : sp) (p : old) : P :=
sorry
#check @mk_ineq_proof_of_lhs_rhs_aux
open tactic
--#check @op_of_one_op_pos
meta def mk_ineq_proof_of_lhs_rhs /-(coeff : ℚ)-/ (lhs rhs : expr) (el er : ℤ) /-(c : spec_comp)-/ {s} (pf : prod_form_proof s) (iq : ineq) : mul_state (tactic expr) :=
do sdl ← si lhs,
match sdl with
| ⟨gen_comp.gt, pf'⟩ := do oil ← oi lhs, oir ← oi rhs, return $
   do --tactic.trace "in mk_ineq_proof_of_lhs_rhs 1",
      pfr ← pf.reconstruct, trace "1", pfr' ← pf'.reconstruct,
      --trace "reconstructed::", infer_type pfr >>= trace, infer_type pfr' >>= trace, trace pf,
      tpr ← tactic.mk_mapp ``op_of_one_op_pos [none, none, none, none, none, some pfr', none, none, some pfr],
      if (el = 1) && (er = -1) then tactic.mk_app ``op_of_inv_op_inv_pow [tpr]
      else if (el = -1) && (er = 1) then tactic.mk_app ``op_of_op_pow [tpr]
      else
         do trace "know", infer_type pfr >>= trace, infer_type pfr' >>= trace,
          trace "wts", trace (lhs, rhs, iq),
         tp ← iq.to_type lhs rhs,
         mk_mapp ``mk_ineq_proof_of_lhs_rhs_aux [tp, none, none, pfr', pfr]
--           fail $ "can't handle non-one exponents yet" ++ to_string el ++ " " ++ to_string er
| ⟨gen_comp.lt, pf'⟩ := return $
   do --tactic.trace "in mk_ineq_proof_of_lhs_rhs 2",
      pfr ← pf.reconstruct,-- trace "reconstructed::", infer_type pfr >>= trace,
      pfr' ← pf'.reconstruct,
      tactic.mk_mapp ``op_of_one_op_neg [none, none, none, none, none, some pfr', none, none, some pfr]
| _ := return $ tactic.fail "mk_ineq_proof_of_lhs_rhs failed, no sign info for lhs"
end
end

meta def find_deps_of_pfp : Π {pfc}, prod_form_proof pfc → tactic (list proof_sketch)
| _ (prod_form_proof.of_ineq_proof id _ _) := do id' ← id.sketch, return [id']
| _ (prod_form_proof.of_eq_proof id _) := do id' ← id.sketch, return [id']
| _ (prod_form_proof.of_expr_def e pf) := do s ← to_string <$> (pf.to_expr >>= tactic.pp), return [⟨"1 = " ++ s, "by definition", []⟩]
| _ (prod_form_proof.of_pow _ pfp) := find_deps_of_pfp pfp
| _ (prod_form_proof.of_mul pfp1 pfp2 _) := do ds1 ← find_deps_of_pfp pfp1, ds2 ← find_deps_of_pfp pfp2, return (ds1 ++ ds2)
| _ (prod_form_proof.adhoc _ t _) := do t' ← t, return [t']
| _ (prod_form_proof.fake _) := return []

meta def make_proof_sketch_for_ineq {s} (lhs rhs : expr) (iq : ineq) (pf : prod_form_proof s) : tactic proof_sketch :=
do s' ← format_ineq lhs rhs iq, deps ← find_deps_of_pfp pf,
   return ⟨s', "by multiplicative arithmetic", deps⟩

-- assumes lhs > rhs as exprs. 1 R coeff* lhs^el * rhs^er ==> ineq_data
private meta def mk_ineq_data_of_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) (c : spec_comp) {s} (pf : prod_form_proof s) :
        mul_state (list Σ l r, ineq_data l r) :=
do iq ← mk_ineq_of_lhs_rhs coeff lhs rhs el er c,
   iq.mmap $ λ id, do tac ← mk_ineq_proof_of_lhs_rhs lhs rhs el er pf id,
      return $ ⟨lhs, rhs, ⟨id, ineq_proof.adhoc _ _ id (make_proof_sketch_for_ineq lhs rhs id pf) tac⟩⟩
/-   match iq with
   | none := return none
   | some id := do tac ← mk_ineq_proof_of_lhs_rhs lhs rhs el er pf id,
      return $ some ⟨lhs, rhs, ⟨id, ineq_proof.adhoc _ _ id $
         tac
--       do t ← id.to_type lhs rhs, tactic.trace "sorrying", tactic.trace t, tactic.to_expr ``(sorry : %%t) --tactic.fail "mk_ineq_data not implemented"
      ⟩⟩
   end-/

-- assumes lhs > rhs as exprs. 1 = coeff* lhs^el * rhs^er ==> eq_data
-- TODO
private meta def mk_eq_data_of_lhs_rhs (coeff : ℚ) (lhs rhs : expr) (el er : ℤ) {s} (pf : prod_form_proof s) :
        mul_state (option Σ l r, eq_data l r) :=
do eqc ← mk_eq_of_lhs_rhs coeff lhs rhs el er,
   match eqc with
   | none := return none
   | some c := do /-tac ← mk_ineq_proof_of_lhs_rhs lhs el er pf,-/ return none
     -- return $ some ⟨lhs, rhs, ⟨id, ineq_proof.adhoc _ _ id $
       --  tac
--       do t ← id.to_type lhs rhs, tactic.trace "sorrying", tactic.trace t, tactic.to_expr ``(sorry : %%t) --tactic.fail "mk_ineq_data not implemented"
--      ⟩⟩ -- todo
   end

-- pf proves 1 c coeff*e^(-1)
-- returns a proof of 1 c' (1/coeff) * e

-- 1 c coeff * e^exp
private meta def mk_ineq_data_of_single_cmp (coeff : ℚ) (e : expr) (exp : ℤ) (c : spec_comp) {s} (pf : prod_form_proof s) :
        mul_state (option Σ lhs rhs, ineq_data lhs rhs) :=
if exp = 1 then
  let inq := ineq.of_comp_and_slope c.to_comp (slope.some coeff),
      id : ineq_data `(1 : ℚ) e := ⟨inq, ineq_proof.adhoc _ _ _ (make_proof_sketch_for_ineq `(1 : ℚ) e inq pf) (do pf' ← pf.reconstruct, tactic.mk_mapp ``one_op_of_op [none, none, none, none, pf'])⟩ in--(tactic.fail "mk_ineq_data_of_single_cmp not implemented")⟩ in
  return $ some ⟨_, _, id⟩
else if exp = -1 then
  let inq := ineq.of_comp_and_slope c.to_comp.reverse (slope.some coeff).invert,
       id : ineq_data `(1 : ℚ) e := ⟨inq, ineq_proof.adhoc _ _ _
         (make_proof_sketch_for_ineq `(1 : ℚ) e inq pf)
         (do pf' ← pf.reconstruct,
           tactic.mk_mapp ``one_op_of_op_inv [none, none, none, none, pf'])⟩ in
  return $ some ⟨_, _, id⟩
else -- TODO
 if exp > 0 then
   if (coeff < 0) && (exp % 2 = 0) then return none -- todo: this is a contradiction
   else do ⟨es, _⟩ ← si e,
   if es.is_greater then
     let m := nth_root_approx approx_dir.over coeff exp.nat_abs approx_prec,
         inq := ineq.of_comp_and_slope c.to_comp (slope.some m) in
     return $ some $ ⟨_, _, ⟨inq, ineq_proof.adhoc rat_one e _
      (make_proof_sketch_for_ineq rat_one e inq pf)
      (tactic.fail "mk_ineq_data_of_single_cmp not implemented")⟩⟩
   else --todo
    return none
 else return none

private meta def mk_eq_data_of_single_cmp (coeff : ℚ) (e : expr) (exp : ℤ) {s} (pf : prod_form_proof s) :
        mul_state (option Σ lhs rhs, eq_data lhs rhs) :=
if exp = 1 then
  let id : eq_data `(1 : ℚ) e := ⟨coeff, eq_proof.adhoc _ _ _ (tactic.fail "mk_eq_data_of_single_cmp not implemented") (tactic.fail "mk_eq_data_of_single_cmp not implemented")⟩ in
  return $ some ⟨_, _, id⟩
else -- TODO
return none

-- we need a proof constructor for ineq and eq
meta def prod_form_comp_data.to_ineq_data : prod_form_comp_data → mul_state (list (Σ lhs rhs, ineq_data lhs rhs))
| ⟨⟨_, spec_comp.eq⟩, _, _⟩ := return []
| ⟨⟨⟨coeff, exps⟩, c⟩, prf, _⟩ :=
  match exps.to_list with
  | [(rhs, cr), (lhs, cl)] :=
    if rhs.lt lhs then  mk_ineq_data_of_lhs_rhs coeff lhs rhs cl cr c prf
    else mk_ineq_data_of_lhs_rhs coeff rhs lhs cr cl c prf
  | [(rhs, cr)] := do t ← mk_ineq_data_of_single_cmp coeff rhs cr c prf,
       return $ /-trace_val-/ ("in pfcd.toid:", t),
      match t with | some t' := return [t'] | none := return [] end
  | [] := if coeff ≥ 1 then return [] else return [⟨rat_one, rat_one, ⟨ineq.of_comp_and_slope c.to_comp (slope.some coeff), ineq_proof.adhoc _ _ _ (tactic.fail "prod_form_comp_data.to_ineq_data not implemented") (tactic.fail "oops")⟩⟩]
  | _ := return []
  end

meta def prod_form_comp_data.to_eq_data : prod_form_comp_data → mul_state (option (Σ lhs rhs, eq_data lhs rhs))
| ⟨⟨⟨coeff, exps⟩, spec_comp.eq⟩, prf, _⟩ :=
  match exps.to_list with
  | [(rhs, cr), (lhs, cl)] :=     if rhs.lt lhs then  mk_eq_data_of_lhs_rhs coeff lhs rhs cl cr prf
    else mk_eq_data_of_lhs_rhs coeff rhs lhs cr cl prf
  | [(rhs, cr)] := mk_eq_data_of_single_cmp coeff rhs cr prf
  | _ := return none
  end
| _ := return none

end sfcd_to_ineq

--meta structure sign_storage :=
--(signs : hash_map expr sign_info)

--private meta def inh_sp (e : expr) : inhabited (sign_proof e gen_comp.ne) := ⟨sign_proof.adhoc _ _ (tactic.failed)⟩

meta def ne_pf_of_si {e : expr} (sd : sign_data e) : sign_proof e gen_comp.ne :=
sign_proof.diseq_of_strict_ineq sd.prf

meta def find_cancelled (pf1 pf2 : prod_form) : list expr :=
pf1.exps.fold [] (λ t exp l, if exp + pf2.get_exp t = 0 then t::l else l)

meta def ne_proofs_of_cancelled (pf1 pf2 : prod_form) : mul_state (list Σ e : expr, sign_proof e gen_comp.ne) :=
(find_cancelled pf1 pf2).mmap (λ e, do sd ← si e, return ⟨e, ne_pf_of_si sd⟩)

meta def prod_form_proof.pfc {pfc} : prod_form_proof pfc → prod_form_comp := λ _, pfc

open native

-- assumes the exponent of pvt in both is nonzero. Does not enforce elim_list preservation
meta def prod_form_comp_data.elim_expr_aux : prod_form_comp_data → prod_form_comp_data → expr →
     mul_state (option prod_form_comp_data)
| ⟨⟨pf1, comp1⟩, prf1, elim_list1⟩ ⟨⟨pf2, comp2⟩, prf2, elim_list2⟩ pvt :=
let exp1 := pf1.get_exp pvt,
    exp2 := pf2.get_exp pvt in
if exp1 * exp2 < 0 then
 let npow : int := nat.lcm exp1.nat_abs exp2.nat_abs,
     pf1p := prod_form_proof.of_pow (npow/(abs exp1)) prf1,
     pf2p := prod_form_proof.of_pow (npow/(abs exp2)) prf2 in do
 neprfs ← ne_proofs_of_cancelled pf1p.pfc.pf pf2p.pfc.pf,
 let nprf := prod_form_proof.of_mul pf1p pf2p neprfs in
 return $ some $ prod_form_comp_data.round ⟨_, nprf, (rb_set.union elim_list1 elim_list2).insert pvt⟩ approx_prec
else if comp1 = spec_comp.eq then
 let pf1p := prod_form_proof.of_pow (-1) prf1 in
 prod_form_comp_data.elim_expr_aux ⟨_, pf1p, elim_list1⟩ ⟨_, prf2, elim_list2⟩ pvt
else if comp2 = spec_comp.eq then
 let pf2p := prod_form_proof.of_pow (-1) prf2 in
 prod_form_comp_data.elim_expr_aux ⟨_, prf1, elim_list1⟩ ⟨_, pf2p, elim_list2⟩ pvt
else return none

meta def prod_form_comp_data.elim_expr (pfcd1 pfcd2 : prod_form_comp_data) (pvt : expr) :
     mul_state (option prod_form_comp_data) :=
if pfcd1.pfc.pf.get_exp pvt = 0 then return $ some ⟨pfcd1.pfc, pfcd1.prf, pfcd1.elim_list.insert pvt⟩
else if pfcd2.pfc.pf.get_exp pvt = 0 then return  none
else prod_form_comp_data.elim_expr_aux pfcd1 pfcd2 pvt

private meta def compare_coeffs (sf1 sf2 : prod_form) (h : expr) : ordering :=
let c1 := sf1.get_exp h, c2 := sf2.get_exp h in
if c1 < c2 then ordering.lt else if c2 < c1 then ordering.gt else ordering.eq

private meta def compare_coeff_lists (sf1 sf2 : prod_form) : list expr → list expr → ordering
| [] [] := ordering.eq
| [] _ := ordering.lt
| _ [] := ordering.gt
| (h1::t1) (h2::t2) :=
   if h1 = h2 then let ccomp := compare_coeffs sf1 sf2 h1 in
     if ccomp = ordering.eq then compare_coeff_lists t1 t2 else ccomp
   else cmp h1 h2

meta def prod_form.order (sf1 sf2 : prod_form) : ordering :=
compare_coeff_lists sf1 sf2 sf1.exps.keys sf2.exps.keys

meta def prod_form_comp.order : prod_form_comp → prod_form_comp → ordering
| ⟨_, spec_comp.lt⟩ ⟨_, spec_comp.le⟩ := ordering.lt
| ⟨_, spec_comp.lt⟩ ⟨_, spec_comp.eq⟩ := ordering.lt
| ⟨_, spec_comp.le⟩ ⟨_, spec_comp.eq⟩ := ordering.lt
| ⟨sf1, _⟩ ⟨sf2, _⟩ := prod_form.order sf1 sf2 -- need to normalize!

meta def prod_form_comp_data.order : prod_form_comp_data → prod_form_comp_data → ordering
| ⟨sfc1, _, ev1⟩ ⟨sfc2, _, ev2⟩ :=
match sfc1.order sfc2 with
| ordering.eq := cmp ev1.keys ev2.keys
| a := a
end

meta instance prod_form_comp_data.has_lt : has_lt prod_form_comp_data := ⟨λ x y, prod_form_comp_data.order x y = ordering.lt⟩
meta instance prod_form_comp_data.decidable_lt : decidable_rel (@has_lt.lt prod_form_comp_data _) := λ _ _, by apply_instance

meta def prod_form_comp_data.elim_into (sfcd1 sfcd2 : prod_form_comp_data) (pvt : expr)
     (rv : rb_set prod_form_comp_data) : mul_state (rb_set prod_form_comp_data) :=
do elimd ← /-trace_val <$>-/ sfcd1.elim_expr sfcd2 pvt,
   match elimd with
   | none := return rv
   | some sfcd := return $ rv.insert sfcd
   end

private meta def check_elim_lists_aux (sfcd1 sfcd2 : prod_form_comp_data) : bool :=
sfcd1.vars.all (λ e, bnot (sfcd2.elim_list.contains e))

private meta def check_elim_lists (sfcd1 sfcd2 : prod_form_comp_data) : bool :=
check_elim_lists_aux sfcd1 sfcd2 && check_elim_lists_aux sfcd2 sfcd1

meta def prod_form_comp_data.needs_elim_against (sfcd1 sfcd2 : prod_form_comp_data) (e : expr) : bool :=
(check_elim_lists sfcd1 sfcd2) &&
 (((sfcd1.vars.append sfcd2.vars).filter (λ e' : expr, e'.lt e)).length ≤ 2)

namespace prod_form

/--
 Uses sfcd to eliminate the e from all comparisons in cmps, and adds the new comparisons to rv
-/
meta def elim_expr_from_comp_data_filtered (sfcd : prod_form_comp_data) (cmps : rb_set prod_form_comp_data)
         (e : expr) (rv : rb_set prod_form_comp_data) : mul_state (rb_set prod_form_comp_data) :=
cmps.mfold rv (λ c rv', if (/-trace_val-/ (sfcd.needs_elim_against (/-trace_val-/ c) (/-trace_val-/ e) : bool)) = tt then sfcd.elim_into c e rv' else return rv')

/--
 Performs all possible eliminations with sfcd on cmps. Returns a set of all new comps, NOT including the old ones.
-/
meta def new_exprs_from_comp_data_set (sfcd : prod_form_comp_data) (cmps : rb_set prod_form_comp_data) : mul_state (rb_set prod_form_comp_data) :=
sfcd.vars.mfoldr (λ e rv, elim_expr_from_comp_data_filtered sfcd cmps (/-trace_val-/ ("nefcds: ", e)).2 rv) mk_rb_set

meta def elim_list_into_set : rb_set prod_form_comp_data → list prod_form_comp_data → mul_state (rb_set prod_form_comp_data)
| cmps [] := return (/-trace_val-/ "elim_list_into_set []") >> return cmps
| cmps (sfcd::new_cmps) := return (/-trace_val-/ ("elim_list_into_set cons", cmps, sfcd)) >>
   if cmps.contains sfcd then elim_list_into_set cmps new_cmps else
   do new_gen ← new_exprs_from_comp_data_set sfcd cmps,--.keys
      let new_gen := new_gen.keys in
      elim_list_into_set (cmps.insert sfcd) (new_cmps.append new_gen)

meta def elim_list_set (cmps : list prod_form_comp_data) (start : rb_set prod_form_comp_data := mk_rb_set) : mul_state (rb_set prod_form_comp_data) :=
do s ← elim_list_into_set (/-trace_val-/ ("start:",start)).2 (/-trace_val-/ ("cmps:",cmps)).2,
  return (/-trace_val-/ ("elim_list_set finished:", s)).2

meta def elim_list (cmps : list prod_form_comp_data) : mul_state (list prod_form_comp_data) :=
rb_set.to_list <$> elim_list_into_set mk_rb_set (/-trace_val-/ ("cmps:", cmps)).2

end prod_form
open prod_form

section bb_process

meta def mk_eqs_of_expr_prod_form_pair : expr × prod_form → prod_form_comp_data
| (e, sf) :=
  let sf' := sf * (prod_form.of_expr e).pow (-1) in
  ⟨⟨sf', spec_comp.eq⟩, prod_form_proof.of_expr_def e sf', mk_rb_set⟩

meta def pfcd_of_ineq_data {lhs rhs} (id : ineq_data lhs rhs) : polya_state (option prod_form_comp_data) :=
do sdl ← get_sign_info lhs, sdr ← get_sign_info rhs,
match sdl, sdr with
| some sil, some sir :=
  if sil.c.is_strict && sir.c.is_strict then
    return $ some $ prod_form_comp_data.of_ineq_data id sil.prf sir.prf
  else return none
| _, _ := return (/-trace_val-/ ("no sign_info", lhs, rhs)) >> return none
end

-- TODO
meta def pfcd_of_eq_data {lhs rhs} (ed : eq_data lhs rhs) : polya_state (option prod_form_comp_data) :=
do sdl ← get_sign_info lhs, sdr ← get_sign_info rhs,
match sdl, sdr with
| some sil, some sir :=
  if sil.c.is_strict && sir.c.is_strict then
    return $ some $ prod_form_comp_data.of_eq_data ed sil.prf.diseq_of_strict_ineq
  else return none
| _, _ := return none
end

section
open tactic
private meta def remove_one_from_pfcd_proof (old : prod_form_comp) (new : prod_form) (prf : prod_form_proof old) : tactic expr :=
do `(1*%%old_e) ← { old.pf with coeff := 1}.to_expr,
   `(1*%%new_e) ← { new with coeff := 1}.to_expr,
   prf' ← prf.reconstruct,
   (_, onp) ← tactic.solve_aux `((%%old_e : ℚ) = %%new_e) `[simp only [rat.one_pow, mul_one, one_mul]],
    --tactic.infer_type onp >>= tactic.trace,
    --tactic.infer_type prf' >>= tactic.trace,
   --(l, r) ← infer_type onp >>= match_eq,
   --trace l,
--   `((<) %%l' %%r') ← infer_type prf',
--    trace r',
 --   trace $ (l = r' : bool),
   (ntp, prf'', _) ← infer_type prf' >>= tactic.rewrite onp,
 --   trace ntp,
   --infer_type prf'' >>= trace,
   --return prf''
   mk_app ``eq.mp [prf'', prf']
end
private meta def remove_one_from_pfcd (pfcd : prod_form_comp_data) : prod_form_comp_data :=
match pfcd with
| ⟨⟨⟨coeff, exps⟩, c⟩, prf, el⟩ :=
  if exps.contains rat_one then
    let pf' : prod_form := ⟨coeff, exps.erase rat_one⟩ in
    ⟨⟨pf', c⟩, (prod_form_proof.adhoc _ --prf.sketch
     (do s ← to_string <$> (pf'.to_expr >>= tactic.pp), deps ← find_deps_of_pfp prf,
         return ⟨"1 " ++ (to_string $ to_fmt c) ++ s, "rearranging", deps⟩)
     (remove_one_from_pfcd_proof pfcd.pfc pf' pfcd.prf)), el⟩
  else pfcd
end

private meta def mk_pfcd_list : polya_state (list prod_form_comp_data) :=
do il ← /-trace_val <$>-/ get_ineq_list, el ← /-trace_val <$>-/ get_eq_list, dfs ← /-trace_val <$> -/ get_mul_defs,
   il' ← /-trace_val <$>-/ list.reduce_option <$> il.mmap (λ ⟨_, _, id⟩, pfcd_of_ineq_data id),
   el' ← /-trace_val <$>-/ list.reduce_option <$> el.mmap (λ ⟨_, _, ed⟩, pfcd_of_eq_data ed),
   let dfs' := /-trace_val $-/ dfs.map mk_eqs_of_expr_prod_form_pair in -- TODO: does this filter ones without sign info?
   return $ list.map remove_one_from_pfcd $ ((il'.append el').append dfs').qsort (λ a b, if cmp a b = ordering.lt then tt else ff)

private meta def mk_signed_pfcd_list : polya_state (list (prod_form × Σ e, option (sign_data e))) :=
do mds ← get_mul_defs,
   mds' : list (prod_form × Σ e, sign_info e) ← mds.mmap (λ e_pf, do sd ← get_sign_info e_pf.1, return (e_pf.2, sigma.mk e_pf.1 sd)),
   return mds'
/-   return $ reduce_option_list $ mds'.map
    (λ pf_sig,
     match pf_sig.2 with
     | ⟨e, some sd⟩ := some ⟨pf_sig.1, ⟨e, sd⟩⟩
     | ⟨_, none⟩ := none
     end)-/

private meta def mk_sign_data_list : list expr → polya_state (list (Σ e, sign_data e))
| [] := return []
| (h::t) :=
  do si ← get_sign_info h,
  match si with
  | some sd := list.cons ⟨h, sd⟩ <$> mk_sign_data_list t
  | none := mk_sign_data_list t
  end
--set_option pp.all true
private meta def mk_one_ineq_info_list : list expr → polya_state (list (Σ e, ineq_info e rat_one))
| [] := return []
| (h::t) :=
  do si ← get_comps_with_one h,
     t' ← mk_one_ineq_info_list t,
     return $ list.cons ⟨h, si⟩ t'

meta def mk_mul_state : polya_state (hash_map expr (λ e, sign_data e) × hash_map expr (λ e, ineq_info e rat_one)) :=
do l ← get_expr_list,
   sds ← mk_sign_data_list l,
   iis ← mk_one_ineq_info_list $ sds.map sigma.fst,
   return (hash_map.of_list sds expr.hash, hash_map.of_list iis expr.hash)

private meta def gather_new_sign_info_pass_one : polya_state (list Σ e, sign_data e) :=
do  dfs ← mk_signed_pfcd_list,
    ms ← mk_mul_state,
    let vv : mul_state (list Σ e, sign_data e) := dfs.mfoldl (λ l (pf_sig : prod_form × Σ e, option (sign_data e)), l.append <$> (get_unknown_sign_data pf_sig.2.1 pf_sig.2.2 pf_sig.1)) [],
    return $ (vv.run ms).1
--    return $ reduce_option_list $ (dfs.mfoldl (λ (pf_sig : prod_form × Σ e, option (sign_data e)) (l : , l.append (get_unknown_sign_data pf_sig.2.1 pf_sig.2.2 pf_sig.1)) ms).1

/-
the second pass was originally to handle transitivity, but we can assume this is handled in the additive module

private meta def find_sign_proof_by_trans_eq {unsigned signed : expr} (ed : eq_data unsigned signed) (sd : sign_data signed) : option (Σ e', sign_data e') :=
none

-- assumes sd is not an eq or diseq
private meta def find_sign_proof_by_trans_ineq {unsigned signed : expr} (id : ineq_data unsigned signed) (sd : sign_data signed) : option (Σ e', sign_data e') :=
let su := id.inq.to_comp,
    ss := sd.c.to_comp in
if su.dir = ss.dir && (su.is_strict || ss.is_strict)
--: ineq_data unsigned signed → sign_data signed → option (Σ e', sign_data e')
--| ⟨inq, prf⟩ ⟨c, prfs⟩ := none
--(id : ineq_data unsigned signed) (sd : sign_data signed) : option (Σ e', sign_data e') :=
--none

meta def find_sign_proof_by_trans (e : expr) : list expr → polya_state (option (Σ e', sign_data e'))
| [] := return none
| (h::t) :=
  do s ← get_sign_info h, ii ← get_ineqs e h,
  match ii, s with
  | _, none := return none
  | ineq_info.no_comps, _ := return none
  | ineq_info.equal ed, some sd :=
     match find_sign_proof_by_trans_eq ed sd with
     | some p := return $ some p
     | none := find_sign_proof_by_trans t
     end
  | ineq_info.one_comp id, some sd :=
    match find_sign_proof_by_trans_ineq id sd with
     | some p := return $ some p
     | none := find_sign_proof_by_trans t
     end
  | ineq_info.two_comps id1 id2, some sd :=
    let o := find_sign_proof_by_trans_ineq id1 sd <|> find_sign_proof_by_trans_ineq id2 sd in
    match o with
     | some p := return $ some p
     | none := find_sign_proof_by_trans t
     end
  end

meta def infer_sign_from_transitivity (e : expr) : polya_state (option (Σ e', sign_data e')) :=
do exs ← get_weak_signed_exprs,
   find_sign_proof_by_trans e exs

private meta def gather_new_sign_info_pass_two : polya_state (list Σ e, sign_data e) :=
do use ← get_unsigned_exprs,
   ose ← use.mmap infer_sign_from_transitivity,
   return $ reduce_option_list ose
-/

lemma rat_pow_pos_of_pos {q : ℚ} (h : q > 0) (z : ℤ) : rat.pow q z > 0 := sorry

lemma rat_pow_pos_of_neg_even {q : ℚ} (h : q < 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 0) : rat.pow q z > 0 := sorry

lemma rat_pow_neg_of_neg_odd {q : ℚ} (h : q < 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 1) : rat.pow q z < 0 := sorry

lemma rat_pow_nonneg_of_nonneg {q : ℚ} (h : q ≥ 0) (z : ℤ) : rat.pow q z ≥ 0 := sorry

lemma rat_pow_nonneg_of_nonpos_even {q : ℚ} (h : q ≤ 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 0) : rat.pow q z ≥ 0 := sorry

lemma rat_pow_nonpos_of_nonpos_odd {q : ℚ} (h : q ≤ 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 1) : rat.pow q z ≤ 0 := sorry

lemma rat_pow_zero_of_zero {q : ℚ} (h : q = 0) (z : ℤ) : rat.pow q z = 0 := sorry

lemma rat_pow_zero (q : ℚ) : rat.pow q 0 = 0 := sorry

lemma rat_pow_pos_of_ne_even {q : ℚ} (h : q ≠ 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 0) : rat.pow q z > 0 := sorry

lemma rat_pow_ne_of_ne_odd {q : ℚ} (h : q ≠ 0) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 1) : rat.pow q z ≠ 0 := sorry

lemma rat_pow_nonneg_of_pos_even (q : ℚ) {z : ℤ} (hz1 : z > 0) (hz2 : z % 2 = 0) : rat.pow q z ≥ 0 := sorry

-- given a proof that e > 0, proves that rat.pow e z > 0.
private meta def pos_pow_tac (pf : expr) (z : ℤ) : tactic expr :=
tactic.mk_app ``rat_pow_pos_of_pos [pf, `(z)]

private meta def nonneg_pow_tac (pf : expr) (z : ℤ) : tactic expr :=
tactic.mk_app ``rat_pow_nonneg_of_nonneg [pf, `(z)]

-- given a proof that e < 0, proves that rat.pow e z has the right sign
private meta def neg_pow_tac (e pf : expr) (z : ℤ) : tactic expr :=
if z > 0 then
  do zpp ← mk_int_sign_pf z, zmp ← mk_int_mod_pf z,--tactic.to_expr ``(by gen_comp_val : %%(reflect z) > 0),
     tactic.mk_mapp (if z % 2 = 0 then ``rat_pow_pos_of_neg_even else ``rat_pow_neg_of_neg_odd) [pf, none, zpp, zmp]
else if z = 0 then tactic.mk_app ``rat_pow_zero [e]
else tactic.fail "neg_pow_tac failed, neg expr to neg power"

-- given a proof that e ≤ 0, proves that rat.pow e z has the right sign
private meta def nonpos_pow_tac (e pf : expr) (z : ℤ) : tactic expr :=
if z > 0 then
  do zpp ← mk_int_sign_pf z, zmp ← mk_int_mod_pf z,--tactic.to_expr ``(by gen_comp_val : %%(reflect z) > 0),
     tactic.mk_mapp (if z % 2 = 0 then ``rat_pow_nonneg_of_nonpos_even else ``rat_pow_nonpos_of_nonpos_odd) [pf, none, zpp, zmp]
else if z = 0 then tactic.mk_app ``rat_pow_zero [e]
else tactic.fail "neg_pow_tac failed, neg expr to neg power"

private meta def ne_pow_tac (e pf : expr) (z : ℤ) : tactic expr :=
if z > 0 then
  do zpp ← mk_int_sign_pf z, zmp ← mk_int_mod_pf z,--tactic.to_expr ``(by gen_comp_val : %%(reflect z) > 0),
     tactic.mk_mapp (if z % 2 = 0 then ``rat_pow_pos_of_ne_even else ``rat_pow_ne_of_ne_odd) [pf, none, zpp, zmp]
else if z = 0 then tactic.mk_app ``rat_pow_zero [e]
else tactic.fail "neg_pow_tac failed, neg expr to neg power"

private meta def even_pow_tac (e : expr) (z : ℤ) : tactic expr :=
if z > 0 then
   do --tactic.trace "in ept", tactic.trace e,
      zpp ← mk_int_sign_pf z, zmp ← mk_int_mod_pf z,
      tactic.mk_mapp ``rat_pow_nonneg_of_pos_even [e, none, zpp, zmp]
else if z = 0 then tactic.mk_app ``rat_pow_zero [e]
else tactic.fail "even_pow_tac failed, cannot handle neg power"

-- assumes pf is the prod form of e and has only one component
private meta def gather_new_sign_info_pass_two_aux (e : expr) (pf : prod_form) : polya_state $ option (Σ e', sign_data e') :=
match pf.exps.to_list with
| [(e', pow)] :=
  do si ← get_sign_info (/-trace_val-/ ("e'", e')).2,
     match si with
     | some ⟨gen_comp.gt, pf⟩ := return $ some ⟨e, ⟨gen_comp.gt, sign_proof.adhoc _ _ (do s ← format_sign e' gen_comp.gt, return ⟨s, "inferred from other sign data", []⟩) (do pf' ← pf.reconstruct, pos_pow_tac pf' pow)⟩⟩
     | some ⟨gen_comp.ge, pf⟩ := return $ some ⟨e, ⟨gen_comp.ge, sign_proof.adhoc _ _ (do s ← format_sign e' gen_comp.ge, return ⟨s, "inferred from other sign data", []⟩) (do pf' ← pf.reconstruct, nonneg_pow_tac pf' pow)⟩⟩
     | some ⟨gen_comp.lt, pf⟩ :=
       if pow ≥ 0 then
         let tac : tactic expr := (do pf' ← pf.reconstruct, neg_pow_tac e' pf' pow),
             c := (if pow = 0 then gen_comp.eq else if pow % 2 = 0 then gen_comp.gt else gen_comp.lt) in
         return $ some ⟨e, ⟨c, sign_proof.adhoc _ _ (do s ← format_sign e c, return ⟨s, "inferred from other sign data", []⟩) tac⟩⟩
       else return none
     | some ⟨gen_comp.le, pf⟩ :=
       if pow ≥ 0 then
         let tac : tactic expr := (do pf' ← pf.reconstruct, nonpos_pow_tac e' pf' pow),
             c := (if pow = 0 then gen_comp.eq else if pow % 2 = 0 then gen_comp.gt else gen_comp.lt) in
         return $ some ⟨e, ⟨c, sign_proof.adhoc _ _ (do s ← format_sign e c, return ⟨s, "inferred from other sign data", []⟩) tac⟩⟩
       else return none
     | some ⟨gen_comp.eq, pf⟩ := return $ some ⟨e, ⟨gen_comp.eq, sign_proof.adhoc _ _ (do s ← format_sign e gen_comp.eq, return ⟨s, "inferred from other sign data", []⟩) (do pf' ← pf.reconstruct, tactic.mk_app ``rat_pow_zero [pf', `(pow)])⟩⟩
     | some ⟨gen_comp.ne, pf⟩ :=
       if pow ≥ 0 then
         let tac : tactic expr := (do pf' ← pf.reconstruct, ne_pow_tac e' pf' pow),
             c := (if pow = 0 then gen_comp.eq else if pow % 2 = 0 then gen_comp.gt else gen_comp.ne) in
         return $ some ⟨e, ⟨c, sign_proof.adhoc _ _ (do s ← format_sign e c, return ⟨s, "inferred from other sign data", []⟩) tac⟩⟩
       else return none
     | none :=
       if (pow ≥ 0) && (pow % 2 = 0) then
          let c := if pow = 0 then gen_comp.eq else gen_comp.ge in
          return $ some ⟨e, ⟨c, sign_proof.adhoc _ _ (do s ← format_sign e c, return ⟨s, "inferred from other sign data", []⟩) (even_pow_tac e' pow)⟩⟩
       else return none
     end
| _ := return none
end

-- get sign info for power exprs
private meta def gather_new_sign_info_pass_two : polya_state (list Σ e, sign_data e) :=
do exs ← get_mul_defs,
   let exs := (/-trace_val-/ ("of length one:", exs.filter (λ e, e.2.exps.size = 1))).2,
   list.reduce_option <$> exs.mmap (λ p, gather_new_sign_info_pass_two_aux p.1 p.2)

private meta def gather_new_sign_info : polya_state (list Σ e, sign_data e) :=
do l1 ← gather_new_sign_info_pass_one,
   l2 ← gather_new_sign_info_pass_two,
   return $ l1.append ((/-trace_val-/ ("THIS IS L2", l2)).2)

private meta def mk_ineq_list (cmps : list prod_form_comp_data) : mul_state (list Σ lhs rhs, ineq_data lhs rhs) :=
do il ← cmps.mmap (λ pfcd, pfcd.to_ineq_data),
   return $ (/-trace_val-/ ("made ineq list: ", il.join)).2

private meta def mk_eq_list (cmps : list prod_form_comp_data) : mul_state (list Σ lhs rhs, eq_data lhs rhs) :=
do il ← cmps.mmap (λ pfcd, pfcd.to_eq_data),
   return $ list.reduce_option il

private meta def mk_ineq_list_of_unelimed (cmps : list prod_form_comp_data) (start : rb_set prod_form_comp_data := mk_rb_set) : mul_state (rb_set prod_form_comp_data × list Σ lhs rhs, ineq_data lhs rhs) :=
do s ← prod_form.elim_list_set cmps start,
   l ← mk_ineq_list s.to_list,
   return (s, l)

meta def prod_form.add_new_ineqs (start : rb_set prod_form_comp_data := mk_rb_set) : polya_state (rb_set prod_form_comp_data) :=
do --new_sign_info ← gather_new_sign_info,
   --new_sign_info.mmap (λ sig, add_sign sig.2),
   is_contr ← contr_found,
   if is_contr then return start else do
   gather_new_sign_info >>= list.mmap (λ sig, add_sign $ /-trace_val-/ sig.2),
   sfcds ← /-trace_val <$>-/ mk_pfcd_list,
   ms ← mk_mul_state,
   let ((pfcs, ineqs), _) := (mk_ineq_list_of_unelimed sfcds start).run ms,
   monad.mapm'
    (λ s : Σ lhs rhs, ineq_data lhs rhs, add_ineq s.2.2)
    ineqs,
   return pfcs -- TODO: FIX RETURN

end bb_process

end polya

author: robertylewis


text:
import ..list data.rat

universe u

variables {α β: Type}

class dense_linear_order (α : Type) extends decidable_linear_order α :=
(inh : inhabited α)
(dense : ∀ {x z : α}, x < z → ∃ (y : α), x < y ∧ y < z)
(exists_lt : ∀ (y : α), ∃ (x : α), x < y)
(exists_gt : ∀ (x : α), ∃ (y : α), x < y)

open dense_linear_order

lemma dense_of_lof [linear_ordered_field α] :
  ∀ {x z : α}, x < z → ∃ (y : α), x < y ∧ y < z :=
begin
  intros x z h, existsi ((x + z) / 2), constructor,
  { have h2 : (x + x) / 2 < (x + z) / 2,
    { apply div_lt_div_of_lt_of_pos, apply add_lt_add_left h,
      apply lt.trans zero_lt_one, apply two_gt_one },
    rw add_self_div_two at h2, apply h2 },
  { have h2 : (x + z) / 2 < (z + z) / 2,
    { apply div_lt_div_of_lt_of_pos, apply add_lt_add_right h,
      apply lt.trans zero_lt_one, apply two_gt_one },
    rw add_self_div_two at h2, apply h2 },
end

lemma exists_lt_of_lof [linear_ordered_field α] :  ∀ (y : α), ∃ (x : α), x < y :=
begin intro y, existsi (y - 1), apply sub_lt_self, apply zero_lt_one end

lemma exists_gt_of_lof [linear_ordered_field α] :  ∀ (x : α), ∃ (y : α), x < y :=
begin intro y, existsi (y + 1), apply lt_add_of_pos_right, apply zero_lt_one, end

instance inh_dom [dense_linear_order β] : inhabited β := dense_linear_order.inh β

lemma exists_upper_bound [dense_linear_order β] :
∀ (bs : list β), ∃ x, ∀ b ∈ bs, b < x
| [] := begin existsi (default β), intros b hb, cases hb end
| (b::bs) :=
  begin
    cases (exists_upper_bound bs) with x hx, by_cases (b < x),
    { existsi x, intros b' hb', cases hb',
      {subst hb', apply h}, {apply hx _ hb'} },
    {
      cases (exists_gt b) with y hy, existsi y, intros b' hb', cases hb',
      {subst hb', apply hy},
      {apply lt.trans (hx _ hb'), apply lt_of_le_of_lt (le_of_not_lt h) hy}
    }
  end

lemma exists_lower_bound [dense_linear_order β] :
∀ (bs : list β), ∃ x, ∀ b ∈ bs, x < b
| [] := begin existsi (default β), intros b hb, cases hb end
| (b::bs) :=
  begin
    cases (exists_lower_bound bs) with x hx, by_cases (x < b),
    { existsi x, intros b' hb', cases hb',
      {subst hb', apply h}, {apply hx _ hb'} },
    {
      cases (exists_lt b) with y hy, existsi y, intros b' hb', cases hb',
      {subst hb', apply hy},
      {apply lt.trans _ (hx _ hb'), apply lt_of_lt_of_le hy (le_of_not_lt h)}
    }
  end

instance rat.dense_linear_order : dense_linear_order rat :=
{ inh := ⟨0⟩,
  dense := @dense_of_lof _ _,
  exists_lt := @exists_lt_of_lof _ _,
  exists_gt := @exists_gt_of_lof _ _ }

author: skbaek

repo: cooper

save_path: github-repos/lean/skbaek-cooper