Equivalent Cauchy sequences

Analysis I, Section 5.2: Equivalent Cauchy sequences

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Notion of an ε-close and eventually ε-close sequences of rationals.

  • Notion of an equivalent Cauchy sequence of rationals.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

  • (Add tip here)

abbrev Rat.CloseSeq (ε: ) (a b: Chapter5.Sequence) : Prop := n, n a.n₀ n b.n₀ ε.Close (a n) (b n)abbrev Rat.EventuallyClose (ε: ) (a b: Chapter5.Sequence) : Prop := N, ε.CloseSeq (a.from N) (b.from N)namespace Chapter5

Definition 5.2.1 ($ε$-close sequences)

lemma Rat.closeSeq_def (ε: ) (a b: Sequence) : ε.CloseSeq a b n, n a.n₀ n b.n₀ ε.Close (a n) (b n) := ε:a:Sequenceb:Sequenceε.CloseSeq a b n a.n₀, n b.n₀ ε.Close (a.seq n) (b.seq n) All goals completed! 🐙

Example 5.2.2

declaration uses 'sorry'example : (0.1:).CloseSeq ((fun n: ((-1)^n:)):Sequence) ((fun n: ((1.1:) * (-1)^n)):Sequence) := Rat.CloseSeq 0.1 (↑fun n => (-1) ^ n) fun n => 1.1 * (-1) ^ n All goals completed! 🐙

Example 5.2.2

declaration uses 'sorry'example : ¬ (0.1:).Steady ((fun n: ((-1)^n:)):Sequence) := ¬Rat.Steady 0.1 fun n => (-1) ^ n All goals completed! 🐙

Example 5.2.2

declaration uses 'sorry'example : ¬ (0.1:).Steady ((fun n: ((1.1:) * (-1)^n)):Sequence) := ¬Rat.Steady 0.1 fun n => 1.1 * (-1) ^ n All goals completed! 🐙

Definition 5.2.3 (Eventually ε-close sequences)

lemma Rat.eventuallyClose_def (ε: ) (a b: Sequence) : ε.EventuallyClose a b N, ε.CloseSeq (a.from N) (b.from N) := ε:a:Sequenceb:Sequenceε.EventuallyClose a b N, ε.CloseSeq (a.from N) (b.from N) All goals completed! 🐙

Definition 5.2.3 (Eventually ε-close sequences)

lemma declaration uses 'sorry'Rat.eventuallyClose_iff (ε: ) (a b: ) : ε.EventuallyClose (a:Sequence) (b:Sequence) N, n N, |a n - b n| ε := ε:a: b: ε.EventuallyClose a b N, n N, |a n - b n| ε All goals completed! 🐙

Example 5.2.5

declaration uses 'sorry'example : ¬ (0.1:).CloseSeq ((fun n: (1:)+10^(-(n:)-1)):Sequence) ((fun n: (1:)-10^(-(n:)-1)):Sequence) := ¬Rat.CloseSeq 0.1 (↑fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) All goals completed! 🐙
declaration uses 'sorry'example : (0.1:).EventuallyClose ((fun n: (1:)+10^(-(n:)-1)):Sequence) ((fun n: (1:)-10^(-(n:)-1)):Sequence) := Rat.EventuallyClose 0.1 (↑fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) All goals completed! 🐙declaration uses 'sorry'example : (0.01:).EventuallyClose ((fun n: (1:)+10^(-(n:)-1)):Sequence) ((fun n: (1:)-10^(-(n:)-1)):Sequence) := Rat.EventuallyClose 1e-2 (↑fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) All goals completed! 🐙

Definition 5.2.6 (Equivalent sequences)

abbrev Sequence.Equiv (a b: ) : Prop := ε > (0:), ε.EventuallyClose (a:Sequence) (b:Sequence)

Definition 5.2.6 (Equivalent sequences)

lemma Sequence.equiv_def (a b: ) : Equiv a b (ε:), ε > 0 ε.EventuallyClose (a:Sequence) (b:Sequence) := a: b: Equiv a b ε > 0, ε.EventuallyClose a b All goals completed! 🐙

Definition 5.2.6 (Equivalent sequences)

lemma declaration uses 'sorry'Sequence.equiv_iff (a b: ) : Equiv a b ε > 0, N, n N, |a n - b n| ε := a: b: Equiv a b ε > 0, N, n N, |a n - b n| ε All goals completed! 🐙

Proposition 5.2.8

lemma Sequence.equiv_example : -- This proof is perhaps more complicated than it needs to be; a shorter version may be -- possible that is still faithful to the original text. Equiv (fun n: (1:)+10^(-(n:)-1)) (fun n: (1:)-10^(-(n:)-1)) := Equiv (fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) a: := fun n => 1 + 10 ^ (-n - 1)Equiv a fun n => 1 - 10 ^ (-n - 1) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)Equiv a b a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1) ε > 0, N, n N, |a n - b n| ε a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0 N, n N, |a n - b n| ε have hab (n:) : |a n - b n| = 2 * 10 ^ (-(n:)-1) := calc _ = |((1:) + (10:)^(-(n:)-1)) - ((1:) - (10:)^(-(n:)-1))| := rfl _ = |2 * (10:)^(-(n:)-1)| := a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0n:|1 + 10 ^ (-n - 1) - (1 - 10 ^ (-n - 1))| = |2 * 10 ^ (-n - 1)| All goals completed! 🐙 _ = _ := abs_of_nonneg (a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0n:0 2 * 10 ^ (-n - 1) All goals completed! 🐙) have hab' (N:) : n N, |a n - b n| 2 * 10 ^(-(N:)-1) := Equiv (fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))N:n:hn:n N|a n - b n| 2 * 10 ^ (-N - 1); a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))N:n:hn:n N2 * 10 ^ (-n - 1) 2 * 10 ^ (-N - 1); a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))N:n:hn:n N1 10; All goals completed! 🐙 have hN : N:, 2 * (10:) ^(-(N:)-1) ε := Equiv (fun n => 1 + 10 ^ (-n - 1)) fun n => 1 - 10 ^ (-n - 1) have hN' (N:) : 2 * (10:)^(-(N:)-1) 2/(N+1) := calc _ = 2 / (10:)^(N+1) := a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 * 10 ^ (-N - 1) = 2 / 10 ^ (N + 1) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 * 10 ^ (-N - 1) * 10 ^ (N + 1) = 2 All goals completed! 🐙 _ _ := a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 / 10 ^ (N + 1) 2 / (N + 1) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:N + 1 10 ^ (N + 1) apply le_trans _ (pow_le_pow_left₀ (show 0 (2:) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 / 10 ^ (N + 1) 2 / (N + 1) All goals completed! 🐙) (show (2:) 10 a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 / 10 ^ (N + 1) 2 / (N + 1) All goals completed! 🐙) _) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:N + 1 = (N + 1)a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 ^ (N + 1) = (2 ^ (N + 1))a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:AddMonoidWithOne a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:AddLeftMono a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:ZeroLEOneClass a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:CharZero a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:N + 1 = (N + 1)a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:2 ^ (N + 1) = (2 ^ (N + 1))a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:AddMonoidWithOne a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:AddLeftMono a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:ZeroLEOneClass a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (of_eq_true (Eq.trans (congr (congrArg (fun x => Eq |x|) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Mathlib.Meta.NormNum.IsNat.of_raw 1) (Eq.refl 2)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2))))) (congrArg abs (Eq.trans (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf' (congrArg (HPow.hPow 10) (Eq.trans (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑n) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Eq.trans (congrArg (fun x => x + 0) (Eq.trans (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (congrArg (HPow.hPow n) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one n))) (Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg (congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1))) (Mathlib.Tactic.RingNF.mul_neg (↑n) 1)) (congrArg Neg.neg (mul_one n)))) (add_zero (-n)))) (Mathlib.Tactic.RingNF.add_neg (-1) n))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (10 ^ (-1 - n)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((10 ^ (-1 - n)) ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Eq.trans (congrArg (fun x => x * 2 + 0) (Eq.trans (congrArg (HPow.hPow (10 ^ (-1 - n))) Mathlib.Tactic.RingNF.nat_rawCast_1) (pow_one (10 ^ (-1 - n))))) (add_zero (10 ^ (-1 - n) * 2)))))) (eq_self |10 ^ (-1 - n) * 2|)))) (abs_of_nonneg (le_of_lt (mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) (zpow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl (Nat.ble 1 10))) (-n - 1)))))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N n hn => Eq.mpr (id (congrArg (fun _a => _a 2 * 10 ^ (-N - 1)) (@_fvar.6550 n))) (mul_le_mul_of_nonneg_left (zpow_le_zpow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 10)) (Eq.refl true)) (sub_le_sub_right (neg_le_neg (GCongr.natCast_le_natCast hn)) 1)) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))))N:CharZero try All goals completed! 🐙 all_goals All goals completed! 🐙 a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NhN': (N : ), 2 * 10 ^ (-N - 1) 2 / (N + 1) := fun N => Trans.trans (@?_mvar.20396 N) (@?_mvar.20397 N)N:hN:2 / ε < N N, 2 * 10 ^ (-N - 1) ε a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NhN': (N : ), 2 * 10 ^ (-N - 1) 2 / (N + 1) := fun N => Trans.trans (@?_mvar.20396 N) (@?_mvar.20397 N)N:hN:2 / ε < N2 / (N + 1) ε a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NhN': (N : ), 2 * 10 ^ (-N - 1) 2 / (N + 1) := fun N => Trans.trans (@?_mvar.20396 N) (@?_mvar.20397 N)N:hN:2 / ε < N2 ε * (N + 1) a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NhN': (N : ), 2 * 10 ^ (-N - 1) 2 / (N + 1) := fun N => Trans.trans (@?_mvar.20396 N) (@?_mvar.20397 N)N:hN:2 < N * ε2 ε * (N + 1) All goals completed! 🐙 a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NN:hN:2 * 10 ^ (-N - 1) ε N, n N, |a n - b n| ε; a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NN:hN:2 * 10 ^ (-N - 1) ε n N, |a n - b n| ε; a: := fun n => 1 + 10 ^ (-n - 1)b: := fun n => 1 - 10 ^ (-n - 1)ε::ε > 0hab: (n : ), |@_fvar.5075 n - @_fvar.5310 n| = 2 * 10 ^ (-n - 1) := fun n => Trans.trans (Trans.trans rfl (@?_mvar.6548 n)) (abs_of_nonneg (@?_mvar.6549 n))hab': (N n : ), n N |@_fvar.5075 n - @_fvar.5310 n| 2 * 10 ^ (-N - 1) := fun N => @?_mvar.12521 NN:hN:2 * 10 ^ (-N - 1) εn:hn:n N|a n - b n| ε All goals completed! 🐙

Exercise 5.2.1

theorem declaration uses 'sorry'Sequence.isCauchy_of_equiv {a b: } (hab: Equiv a b) : (a:Sequence).IsCauchy (b:Sequence).IsCauchy := a: b: hab:Equiv a b(↑a).IsCauchy (↑b).IsCauchy All goals completed! 🐙

Exercise 5.2.2

theorem declaration uses 'sorry'Sequence.isBounded_of_eventuallyClose {ε:} {a b: } (hab: ε.EventuallyClose a b) : (a:Sequence).IsBounded (b:Sequence).IsBounded := ε:a: b: hab:ε.EventuallyClose a b(↑a).IsBounded (↑b).IsBounded All goals completed! 🐙
end Chapter5