Approximation tactic in lean4

Approx.lean

import Mathlib.Tactic.NormNum
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.SlimCheck

namespace Tactic

namespace Approx

def RoundDown (a b : ℤ) : Prop := 2 * b ≤ a
#align tactic.approx.round_down Tactic.Approx.RoundDown

def RoundUp (a b : ℤ) : Prop := a ≤ 2 * b
#align tactic.approx.round_up Tactic.Approx.RoundUp

theorem RoundDown.weak {a b a' b'} (h : RoundDown a b) (ha : a ≤ a') (hb : b' ≤ b) :
    RoundDown a' b' :=
  ((mul_le_mul_left two_pos (α := ℤ)).2 hb).trans <| le_trans h ha
#align tactic.approx.round_down.weak Tactic.Approx.RoundDown.weak

theorem RoundUp.weak {a b a' b'} (h : RoundUp a b) (ha : a' ≤ a) (hb : b ≤ b') : RoundUp a' b' :=
  ha.trans <| le_trans h <| (mul_le_mul_left two_pos (α := ℤ)).2 hb
#align tactic.approx.round_up.weak Tactic.Approx.RoundUp.weak

theorem RoundDown.zero : RoundDown 0 0 := by unfold RoundDown; decide
#align tactic.approx.round_down.zero Tactic.Approx.RoundDown.zero

theorem RoundDown.one : RoundDown 1 0 := by unfold RoundDown; decide
#align tactic.approx.round_down.one Tactic.Approx.RoundDown.one

theorem RoundDown.neg_one : RoundDown (-1) (-1) := by unfold RoundDown; decide
#align tactic.approx.round_down.neg_one Tactic.Approx.RoundDown.neg_one

theorem RoundDown.bit0_pos (a) : RoundDown (bit0 a) a :=
  (bit0_eq_two_mul _).ge
#align tactic.approx.round_down.bit0_pos Tactic.Approx.RoundDown.bit0_pos

theorem RoundDown.bit0_neg (a) : RoundDown (-bit0 a) (-a) := by
  rw [← _root_.bit0_neg]; apply RoundDown.bit0_pos
#align tactic.approx.round_down.bit0_neg Tactic.Approx.RoundDown.bit0_neg

theorem RoundDown.bit1_pos (a) : RoundDown (bit1 a) a :=
  sorry -- (RoundDown.bit0_pos a).weak (NormNum.le_bit0_bit1 _ _ le_rfl) le_rfl
#align tactic.approx.round_down.bit1_pos Tactic.Approx.RoundDown.bit1_pos

theorem RoundDown.bit1_neg {a b} (h : a + 1 = b) : RoundDown (-bit1 a) (-b) := by
  simp [RoundDown, ← bit0_eq_two_mul, bit0_neg]
  sorry -- apply NormNum.le_bit1_bit0; exact_mod_cast h.le
#align tactic.approx.round_down.bit1_neg Tactic.Approx.RoundDown.bit1_neg

theorem RoundUp.zero : RoundUp 0 0 := by unfold RoundUp; decide
#align tactic.approx.round_up.zero Tactic.Approx.RoundUp.zero

theorem RoundUp.one : RoundUp 1 1 := by unfold RoundUp; decide
#align tactic.approx.round_up.one Tactic.Approx.RoundUp.one

theorem RoundUp.neg_one : RoundUp (-1) 0 := by unfold RoundUp; decide
#align tactic.approx.round_up.neg_one Tactic.Approx.RoundUp.neg_one

theorem RoundUp.bit0_pos (a) : RoundUp (bit0 a) a :=
  (bit0_eq_two_mul _).le
#align tactic.approx.round_up.bit0_pos Tactic.Approx.RoundUp.bit0_pos

theorem RoundUp.bit0_neg (a) : RoundUp (-bit0 a) (-a) := by
  rw [← _root_.bit0_neg]; apply RoundUp.bit0_pos
#align tactic.approx.round_up.bit0_neg Tactic.Approx.RoundUp.bit0_neg

theorem RoundUp.bit1_pos {a b} (h : a + 1 = b) : RoundUp (bit1 a) b :=
  by
  simp [RoundUp, ← bit0_eq_two_mul]
  sorry -- apply NormNum.le_bit1_bit0; exact_mod_cast h.le
#align tactic.approx.round_up.bit1_pos Tactic.Approx.RoundUp.bit1_pos

theorem RoundUp.bit1_neg (a) : RoundUp (-bit1 a) (-a) :=
  sorry -- (RoundUp.bit0_neg a).weak (neg_le_neg <| NormNum.le_bit0_bit1 _ _ le_rfl) le_rfl
#align tactic.approx.round_up.bit1_neg Tactic.Approx.RoundUp.bit1_neg

def Approx (n lo hi : ℤ) (x : ℝ) : Prop :=
  (lo / 2 ^ n : ℝ) ≤ x ∧ x ≤ hi / 2 ^ n
#align tactic.approx.approx Tactic.Approx.Approx

theorem bit0_neg (a : ℤ) : bit0 (-a) = -bit0 a := _root_.bit0_neg _
#align tactic.approx.bit0_neg Tactic.Approx.bit0_neg

theorem Approx.up' {n lo hi lo' hi' : ℤ} {x : ℝ} (hlo : 2 * lo = lo') (hhi : 2 * hi = hi') :
    Approx (n + 1) lo' hi' x ↔ Approx n lo hi x := by
  simp [Approx, ← hlo, ← hhi, zpow_add_one₀ (two_ne_zero' ℝ), mul_comm, fun a b =>
    mul_div_mul_left a b (two_ne_zero' ℝ)]
  sorry
#align tactic.approx.approx.up' Tactic.Approx.Approx.up'

theorem Approx.le {n lo hi : ℤ} {x : ℝ} (h : Approx n lo hi x) : lo ≤ hi :=
  by
  rw [← @Int.cast_le ℝ, ← div_le_div_right (zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) n)]
  exact h.1.trans h.2
#align tactic.approx.approx.le Tactic.Approx.Approx.le

theorem Approx.weak {n lo hi lo' hi' : ℤ} {x : ℝ} (h : Approx n lo hi x) (hlo : lo' ≤ lo)
    (hhi : hi ≤ hi') : Approx n lo' hi' x :=
  by
  rw [← @Int.cast_le ℝ, ← div_le_div_right (zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) n)] at hlo hhi
  exact ⟨hlo.trans h.1, h.2.trans hhi⟩
#align tactic.approx.approx.weak Tactic.Approx.Approx.weak

theorem Approx.to_le {n xlo xhi ylo yhi : ℤ} {x y : ℝ} (hx : Approx n xlo xhi x)
    (hy : Approx n ylo yhi y) (h : xhi ≤ ylo) : x ≤ y :=
  haveI n0 := zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) n
  hx.2.trans (((div_le_div_right n0).2 (Int.cast_le.2 h)).trans hy.1)
#align tactic.approx.approx.to_le Tactic.Approx.Approx.to_le

theorem Approx.to_lt {n xlo xhi ylo yhi : ℤ} {x y : ℝ} (hx : Approx n xlo xhi x)
    (hy : Approx n ylo yhi y) (h : xhi < ylo) : x < y :=
  haveI n0 := zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) n
  hx.2.trans_lt (((div_lt_div_right n0).2 (Int.cast_lt.2 h)).trans_le hy.1)
#align tactic.approx.approx.to_lt Tactic.Approx.Approx.to_lt

theorem Approx.to_lt₂ {n xlo xhi ylo yhi zlo zhi : ℤ} {x y z : ℝ} (hx : Approx n xlo xhi x)
    (hy : Approx n ylo yhi y) (hz : Approx n zlo zhi z) (h₁ : xhi < ylo) (h₂ : yhi < zlo) :
    x < y ∧ y < z :=
  ⟨hx.to_lt hy h₁, hy.to_lt hz h₂⟩
#align tactic.approx.approx.to_lt₂ Tactic.Approx.Approx.to_lt₂

theorem Approx.of_exact {n a : ℤ} {x x' : ℝ} (hx : Approx n a a x) (h : (a : ℝ) / 2 ^ n = x') :
    x = x' :=
  (le_antisymm hx.2 hx.1).trans h
#align tactic.approx.approx.of_exact Tactic.Approx.Approx.of_exact

theorem Approx.approx {n lo hi lo' hi' zlo zhi : ℤ} {x y z : ℝ} (hx : Approx n lo hi x)
    (xy : |x - y| ≤ z) (hz : Approx n zlo zhi z) (hlo : lo - zhi = lo') (hhi : hi + zhi = hi') :
    Approx n lo' hi' y :=
  by
  obtain ⟨h₁, h₂⟩ := abs_sub_le_iff.1 (xy.trans hz.2)
  constructor
  · rw [← hlo, Int.cast_sub, ← div_sub_div_same]
    exact (sub_le_sub_right hx.1 _).trans (sub_le_comm.1 h₁)
  · rw [← hhi, Int.cast_add, ← div_add_div_same]
    refine' le_trans (sub_le_iff_le_add'.1 h₂) (add_le_add_right hx.2 _)
#align tactic.approx.approx.approx Tactic.Approx.Approx.approx

theorem Approx.of_integer {n ll lo hi hh z zl zr : ℤ} {x : ℝ} (hx : Approx n lo hi x)
    (ezl : z - 1 = zl) (ezr : z + 1 = zr) (hzl : Approx n ll ll zl) (hzr : Approx n hh hh zr)
    (h₁ : ll < lo) (h₂ : hi < hh) (h : ∃ z : ℤ, x = z) : x = z :=
  by
  obtain ⟨rfl, rfl, ⟨a, rfl⟩⟩ := ezl, ezr, h
  congr;
  exact
    le_antisymm (Int.lt_add_one_iff.1 (Int.cast_lt.1 (hx.to_lt hzr h₂)))
      (Int.sub_one_lt_iff.1 (Int.cast_lt.1 (hzl.to_lt hx h₁)))
#align tactic.approx.approx.of_integer Tactic.Approx.Approx.of_integer

theorem Approx.up {n lo hi lo' hi' : ℤ} {x : ℝ} (h : Approx n lo hi x) (hlo : bit0 lo = lo')
    (hhi : bit0 hi = hi') : Approx (n + 1) lo' hi' x := by
  rw [bit0_eq_two_mul] at hlo hhi; exact (Approx.up' hlo hhi).2 h
#align tactic.approx.approx.up Tactic.Approx.Approx.up

theorem Approx.down {n lo hi lo' hi' : ℤ} {x : ℝ} (h : Approx n lo hi x) (hlo : RoundDown lo lo')
    (hhi : RoundUp hi hi') : Approx (n - 1) lo' hi' x :=
  by
  have := h.weak hlo hhi
  rwa [← sub_add_cancel n 1, Approx.up' rfl rfl] at this
#align tactic.approx.approx.down Tactic.Approx.Approx.down

theorem Approx.assume {n ll lh hl hh : ℤ} {xl x xh : ℝ} (hxl : Approx n ll lh xl)
    (hxh : Approx n hl hh xh) (hlo : xl ≤ x) (hhi : x ≤ xh) : Approx n ll hh x :=
  ⟨le_trans hxl.1 hlo, le_trans hhi hxh.2⟩
#align tactic.approx.approx.assume Tactic.Approx.Approx.assume

theorem Approx.eq_zero (n) {x} : Approx n 0 0 x ↔ x = 0 := by
  simp [Approx, le_antisymm_iff, and_comm]
#align tactic.approx.approx.eq_zero Tactic.Approx.Approx.eq_zero

theorem Approx.zero (n) : Approx n 0 0 0 :=
  (Approx.eq_zero _).2 rfl
#align tactic.approx.approx.zero Tactic.Approx.Approx.zero

theorem Approx.const {a : ℤ} {x : ℝ} (h : ↑a = x) : Approx 0 a a x := by simp [Approx, ← h]
#align tactic.approx.approx.const Tactic.Approx.Approx.const

theorem Approx.neg {n lo hi lo' hi' : ℤ} {x : ℝ} (h : Approx n lo hi x) (hlo : -lo = hi')
    (hhi : -hi = lo') : Approx n lo' hi' (-x) := by
  simpa [Approx, ← hlo, ← hhi, neg_div, and_comm] using h
#align tactic.approx.approx.neg Tactic.Approx.Approx.neg

theorem Approx.add {n xlo xhi ylo yhi lo hi : ℤ} {x y : ℝ} (hx : Approx n xlo xhi x)
    (hy : Approx n ylo yhi y) (hlo : xlo + ylo = lo) (hhi : xhi + yhi = hi) :
    Approx n lo hi (x + y) := by
  simpa [Approx, ← hlo, ← hhi, add_div] using
    And.intro (add_le_add hx.1 hy.1) (add_le_add hx.2 hy.2)
#align tactic.approx.approx.add Tactic.Approx.Approx.add

theorem Approx.sub {n xlo xhi ylo yhi lo hi : ℤ} {x y : ℝ} (hx : Approx n xlo xhi x)
    (hy : Approx n ylo yhi y) (hlo : xlo - yhi = lo) (hhi : xhi - ylo = hi) :
    Approx n lo hi (x - y) :=
  Approx.add hx (Approx.neg hy rfl rfl) hlo hhi
#align tactic.approx.approx.sub Tactic.Approx.Approx.sub

def MulBound (xlo xhi ylo yhi lo hi : ℤ) : Prop :=
  xlo ≤ xhi → ylo ≤ yhi →
  (lo ≤ xlo * ylo ∧ xlo * ylo ≤ hi) ∧ (lo ≤ xlo * yhi ∧ xlo * yhi ≤ hi) ∧
  (lo ≤ xhi * ylo ∧ xhi * ylo ≤ hi) ∧ (lo ≤ xhi * yhi ∧ xhi * yhi ≤ hi)
#align tactic.approx.mul_bound Tactic.Approx.MulBound

theorem MulBound.exact {x y z : ℤ} (h : x * y = z) : MulBound x x y y z z := fun hx hy => by
  suffices h; exact ⟨h, h, h, h⟩; exact ⟨h.ge, h.le⟩
#align tactic.approx.mul_bound.exact Tactic.Approx.MulBound.exact

theorem MulBound.pos_pos {xlo xhi ylo yhi lo hi : ℤ} (x0 : 0 ≤ xlo) (y0 : 0 ≤ ylo)
    (hlo : xlo * ylo = lo) (hhi : xhi * yhi = hi) : MulBound xlo xhi ylo yhi lo hi := fun hx hy =>
  by
  have lll := hlo.ge; have hhh := hhi.le
  have llh := lll.trans (mul_le_mul_of_nonneg_left hy x0)
  have lhl := lll.trans (mul_le_mul_of_nonneg_right hx y0)
  have lhh := lhl.trans (mul_le_mul_of_nonneg_left hy (x0.trans hx))
  have hhl := (mul_le_mul_of_nonneg_left hy (x0.trans hx)).trans hhh
  have hlh := (mul_le_mul_of_nonneg_right hx (y0.trans hy)).trans hhh
  have hll := (mul_le_mul_of_nonneg_right hx y0).trans hhl
  exact ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩
#align tactic.approx.mul_bound.pos_pos Tactic.Approx.MulBound.pos_pos

theorem MulBound.pos_neg {xlo xhi ylo yhi lo hi : ℤ} (x0 : 0 ≤ xlo) (y0 : yhi ≤ 0)
    (hlo : xhi * ylo = lo) (hhi : xlo * yhi = hi) : MulBound xlo xhi ylo yhi lo hi := fun hx hy =>
  by
  have lhl := hlo.ge; have hlh := hhi.le
  have lll := lhl.trans (mul_le_mul_of_nonpos_right hx (hy.trans y0))
  have llh := lll.trans (mul_le_mul_of_nonneg_left hy x0)
  have lhh := lhl.trans (mul_le_mul_of_nonneg_left hy (x0.trans hx))
  have hhh := (mul_le_mul_of_nonpos_right hx y0).trans hlh
  have hhl := (mul_le_mul_of_nonneg_left hy (x0.trans hx)).trans hhh
  have hll := (mul_le_mul_of_nonneg_left hy x0).trans hlh
  exact ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩
#align tactic.approx.mul_bound.pos_neg Tactic.Approx.MulBound.pos_neg

theorem MulBound.neg_pos {xlo xhi ylo yhi lo hi : ℤ} (x0 : xhi ≤ 0) (y0 : 0 ≤ ylo)
    (hlo : xlo * yhi = lo) (hhi : xhi * ylo = hi) : MulBound xlo xhi ylo yhi lo hi := fun hx hy =>
  by
  have llh := hlo.ge; have hhl := hhi.le
  have lll := llh.trans (mul_le_mul_of_nonpos_left hy (hx.trans x0))
  have lhl := lll.trans (mul_le_mul_of_nonneg_right hx y0)
  have lhh := llh.trans (mul_le_mul_of_nonneg_right hx (y0.trans hy))
  have hhh := (mul_le_mul_of_nonpos_left hy x0).trans hhl
  have hlh := (mul_le_mul_of_nonneg_right hx (y0.trans hy)).trans hhh
  have hll := (mul_le_mul_of_nonneg_right hx y0).trans hhl
  exact ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩
#align tactic.approx.mul_bound.neg_pos Tactic.Approx.MulBound.neg_pos

theorem MulBound.neg_neg {xlo xhi ylo yhi lo hi : ℤ} (x0 : xhi ≤ 0) (y0 : yhi ≤ 0)
    (hlo : xhi * yhi = lo) (hhi : xlo * ylo = hi) : MulBound xlo xhi ylo yhi lo hi := fun hx hy =>
  by
  have lhh := hlo.ge; have hll := hhi.le
  have lhl := lhh.trans (mul_le_mul_of_nonpos_left hy x0)
  have llh := lhh.trans (mul_le_mul_of_nonpos_right hx y0)
  have lll := llh.trans (mul_le_mul_of_nonpos_left hy (hx.trans x0))
  have hlh := (mul_le_mul_of_nonpos_left hy (hx.trans x0)).trans hll
  have hhl := (mul_le_mul_of_nonpos_right hx (hy.trans y0)).trans hll
  have hhh := (mul_le_mul_of_nonpos_right hx y0).trans hlh
  exact ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩
#align tactic.approx.mul_bound.neg_neg Tactic.Approx.MulBound.neg_neg

theorem MulBound.mk {xlo xhi ylo yhi ll lh hl hh lo hi : ℤ} (ell : xlo * ylo = ll)
    (elh : xlo * yhi = lh) (ehl : xhi * ylo = hl) (ehh : xhi * yhi = hh) (lll : lo ≤ ll)
    (hll : ll ≤ hi) (llh : lo ≤ lh) (hlh : lh ≤ hi) (lhl : lo ≤ hl) (hhl : hl ≤ hi) (lhh : lo ≤ hh)
    (hhh : hh ≤ hi) : MulBound xlo xhi ylo yhi lo hi := fun hx hy => by
  rw [ell, elh, ehl, ehh]
  exact ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩
#align tactic.approx.mul_bound.mk Tactic.Approx.MulBound.mk

theorem Approx.mul {m n xlo xhi ylo yhi lo hi : ℤ} {x y : ℝ} (hx : Approx m xlo xhi x)
    (hy : Approx n ylo yhi y) (hbd : MulBound xlo xhi ylo yhi lo hi) :
    Approx (m + n) lo hi (x * y) := by
  obtain ⟨⟨lll, hll⟩, ⟨llh, hlh⟩, ⟨lhl, hhl⟩, ⟨lhh, hhh⟩⟩ := hbd hx.le hy.le
  have : ∀ a b : ℤ, (↑(a * b) : ℝ) / 2 ^ (m + n) = a / 2 ^ m * (b / 2 ^ n) := by
    intros; rw [zpow_add₀ (two_ne_zero' ℝ), Int.cast_mul, mul_div_mul_comm]
  rw [← @Int.cast_le ℝ, ← div_le_div_right (zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) (m + n)),
    this] at lll hll llh hlh lhl hhl lhh hhh
  obtain x0 | x0 := le_total x 0 <;> constructor
  · refine' le_trans _ (mul_le_mul_of_nonpos_left hy.2 x0)
    obtain y0 | y0 := le_total ((yhi : ℝ) / 2 ^ n) 0
    · exact le_trans lhh (mul_le_mul_of_nonpos_right hx.2 y0)
    · exact le_trans llh (mul_le_mul_of_nonneg_right hx.1 y0)
  · refine' le_trans (mul_le_mul_of_nonpos_left hy.1 x0) _
    obtain y0 | y0 := le_total ((ylo : ℝ) / 2 ^ n) 0
    · exact le_trans (mul_le_mul_of_nonpos_right hx.1 y0) hll
    · exact le_trans (mul_le_mul_of_nonneg_right hx.2 y0) hhl
  · refine' le_trans _ (mul_le_mul_of_nonneg_left hy.1 x0)
    obtain y0 | y0 := le_total ((ylo : ℝ) / 2 ^ n) 0
    · exact le_trans lhl (mul_le_mul_of_nonpos_right hx.2 y0)
    · exact le_trans lll (mul_le_mul_of_nonneg_right hx.1 y0)
  · refine' le_trans (mul_le_mul_of_nonneg_left hy.2 x0) _
    obtain y0 | y0 := le_total ((yhi : ℝ) / 2 ^ n) 0
    · exact le_trans (mul_le_mul_of_nonpos_right hx.1 y0) hlh
    · exact le_trans (mul_le_mul_of_nonneg_right hx.2 y0) hhh
#align tactic.approx.approx.mul Tactic.Approx.Approx.mul

theorem Approx.div {m n xlo xhi ylo yhi lo hi : ℤ} {x y : ℝ} (hx : Approx m xlo xhi x)
    (hy : Approx n ylo yhi y⁻¹) (hbd : MulBound xlo xhi ylo yhi lo hi) :
    Approx (m + n) lo hi (x / y) :=
  Approx.mul hx hy hbd
#align tactic.approx.approx.div Tactic.Approx.Approx.div

theorem Approx.inv_lem {m n lo hi lo' hi' : ℤ} {x p : ℝ} (hx : Approx m lo hi x)
    (hp : p = 2 ^ (m + n))
    (H : 0 < lo ∧ p ≤ ↑(lo * hi') ∧ ↑(hi * lo') ≤ p ∨ hi < 0 ∧ p ≤ ↑(hi * lo') ∧ ↑(lo * hi') ≤ p) :
    Approx n lo' hi' x⁻¹ := by
  have two_pos := (two_pos : 0 < (2 : ℝ))
  rw [zpow_add₀ two_pos.ne'] at hp
  have mn0 : (0 : ℝ) < 2 ^ m * 2 ^ n :=
    mul_pos (zpow_pos_of_pos two_pos _) (zpow_pos_of_pos two_pos _)
  obtain ⟨x0, hlo, hhi⟩ | ⟨x0, hlo, hhi⟩ := H <;> rw [Int.cast_mul, hp] at hlo hhi  <;>
        rw [← div_le_one mn0, ← div_mul_div_comm] at hhi  <;>
      rw [← one_le_div mn0, ← div_mul_div_comm] at hlo  <;>
    rw [← @Int.cast_lt ℝ, ← div_lt_div_right (zpow_pos_of_pos two_pos m), Int.cast_zero,
      zero_div] at x0
  · have x0' := x0.trans_le hx.1; constructor
    · obtain lo0 | lo0 := le_total ((lo' : ℝ) / 2 ^ n) 0
      · exact le_trans lo0 (inv_pos.2 x0').le
      rw [← one_div, le_div_iff' x0']
      exact le_trans (mul_le_mul_of_nonneg_right hx.2 lo0) hhi
    · have hi0 : 0 ≤ (hi' : ℝ) / 2 ^ n :=
        by
        rw [← div_le_iff' x0, one_div] at hlo
        exact le_trans (inv_nonneg.2 x0.le) hlo
      rw [← one_div, div_le_iff' x0']
      exact le_trans hlo (mul_le_mul_of_nonneg_right hx.1 hi0)
  · have x0' := hx.2.trans_lt x0; constructor
    · have lo0 : (lo' : ℝ) / 2 ^ n ≤ 0 :=
        by
        rw [← le_div_iff_of_neg' x0, one_div] at hlo
        exact le_trans hlo (inv_nonpos.2 x0.le)
      rw [← one_div, le_div_iff_of_neg' x0']
      refine' le_trans hlo (mul_le_mul_of_nonpos_right hx.2 lo0)
    · obtain hi0 | hi0 := le_total 0 ((hi' : ℝ) / 2 ^ n)
      · exact le_trans (inv_lt_zero.2 x0').le hi0
      rw [← one_div, div_le_iff_of_neg' x0']
      exact le_trans (mul_le_mul_of_nonpos_right hx.1 hi0) hhi
#align tactic.approx.approx.inv_lem Tactic.Approx.Approx.inv_lem

theorem Approx.inv_lem' {m n lo hi lo' hi' lh hl p2 : ℤ} {x : ℝ} {p : ℕ} (hx : Approx m lo hi x)
    (hp : (p : ℤ) = m + n) (hp2 : 2 ^ p = p2) (hlh : lo * hi' = lh) (hhl : hi * lo' = hl)
    (H : 0 < lo ∧ p2 ≤ lh ∧ hl ≤ p2 ∨ hi < 0 ∧ p2 ≤ hl ∧ lh ≤ p2) : Approx n lo' hi' x⁻¹ :=
  by
  substs hp2 hlh hhl
  have : ((2 ^ p : ℤ) : ℝ) = 2 ^ (m + n) := by rw [← hp]; norm_cast
  exact Approx.inv_lem hx this (by simpa only [Int.cast_le] using H)
#align tactic.approx.approx.inv_lem' Tactic.Approx.Approx.inv_lem'

nonrec theorem Approx.inv_zero {m n : ℤ} {x : ℝ} (hx : Approx m 0 0 x) : Approx n 0 0 x⁻¹ := by
  simp only [(Approx.eq_zero _).1 hx, inv_zero, Approx.zero]
#align tactic.approx.approx.inv_zero Tactic.Approx.Approx.inv_zero

theorem Approx.inv_pos {m n lo hi lo' hi' lh hl p2 : ℤ} {x : ℝ} {p : ℕ} (hx : Approx m lo hi x)
    (hp : (p : ℤ) = m + n) (x0 : 0 < lo) (hp2 : 2 ^ p = p2) (hlh : lo * hi' = lh)
    (hhl : hi * lo' = hl) (hlo : p2 ≤ lh) (hhi : hl ≤ p2) : Approx n lo' hi' x⁻¹ :=
  Approx.inv_lem' hx hp hp2 hlh hhl (Or.inl ⟨x0, hlo, hhi⟩)
#align tactic.approx.approx.inv_pos Tactic.Approx.Approx.inv_pos

theorem Approx.inv_neg {m n lo hi lo' hi' lh hl p2 : ℤ} {x : ℝ} {p : ℕ} (hx : Approx m lo hi x)
    (hp : (p : ℤ) = m + n) (x0 : hi < 0) (hp2 : 2 ^ p = p2) (hlh : lo * hi' = lh)
    (hhl : hi * lo' = hl) (hlo : p2 ≤ hl) (hhi : lh ≤ p2) : Approx n lo' hi' x⁻¹ :=
  Approx.inv_lem' hx hp hp2 hlh hhl (Or.inr ⟨x0, hlo, hhi⟩)
#align tactic.approx.approx.inv_neg Tactic.Approx.Approx.inv_neg

theorem Approx.inv_triv_pos {m n lo hi : ℤ} {x : ℝ} (hx : Approx m lo hi x)
    (hp : decide (m + n ≤ 0) = true) (x0 : 0 < lo) : Approx n 0 1 x⁻¹ :=
  by
  replace hp := Bool.of_decide_true hp
  refine' Approx.inv_lem hx rfl (Or.inl ⟨x0, _, _⟩) <;> simp
  · refine' le_trans _ (Int.cast_le.2 (Int.add_one_le_iff.2 x0))
    simpa only [zpow_zero, Int.cast_one, zero_add] using zpow_le_of_le one_le_two hp
  · exact (zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) _).le
#align tactic.approx.approx.inv_triv_pos Tactic.Approx.Approx.inv_triv_pos

theorem Approx.inv_triv_neg {m n lo hi : ℤ} {x : ℝ} (hx : Approx m lo hi x)
    (hp : decide (m + n ≤ 0) = true) (x0 : hi < 0) : Approx n (-1) 0 x⁻¹ :=
  by
  replace hp := Bool.of_decide_true hp
  refine' Approx.inv_lem hx rfl (Or.inr ⟨x0, _, _⟩) <;> simp
  · rw [← Int.cast_neg]; rw [← neg_pos] at x0
    refine' le_trans _ (Int.cast_le.2 (Int.add_one_le_iff.2 x0))
    simpa only [zpow_zero, Int.cast_one, zero_add] using zpow_le_of_le one_le_two hp
  · exact (zpow_pos_of_pos (two_pos : 0 < (2 : ℝ)) _).le
#align tactic.approx.approx.inv_triv_neg Tactic.Approx.Approx.inv_triv_neg

open Tactic Mathlib.Meta.NormNum

-- /-- Given `a`, proves `(b, |- round_down a b)` -/
-- unsafe def prove_round_down (ic : instance_cache) (a : expr) :
--     tactic (instance_cache × expr × expr) :=
--   match match_neg a with
--   | some a =>
--     match match_numeral a with
--     | match_numeral_result.one => pure (ic, q((-1 : ℤ)), q(RoundDown.neg_one))
--     | match_numeral_result.bit0 a =>
--       pure (ic, q((Neg.neg : ℤ → ℤ)).mk_app [a], q(RoundDown.bit0_neg).mk_app [a])
--     | match_numeral_result.bit1 a => do
--       let (ic, b, h) ← prove_succ' ic a
--       pure (ic, q((Neg.neg : ℤ → ℤ)).mk_app [b], q(@RoundDown.bit1_neg).mk_app [a, b, h])
--     | _ => failed
--   | none =>
--     match match_numeral a with
--     | match_numeral_result.zero => pure (ic, q((0 : ℤ)), q(RoundDown.zero))
--     | match_numeral_result.one => pure (ic, q((0 : ℤ)), q(RoundDown.one))
--     | match_numeral_result.bit0 a => pure (ic, a, q(RoundDown.bit0_pos).mk_app [a])
--     | match_numeral_result.bit1 a => pure (ic, a, q(@RoundDown.bit1_pos).mk_app [a])
--     | _ => failed
-- #align tactic.approx.prove_round_down Tactic.Approx.prove_round_down

-- /-- Given `a`, proves `(b, |- round_up a b)` -/
-- unsafe def prove_round_up (ic : instance_cache) (a : expr) :
--     tactic (instance_cache × expr × expr) :=
--   match match_neg a with
--   | some a =>
--     match match_numeral a with
--     | match_numeral_result.one => pure (ic, q((0 : ℤ)), q(RoundUp.neg_one))
--     | match_numeral_result.bit0 a =>
--       pure (ic, q((Neg.neg : ℤ → ℤ)).mk_app [a], q(RoundUp.bit0_neg).mk_app [a])
--     | match_numeral_result.bit1 a =>
--       pure (ic, q((Neg.neg : ℤ → ℤ)).mk_app [a], q(RoundUp.bit1_neg).mk_app [a])
--     | _ => failed
--   | none =>
--     match match_numeral a with
--     | match_numeral_result.zero => pure (ic, q((0 : ℤ)), q(RoundUp.zero))
--     | match_numeral_result.one => pure (ic, q((1 : ℤ)), q(RoundUp.one))
--     | match_numeral_result.bit0 a => pure (ic, a, q(RoundUp.bit0_pos).mk_app [a])
--     | match_numeral_result.bit1 a => do
--       let (ic, b, h) ← prove_succ' ic a
--       pure (ic, b, q(@RoundUp.bit1_pos).mk_app [a, b, h])
--     | _ => failed
-- #align tactic.approx.prove_round_up Tactic.Approx.prove_round_up

inductive ApproxExtra
  | mk
#align tactic.approx.approx_extra Tactic.Approx.ApproxExtra

inductive ApproxArgs
  | nil : ApproxArgs
  | prec : ℤ → ApproxArgs → ApproxArgs
  | unop : ApproxArgs → ApproxArgs
  | binop : ApproxArgs → ApproxArgs → ApproxArgs
  | extra : ApproxExtra → ApproxArgs
#align tactic.approx.approx_args Tactic.Approx.ApproxArgs

def ApproxArgs.getPrec : ApproxArgs → Option ℤ
  | ApproxArgs.prec n _ => some n
  | ApproxArgs.nil => none
  | ApproxArgs.unop _ => none
  | ApproxArgs.binop _ _ => none
  | ApproxArgs.extra _ => none
#align tactic.approx.approx_args.get_prec Tactic.Approx.ApproxArgs.getPrec

def ApproxArgs.getBinop : ApproxArgs → ApproxArgs × ApproxArgs
  | ApproxArgs.prec n p => p.getBinop
  | ApproxArgs.binop a b => (a, b)
  | _ => (ApproxArgs.nil, ApproxArgs.nil)
#align tactic.approx.approx_args.get_binop Tactic.Approx.ApproxArgs.getBinop

def ApproxArgs.getUnop : ApproxArgs → ApproxArgs
  | ApproxArgs.prec n p => p.getUnop
  | ApproxArgs.unop p => p
  | _ => ApproxArgs.nil
#align tactic.approx.approx_args.get_unop Tactic.Approx.ApproxArgs.getUnop

-- /-- Given `a : ℤ` proves `(b, |- bit0 a = b)` -/
-- unsafe def prove_bit0 : expr → expr × expr
--   | a =>
--     match match_neg a with
--     | some a => (q((Neg.neg : ℤ → ℤ)).mk_app [a], q(bit0_neg).mk_app [a])
--     | none =>
--       let b0 := q((bit0 : ℤ → ℤ)).mk_app [a]
--       (b0, q(@rfl ℤ).mk_app [b0])
-- #align tactic.approx.prove_bit0 Tactic.Approx.prove_bit0

-- /-- `set_prec tgt ic n en lo hi x hx`:
--   * `en` is the expression for `n`
--   * `hx : approx n lo hi x`
--   returns `(ic, lo', hi', |- approx tgt lo' hi' x)` -/
-- unsafe def set_prec (tgt : ℤ) :
--     instance_cache →
--       ℤ → expr → expr → expr → expr → expr → tactic (instance_cache × expr × expr × expr)
--   | ic, n, en, lo, hi, x, hx =>
--     if n < tgt then do
--       let (ic, en') ← ic.ofInt (n + 1)
--       let (lo', hlo) := prove_bit0 lo
--       let (hi', hhi) := prove_bit0 hi
--       set_prec ic (n + 1) en' lo' hi' x <|
--           q(@Approx.up).mk_app [en, lo, hi, lo', hi', x, hx, hlo, hhi]
--     else
--       if tgt < n then do
--         let (ic, en') ← ic.ofInt (n - 1)
--         let (ic, lo', hlo) ← prove_round_down ic lo
--         let (ic, hi', hhi) ← prove_round_up ic hi
--         set_prec ic (n - 1) en' lo' hi' x <|
--             q(@Approx.down).mk_app [en, lo, hi, lo', hi', x, hx, hlo, hhi]
--       else pure (ic, lo, hi, hx)
-- #align tactic.approx.set_prec tactic.approx.set_prec

-- unsafe def approx_fn :=
--   instance_cache → ℤ → expr → expr → tactic (instance_cache × expr × expr × expr)
-- #align tactic.approx.approx_fn tactic.approx.approx_fn

-- unsafe def eval_approx_neg (xfn : approx_fn) (n' : ℤ) (x : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, en') ← ic.ofInt n'
--     let (ic, lo, hi, hx) ← xfn ic n' en' x
--     let (ic, hi', hlo) ← prove_neg ic lo
--     let (ic, lo', hhi) ← prove_neg ic hi
--     set_prec n ic n' en' lo' hi' e <| q(@Approx.neg).mk_app [en', lo, hi, lo', hi', x, hx, hlo, hhi]
-- #align tactic.approx.eval_approx_neg tactic.approx.eval_approx_neg

-- unsafe def eval_approx_add (xfn yfn : approx_fn) (n' : ℤ) (x y : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, en') ← ic.ofInt n'
--     let (ic, xlo, xhi, hx) ← xfn ic n' en' x
--     let (ic, ylo, yhi, hy) ← yfn ic n' en' y
--     let (ic, lo, hlo) ← prove_add_rat' ic xlo ylo
--     let (ic, hi, hhi) ← prove_add_rat' ic xhi yhi
--     set_prec n ic n' en' lo hi e <|
--         q(@Approx.add).mk_app [en', xlo, xhi, ylo, yhi, lo, hi, x, y, hx, hy, hlo, hhi]
-- #align tactic.approx.eval_approx_add tactic.approx.eval_approx_add

-- unsafe def eval_approx_sub (xfn yfn : approx_fn) (n' : ℤ) (x y : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, en') ← ic.ofInt n'
--     let (ic, xlo, xhi, hx) ← xfn ic n' en' x
--     let (ic, ylo, yhi, hy) ← yfn ic n' en' y
--     let (ic, lo, hlo) ← prove_sub ic xlo yhi
--     let (ic, hi, hhi) ← prove_sub ic xhi ylo
--     set_prec n ic n' en' lo hi e <|
--         q(@Approx.sub).mk_app [en', xlo, xhi, ylo, yhi, lo, hi, x, y, hx, hy, hlo, hhi]
-- #align tactic.approx.eval_approx_sub tactic.approx.eval_approx_sub

-- /-- Given `xlo, xhi, ylo, yhi` proves `(lo, hi, |- mul_bound xlo xhi ylo yhi lo hi)` -/
-- unsafe def eval_mul_bound (ic : instance_cache) (exlo exhi eylo eyhi : expr) :
--     tactic (instance_cache × expr × expr × expr) := do
--   let xlo ← exlo.toInt
--   let xhi ← exhi.toInt
--   let ylo ← eylo.toInt
--   let yhi ← eyhi.toInt
--   let rxlo := Rat.ofInt xlo
--   let rxhi := Rat.ofInt xhi
--   let rylo := Rat.ofInt ylo
--   let ryhi := Rat.ofInt yhi
--   (if 0 ≤ xlo then do
--         let (ic, x0) ← prove_nonneg ic exlo
--         if 0 ≤ ylo then do
--             let (ic, y0) ← prove_nonneg ic eylo
--             let (ic, lo, hlo) ← prove_mul_rat ic exlo eylo rxlo rylo
--             let (ic, hi, hhi) ← prove_mul_rat ic exhi eyhi rxhi ryhi
--             pure
--                 (ic, lo, hi,
--                   q(@MulBound.pos_pos).mk_app [exlo, exhi, eylo, eyhi, lo, hi, x0, y0, hlo, hhi])
--           else
--             if yhi ≤ 0 then do
--               let (ic, y0) ← prove_le_rat ic eyhi q((0 : ℤ)) ryhi 0
--               let (ic, lo, hlo) ← prove_mul_rat ic exhi eylo rxhi rylo
--               let (ic, hi, hhi) ← prove_mul_rat ic exlo eyhi rxlo ryhi
--               pure
--                   (ic, lo, hi,
--                     q(@MulBound.pos_neg).mk_app [exlo, exhi, eylo, eyhi, lo, hi, x0, y0, hlo, hhi])
--             else failed
--       else
--         if xhi ≤ 0 then do
--           let (ic, x0) ← prove_le_rat ic exhi q((0 : ℤ)) rxhi 0
--           if 0 ≤ ylo then do
--               let (ic, y0) ← prove_nonneg ic eylo
--               let (ic, lo, hlo) ← prove_mul_rat ic exlo eyhi rxlo ryhi
--               let (ic, hi, hhi) ← prove_mul_rat ic exhi eylo rxhi rylo
--               pure
--                   (ic, lo, hi,
--                     q(@MulBound.neg_pos).mk_app [exlo, exhi, eylo, eyhi, lo, hi, x0, y0, hlo, hhi])
--             else
--               if yhi ≤ 0 then do
--                 let (ic, y0) ← prove_le_rat ic eyhi q((0 : ℤ)) ryhi 0
--                 let (ic, lo, hlo) ← prove_mul_rat ic exhi eyhi rxhi ryhi
--                 let (ic, hi, hhi) ← prove_mul_rat ic exlo eylo rxlo rylo
--                 pure
--                     (ic, lo, hi,
--                       q(@MulBound.neg_neg).mk_app
--                         [exlo, exhi, eylo, eyhi, lo, hi, x0, y0, hlo, hhi])
--               else failed
--         else failed) <|>
--       do
--       let (ic, ell, hell) ← prove_mul_rat ic exlo eylo rxlo rylo
--       let ll := xlo * ylo
--       let rll := Rat.ofInt ll
--       let (ic, elh, helh) ← prove_mul_rat ic exlo eyhi rxlo ryhi
--       let lh := xlo * yhi
--       let rlh := Rat.ofInt lh
--       let (ic, ehl, hehl) ← prove_mul_rat ic exhi eylo rxhi rylo
--       let hl := xhi * ylo
--       let rhl := Rat.ofInt hl
--       let (ic, ehh, hehh) ← prove_mul_rat ic exhi eyhi rxhi ryhi
--       let hh := xhi * yhi
--       let rhh := Rat.ofInt hh
--       let lo := min ll <| min lh <| min hl hh
--       let hi := max ll <| max lh <| max hl hh
--       let (ic, elo) ← ic lo
--       let (ic, ehi) ← ic hi
--       let rlo := Rat.ofInt lo
--       let rhi := Rat.ofInt hi
--       let (ic, lll) ← prove_le_rat ic elo ell rlo rll
--       let (ic, hll) ← prove_le_rat ic ell ehi rll rhi
--       let (ic, llh) ← prove_le_rat ic elo elh rlo rlh
--       let (ic, hlh) ← prove_le_rat ic elh ehi rlh rhi
--       let (ic, lhl) ← prove_le_rat ic elo ehl rlo rhl
--       let (ic, hhl) ← prove_le_rat ic ehl ehi rhl rhi
--       let (ic, lhh) ← prove_le_rat ic elo ehh rlo rhh
--       let (ic, hhh) ← prove_le_rat ic ehh ehi rhh rhi
--       pure
--           (ic, elo, ehi,
--             q(@MulBound.mk).mk_app
--               [exlo, exhi, eylo, eyhi, ell, elh, ehl, ehh, elo, ehi, hell, helh, hehl, hehh, lll,
--                 hll, llh, hlh, lhl, hhl, lhh, hhh])
-- #align tactic.approx.eval_mul_bound tactic.approx.eval_mul_bound

-- unsafe def eval_approx_mul (xfn yfn : approx_fn) (xp yp : ℤ) (x y : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, exp) ← ic.ofInt xp
--     let (ic, eyp) ← ic.ofInt yp
--     let (ic, xlo, xhi, hx) ← xfn ic xp exp x
--     let (ic, ylo, yhi, hy) ← yfn ic yp eyp y
--     let (ic, lo, hi, hbd) ← eval_mul_bound ic xlo xhi ylo yhi
--     let n' := xp + yp
--     let (ic, en') ← ic.ofInt n'
--     set_prec n ic n' en' lo hi e <|
--         q(@Approx.mul).mk_app [exp, eyp, xlo, xhi, ylo, yhi, lo, hi, x, y, hx, hy, hbd]
-- #align tactic.approx.eval_approx_mul tactic.approx.eval_approx_mul

-- unsafe def inv_expr : expr :=
--   q((Inv.inv : ℝ → ℝ))
-- #align tactic.approx.inv_expr tactic.approx.inv_expr

-- unsafe def eval_approx_div (xfn iyfn : approx_fn) (xp yp : ℤ) (x y : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, exp) ← ic.ofInt xp
--     let (ic, eyp) ← ic.ofInt yp
--     let (ic, xlo, xhi, hx) ← xfn ic xp exp x
--     let (ic, ylo, yhi, hy) ← iyfn ic yp eyp (inv_expr y)
--     let (ic, lo, hi, hbd) ← eval_mul_bound ic xlo xhi ylo yhi
--     pure
--         (ic, lo, hi,
--           q(@Approx.div).mk_app [exp, eyp, xlo, xhi, ylo, yhi, lo, hi, x, y, hx, hy, hbd])
-- #align tactic.approx.eval_approx_div tactic.approx.eval_approx_div

-- unsafe def eval_approx_inv (xfn : approx_fn) (m : ℤ) (x : expr) : approx_fn
--   | ic, n, en, e => do
--     let (ic, em) ← ic.ofInt m
--     let (ic, elo, ehi, hx) ← xfn ic m em x
--     let lo ← elo.toInt
--     let hi ← ehi.toInt
--     if lo = 0 ∧ hi = 0 then
--         pure (ic, q((0 : ℤ)), q((0 : ℤ)), q(@Approx.inv_zero).mk_app [em, en, x, hx])
--       else
--         if m + n ≤ 0 then
--           if 0 < lo then do
--             let (ic, x0) ← prove_pos ic elo
--             pure
--                 (ic, q((0 : ℤ)), q((1 : ℤ)),
--                   q(@Approx.inv_triv_pos).mk_app [em, en, elo, ehi, x, hx, q(@rfl _ true), x0])
--           else
--             if hi < 0 then do
--               let (ic, x0) ← prove_lt_rat ic ehi q((0 : ℤ)) (Rat.ofInt hi) 0
--               pure
--                   (ic, q((-1 : ℤ)), q((0 : ℤ)),
--                     q(@Approx.inv_triv_neg).mk_app [em, en, elo, ehi, x, hx, q(@rfl _ true), x0])
--             else fail f! "at {x}⁻¹: Failed to bound away from zero. Try increasing the precision"
--         else do
--           let nc ← mk_instance_cache q(ℕ)
--           let p := (m + n).toNat
--           let (nc, ep) ← nc p
--           let hp := q(@rfl _ (($(ep) : ℕ) : ℤ))
--           let (ic, ep2, hp2) ← prove_pow q((2 : ℤ)) 2 ic ep
--           let p2 : ℤ := 2 ^ p
--           let rp2 := Rat.ofInt p2
--           let rlo := Rat.ofInt lo
--           let rhi := Rat.ofInt hi
--           if 0 < lo then do
--               let (ic, x0) ← prove_pos ic elo
--               let lo' := p2 / hi
--               let hi' := (p2 - 1) / lo + 1
--               let (ic, elo') ← ic lo'
--               let (ic, ehi') ← ic hi'
--               let (ic, elh, hlh) ← prove_mul_rat ic elo ehi' rlo (Rat.ofInt hi')
--               let (ic, ehl, hhl) ← prove_mul_rat ic ehi elo' rhi (Rat.ofInt lo')
--               let (ic, hlo) ← prove_le_rat ic ep2 elh p2 (Rat.ofInt (lo * hi'))
--               let (ic, hhi) ← prove_le_rat ic ehl ep2 (Rat.ofInt (hi * lo')) p2
--               pure
--                   (ic, elo, ehi,
--                     q(@Approx.inv_pos).mk_app
--                       [em, en, elo, ehi, elo', ehi', elh, ehl, ep2, x, ep, hx, hp, x0, hp2, hlh,
--                         hhl, hlo, hhi])
--             else
--               if hi < 0 then do
--                 let (ic, x0) ← prove_lt_rat ic ehi q((0 : ℤ)) rhi 0
--                 let lo' := (p2 - 1) / hi - 1
--                 let hi' := p2 / lo
--                 let (ic, elo') ← ic lo'
--                 let (ic, ehi') ← ic hi'
--                 let (ic, elh, hlh) ← prove_mul_rat ic elo ehi' rlo (Rat.ofInt hi')
--                 let (ic, ehl, hhl) ← prove_mul_rat ic ehi elo' rhi (Rat.ofInt lo')
--                 let (ic, hlo) ← prove_le_rat ic ep2 ehl p2 (Rat.ofInt (hi * lo'))
--                 let (ic, hhi) ← prove_le_rat ic elh ep2 (Rat.ofInt (lo * hi')) p2
--                 pure
--                     (ic, elo, ehi,
--                       q(@Approx.inv_neg).mk_app
--                         [em, en, elo, ehi, elo', ehi', elh, ehl, ep2, x, ep, hx, hp, x0, hp2, hlh,
--                           hhl, hlo, hhi])
--               else fail f! "at {x}⁻¹: Failed to bound away from zero. Try increasing the precision"
-- #align tactic.approx.eval_approx_inv tactic.approx.eval_approx_inv

-- -- PLEASE REPORT THIS TO MATHPORT DEVS, THIS SHOULD NOT HAPPEN.
-- -- failed to format: unknown constant 'term.pseudo.antiquot'
-- unsafe
--   def
--     eval_approx
--     : ApproxArgs → approx_fn
--     | approx_args.extra args , ic , n , en , e => failed
--       |
--         approx_args.prec n' args , ic , n , en , e
--         =>
--         do
--           let ( ic , en' ) ← ic . ofInt n'
--             let ( ic , lo , hi , hx ) ← eval_approx args ic n' en' e
--             set_prec n ic n' en' lo hi e hx
--       |
--         args , ic , n , en , e
--         =>
--         do
--           let
--               r
--                 ←
--                 try_core
--                   (
--                     match
--                       e . toNat
--                       with
--                       | some 0 => pure none
--                         |
--                           some _
--                           =>
--                           do let rc ← mk_instance_cache q( ℝ ) some <$> prove_int_uncast rc ic e
--                         | _ => failed
--                     )
--             match
--               r
--               with
--               |
--                   some none
--                   =>
--                   pure ( ic , q( ( 0 : ℤ ) ) , q( ( 0 : ℤ ) ) , q( Approx.zero ) . mk_app [ en ] )
--                 |
--                   some ( some ( _ , ic , a , ha ) )
--                   =>
--                   do
--                     set_prec n ic 0 q( ( 0 : ℤ ) ) a a e
--                       <|
--                       q( @ Approx.const ) . mk_app [ a , e , ha ]
--                 |
--                   none
--                   =>
--                   match
--                     e
--                     with
--                     |
--                         q( - $ ( x ) )
--                         =>
--                         do
--                           let xargs := args
--                             let n' := ( match xargs with | some xp => min n xp | _ => n : ℤ )
--                             eval_approx_neg ( eval_approx xargs ) n' x ic n en e
--                       |
--                         q( $ ( x ) + $ ( y ) )
--                         =>
--                         do
--                           let ( xargs , yargs ) := args
--                             let
--                               n'
--                                 :=
--                                 (
--                                   match
--                                     xargs , yargs
--                                     with
--                                     | some xp , some yp => min n ( max xp yp ) | _ , _ => n
--                                   :
--                                   ℤ
--                                   )
--                             eval_approx_add
--                               ( eval_approx xargs ) ( eval_approx yargs ) n' x y ic n en e
--                       |
--                         q( $ ( x ) - $ ( y ) )
--                         =>
--                         do
--                           let ( xargs , yargs ) := args
--                             let
--                               n'
--                                 :=
--                                 (
--                                   match
--                                     xargs , yargs
--                                     with
--                                     | some xp , some yp => min n ( max xp yp ) | _ , _ => n
--                                   :
--                                   ℤ
--                                   )
--                             eval_approx_sub
--                               ( eval_approx xargs ) ( eval_approx yargs ) n' x y ic n en e
--                       |
--                         q( $ ( x ) * $ ( y ) )
--                         =>
--                         do
--                           let ( xargs , yargs ) := args
--                             let
--                               ( xp , yp )
--                                 :=
--                                 (
--                                   match
--                                     xargs , yargs
--                                     with
--                                     | some xp , some yp => ( xp , yp )
--                                       | none , some yp => ( n - yp , yp )
--                                       | some xp , none => ( xp , n - xp )
--                                       | none , none => let xp := n / 2 ( xp , n - xp )
--                                   :
--                                   ℤ × ℤ
--                                   )
--                             eval_approx_mul
--                               ( eval_approx xargs ) ( eval_approx yargs ) xp yp x y ic n en e
--                       |
--                         q( $ ( x ) / $ ( y ) )
--                         =>
--                         do
--                           let ( xargs , yargs ) := args
--                             let xp := xargs ( n / 2 )
--                             let yp := n - xp
--                             eval_approx_div
--                               ( eval_approx xargs )
--                                 ( eval_approx ( approx_args.unop yargs ) )
--                                 xp
--                                 yp
--                                 x
--                                 y
--                                 ic
--                                 n
--                                 en
--                                 e
--                       |
--                         q( $ ( x ) ⁻¹ )
--                         =>
--                         do
--                           let xargs := args
--                             let m := xargs ( abs n )
--                             eval_approx_inv ( eval_approx xargs ) m x ic n en e
--                       | _ => failed
-- #align tactic.approx.eval_approx tactic.approx.eval_approx

end Approx

end Tactic