Information
Difficulty: easy — 3 definitions, 1 abbreviations, 2 lemmas, 3 theorems, 17 examples.
no_pow_two_eq_pow_three
theorem no_pow_two_eq_pow_three (p q : ℕ) (hq : 0 < q) : 2 ^ p ≠ 3 ^ q
Show details
fun p q hq h => Or.casesOn (Nat.eq_zero_or_pos p) (fun hp => Eq.ndrec (motive := fun p => 2 ^ p = 3 ^ q → False) (fun h => have h31 := Nat.le_self_pow (LT.lt.ne' hq) 3; no_pow_two_eq_pow_three._proof_1_1 q h31 (Eq.mp (congrFun' (congrArg Eq (pow_zero 2)) (3 ^ q)) h)) (Eq.symm hp) h) fun hp => have hp' := Decidable.byContradiction fun a => no_pow_two_eq_pow_three._proof_1_2 p q hp a; have e1 := Eq.mpr (id ((fun a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 : ℕ), (a = a_3) = (a_2 = a_3)) (fun a_2 => Eq.refl (a = a_2)) e_a) (2 ^ p % 2) (2 ^ (p - 1) * 2 % 2) (Eq.trans (congrArg (fun _a => 2 ^ _a % 2) (Eq.symm hp')) (Eq.trans (congrArg (fun _a => _a % 2) (pow_succ 2 (p - 1))) (Eq.refl (2 ^ (p - 1) * 2 % 2)))) 0)) (Decidable.byContradiction fun a => no_pow_two_eq_pow_three._proof_1_3 p q a); have e2 := have h := Nat.pow_mod 3 q 2; Eq.mp (congrArg (Eq (3 ^ q % 2)) (Eq.trans (congrFun' (congrArg HMod.hMod (one_pow q)) 2) (Nat.mod_succ 1))) h; no_pow_two_eq_pow_three._proof_1_4 p q (Eq.mp (congrArg (fun _a => _a % 2 = 0) h) e1) e2
Complexity: 4802 (size of the value term)
Dependencies: (none)
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, GT.gt, Int, Int.add_one_le_of_lt, Int.emod_def, Int.lt_mul_ediv_self_add, Int.mul_ediv_self_le, Int.natCast_add, Int.natCast_emod, Int.natCast_mul, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.isZero, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.mul_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_pow, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.coordinate_eval_6, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.mul, Lean.Omega.LinearCombo.mul_eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.eq_zero_or_pos, Nat.le_self_pow, Nat.lt_or_gt_of_ne, Nat.mod_succ, Nat.pow_mod, Ne, Not, Or, Or.elim, congrArg, congrFun', id, le_of_le_of_eq, of_decide_eq_true
Used by: irrational_logb_two_three
irrational_logb_two_three
theorem irrational_logb_two_three : Irrational (Real.logb 2 3)
Show details
fun a => Exists.casesOn a fun r hr => have h3 := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false); have hb1 := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); have key := Eq.mpr (id (congrArg (fun _a => 2 ^ _a = 3) hr)) (Real.rpow_logb (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)) (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl false)) h3); have hrpos := have h0 := Real.rpow_zero 2; have this := Eq.mpr (id (congrArg (fun _a => 2 ^ 0 < _a) key)) (Eq.mpr (id (congrArg (fun _a => _a < 3) h0)) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))); have this := (Real.rpow_lt_rpow_left_iff hb1).mp this; cast (Eq.trans (Eq.trans (Eq.trans (congrFun' (congrArg LT.lt (Eq.symm Nat.cast_zero)) ↑r) Rat.natCast_lt_cast._simp_1) (congrFun' (congrArg LT.lt Nat.cast_zero) r)) (Eq.symm (Eq.trans (congrFun' (congrArg LT.lt (Eq.symm Nat.cast_zero)) r) (congrFun' (congrArg LT.lt Nat.cast_zero) r)))) this; have hq := Rat.pos r; have hp := Rat.num_pos.mpr hrpos; have hcastQ := have hd := cast (Eq.symm (Eq.trans (congrArg (Ne ↑r.den) (Eq.symm Nat.cast_zero)) (congrArg Not Nat.cast_inj._simp_1))) r.den_nz; have h := Rat.num_div_den r; Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (r * ↑r.den) (↑r.num) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (↑r.num ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.num) (Nat.rawCast 1) (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.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (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.ofNat 0)))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq (Eq.mp (congrArg (fun _a => _a) (propext (div_eq_iff hd))) h)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.Common.neg_zero))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (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.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.den) (Nat.rawCast 1) (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.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq (Eq.mp (congrArg (fun _a => _a) (propext (div_eq_iff hd))) h))) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))); have hcast := cast (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congrArg (HMul.hMul ↑r) (Eq.symm (Rat.cast_natCast r.den))) (Rat.cast_mul._simp_1 r ↑r.den))) ↑r.num) (congrArg (Eq ↑(r * ↑r.den)) (Eq.symm (Rat.cast_intCast r.num)))) Rat.cast_inj._simp_1)) hcastQ; have key2 := Eq.mpr (id (congrArg (fun _a => _a ^ r.den = 3 ^ r.den) key)) (Eq.refl (3 ^ r.den)); have hnumcast := have this := Int.toNat_of_nonneg (LT.lt.le hp); cast (Eq.symm (Eq.trans (congrArg (Eq ↑r.num) (Eq.symm (Int.cast_natCast r.num.toNat))) Int.cast_inj._simp_1)) (Eq.symm this); have key4 := cast (Eq.trans (congr (congrArg Eq (Nat.cast_pow._simp_1 2 r.num.toNat)) (Nat.cast_pow._simp_1 3 r.den)) Nat.cast_inj._simp_1) (Eq.mp (congrArg (fun _a => _a = 3 ^ r.den) (Real.rpow_natCast 2 r.num.toNat)) (Eq.mp (congrArg (fun _a => 2 ^ _a = 3 ^ r.den) hnumcast) (Eq.mp (congrArg (fun _a => 2 ^ _a = 3 ^ r.den) hcast) (Eq.mp (congrArg (fun _a => _a = 3 ^ r.den) (Eq.symm (Real.rpow_mul (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true)) ↑r ↑r.den))) (Eq.mp (congrArg (fun _a => _a = 3 ^ r.den) (Eq.symm (Real.rpow_natCast (2 ^ ↑r) r.den))) key2))))); no_pow_two_eq_pow_three r.num.toNat r.den hq key4
Complexity: 75216 (size of the value term)
Dependencies: (none)
Proof dependencies: no_pow_two_eq_pow_three
Mathlib dependencies: Int.cast_natCast, Int.rawCast, Irrational, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_one, Nat.cast_zero, Nat.rawCast, Rat.cast_intCast, Rat.cast_natCast, Rat.num_div_den, Rat.num_pos, Rat.pos, Real, Real.logb, Real.rpow_logb, Real.rpow_lt_rpow_left_iff, Real.rpow_mul, Real.rpow_natCast, Real.rpow_zero, Ring, Set, Set.range, div_eq_iff, neg_eq_zero, sub_eq_zero_of_eq
Lean core dependencies: Bool, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, Int, Int.cast, Int.negOfNat, Int.toNat, Int.toNat_of_nonneg, Nat, Nat.cast, Ne, Not, Not.intro, Rat, cast, congr, congrArg, congrFun', id, inferInstance, rfl
Used by: irrational_trafficLightInformation
TrafficLightColor
inductive TrafficLightColor : Type
green : TrafficLightColor
amber : TrafficLightColor
red : TrafficLightColor
Show details
Outer dependencies: (none)
Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum
TrafficLightColor_cardinality
theorem TrafficLightColor_cardinality : Fintype.card TrafficLightColor = 3
Show details
of_decide_eq_true (id (Eq.refl true))
Complexity: 93 (size of the value term)
Dependencies: TrafficLightColor
Mathlib dependencies: Fintype.card
Lean core dependencies: Bool, Decidable.decide, Eq, Nat, id, of_decide_eq_true
Used by: trafficLightInformation_eq
trafficLightInformation
def trafficLightInformation : ℝ
Show details
| trafficLightInformation = Real.logb 2 ↑(Fintype.card TrafficLightColor)
Complexity: 29 (size of the value term)
Outer dependencies: (none)
Inner dependencies: TrafficLightColor
Mathlib dependencies: Fintype.card, Real, Real.logb
trafficLightInformation_eq
theorem trafficLightInformation_eq : trafficLightInformation = Real.logb 2 3
Show details
have h := cast (Eq.symm Nat.cast_inj._simp_1) TrafficLightColor_cardinality; id (Eq.mpr (id (congrArg (fun _a => Real.logb 2 _a = Real.logb 2 3) h)) (Eq.refl (Real.logb 2 3)))
Complexity: 1080 (size of the value term)
Dependencies: trafficLightInformation
Proof dependencies: TrafficLightColor, TrafficLightColor_cardinality
Mathlib dependencies: Fintype.card, Real, Real.logb
Used by: irrational_trafficLightInformation
irrational_trafficLightInformation
theorem irrational_trafficLightInformation : Irrational trafficLightInformation
Show details
Eq.mpr (id (congrArg (fun _a => Irrational _a) trafficLightInformation_eq)) irrational_logb_two_three
Complexity: 271 (size of the value term)
Dependencies: trafficLightInformation
Proof dependencies: irrational_logb_two_three, trafficLightInformation_eq
Mathlib dependencies: Irrational, Real, Real.logb
Used by: (none)
PhoneNumber
abbrev PhoneNumber : Type
Show details
| PhoneNumber = (Fin 15 → Fin 10)
Complexity: 23 (size of the value term)
Outer dependencies: (none)
phoneNumber_cardinality
theorem phoneNumber_cardinality : Fintype.card PhoneNumber = 10 ^ 15
Show details
Eq.mpr (id (congrArg (fun _a => _a = 10 ^ 15) Fintype.card_fun)) (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congr (congrArg HPow.hPow (Fintype.card_fin 10)) (Fintype.card_fin 15))) 1000000000000000) (eq_self 1000000000000000)))
Complexity: 1491 (size of the value term)
Dependencies: PhoneNumber
Mathlib dependencies: Fintype.card, Fintype.card_fin, Fintype.card_fun
no_pow_two_eq_pow_five
theorem no_pow_two_eq_pow_five (p q : ℕ) (hq : 0 < q) : 2 ^ p ≠ 5 ^ q
Show details
fun p q hq h => Or.casesOn (Nat.eq_zero_or_pos p) (fun hp => Eq.ndrec (motive := fun p => 2 ^ p = 5 ^ q → False) (fun h => have h31 := Nat.le_self_pow (LT.lt.ne' hq) 5; no_pow_two_eq_pow_five._proof_1_1 q h31 (Eq.mp (congrFun' (congrArg Eq (pow_zero 2)) (5 ^ q)) h)) (Eq.symm hp) h) fun hp => have hp' := Decidable.byContradiction fun a => no_pow_two_eq_pow_five._proof_1_2 p q hp a; have e1 := Eq.mpr (id ((fun a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 : ℕ), (a = a_3) = (a_2 = a_3)) (fun a_2 => Eq.refl (a = a_2)) e_a) (2 ^ p % 2) (2 ^ (p - 1) * 2 % 2) (Eq.trans (congrArg (fun _a => 2 ^ _a % 2) (Eq.symm hp')) (Eq.trans (congrArg (fun _a => _a % 2) (pow_succ 2 (p - 1))) (Eq.refl (2 ^ (p - 1) * 2 % 2)))) 0)) (Decidable.byContradiction fun a => no_pow_two_eq_pow_five._proof_1_3 p q a); have e2 := have h := Nat.pow_mod 5 q 2; Eq.mp (congrArg (Eq (5 ^ q % 2)) (Eq.trans (congrFun' (congrArg HMod.hMod (one_pow q)) 2) (Nat.mod_succ 1))) h; no_pow_two_eq_pow_five._proof_1_4 p q (Eq.mp (congrArg (fun _a => _a % 2 = 0) h) e1) e2
Complexity: 4802 (size of the value term)
Dependencies: (none)
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, GT.gt, Int, Int.add_one_le_of_lt, Int.emod_def, Int.lt_mul_ediv_self_add, Int.mul_ediv_self_le, Int.natCast_add, Int.natCast_emod, Int.natCast_mul, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.isZero, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.mul_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_pow, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.coordinate_eval_6, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.mul, Lean.Omega.LinearCombo.mul_eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.eq_zero_or_pos, Nat.le_self_pow, Nat.lt_or_gt_of_ne, Nat.mod_succ, Nat.pow_mod, Ne, Not, Or, Or.elim, congrArg, congrFun', id, le_of_le_of_eq, of_decide_eq_true
Used by: irrational_logb_two_five
irrational_logb_two_five
theorem irrational_logb_two_five : Irrational (Real.logb 2 5)
Show details
fun a => Exists.casesOn a fun r hr => have h5 := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 5)) (Eq.refl false); have hb1 := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); have key := Eq.mpr (id (congrArg (fun _a => 2 ^ _a = 5) hr)) (Real.rpow_logb (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)) (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl false)) h5); have hrpos := have h0 := Real.rpow_zero 2; have this := Eq.mpr (id (congrArg (fun _a => 2 ^ 0 < _a) key)) (Eq.mpr (id (congrArg (fun _a => _a < 5) h0)) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 5)) (Eq.refl false))); have this := (Real.rpow_lt_rpow_left_iff hb1).mp this; cast (Eq.trans (Eq.trans (Eq.trans (congrFun' (congrArg LT.lt (Eq.symm Nat.cast_zero)) ↑r) Rat.natCast_lt_cast._simp_1) (congrFun' (congrArg LT.lt Nat.cast_zero) r)) (Eq.symm (Eq.trans (congrFun' (congrArg LT.lt (Eq.symm Nat.cast_zero)) r) (congrFun' (congrArg LT.lt Nat.cast_zero) r)))) this; have hq := Rat.pos r; have hp := Rat.num_pos.mpr hrpos; have hcastQ := have hd := cast (Eq.symm (Eq.trans (congrArg (Ne ↑r.den) (Eq.symm Nat.cast_zero)) (congrArg Not Nat.cast_inj._simp_1))) r.den_nz; have h := Rat.num_div_den r; Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (r * ↑r.den) (↑r.num) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (↑r.num ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.num) (Nat.rawCast 1) (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.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (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.ofNat 0)))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq (Eq.mp (congrArg (fun _a => _a) (propext (div_eq_iff hd))) h)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.Common.neg_zero))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (↑r.num) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.num ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf r rfl (Eq.mpr (id (congrArg (fun _a => r ^ Nat.rawCast 1 * Nat.rawCast 1 = r ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (r ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (↑r.den) rfl (Eq.mpr (id (congrArg (fun _a => ↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 = ↑r.den ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.mul_pf_right (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1) (Eq.refl 1))))) (Mathlib.Tactic.Ring.Common.mul_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.neg_mul (↑r.den) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (↑r.num ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (r ^ Nat.rawCast 1 * (↑r.den ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.num) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (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.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero r (Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (↑r.den) (Nat.rawCast 1) (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.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq (Eq.mp (congrArg (fun _a => _a) (propext (div_eq_iff hd))) h))) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))); have hcast := cast (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congrArg (HMul.hMul ↑r) (Eq.symm (Rat.cast_natCast r.den))) (Rat.cast_mul._simp_1 r ↑r.den))) ↑r.num) (congrArg (Eq ↑(r * ↑r.den)) (Eq.symm (Rat.cast_intCast r.num)))) Rat.cast_inj._simp_1)) hcastQ; have key2 := Eq.mpr (id (congrArg (fun _a => _a ^ r.den = 5 ^ r.den) key)) (Eq.refl (5 ^ r.den)); have hnumcast := have this := Int.toNat_of_nonneg (LT.lt.le hp); cast (Eq.symm (Eq.trans (congrArg (Eq ↑r.num) (Eq.symm (Int.cast_natCast r.num.toNat))) Int.cast_inj._simp_1)) (Eq.symm this); have key4 := cast (Eq.trans (congr (congrArg Eq (Nat.cast_pow._simp_1 2 r.num.toNat)) (Nat.cast_pow._simp_1 5 r.den)) Nat.cast_inj._simp_1) (Eq.mp (congrArg (fun _a => _a = 5 ^ r.den) (Real.rpow_natCast 2 r.num.toNat)) (Eq.mp (congrArg (fun _a => 2 ^ _a = 5 ^ r.den) hnumcast) (Eq.mp (congrArg (fun _a => 2 ^ _a = 5 ^ r.den) hcast) (Eq.mp (congrArg (fun _a => _a = 5 ^ r.den) (Eq.symm (Real.rpow_mul (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true)) ↑r ↑r.den))) (Eq.mp (congrArg (fun _a => _a = 5 ^ r.den) (Eq.symm (Real.rpow_natCast (2 ^ ↑r) r.den))) key2))))); no_pow_two_eq_pow_five r.num.toNat r.den hq key4
Complexity: 75216 (size of the value term)
Dependencies: (none)
Proof dependencies: no_pow_two_eq_pow_five
Mathlib dependencies: Int.cast_natCast, Int.rawCast, Irrational, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_one, Nat.cast_zero, Nat.rawCast, Rat.cast_intCast, Rat.cast_natCast, Rat.num_div_den, Rat.num_pos, Rat.pos, Real, Real.logb, Real.rpow_logb, Real.rpow_lt_rpow_left_iff, Real.rpow_mul, Real.rpow_natCast, Real.rpow_zero, Ring, Set, Set.range, div_eq_iff, neg_eq_zero, sub_eq_zero_of_eq
Lean core dependencies: Bool, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, Int, Int.cast, Int.negOfNat, Int.toNat, Int.toNat_of_nonneg, Nat, Nat.cast, Ne, Not, Not.intro, Rat, cast, congr, congrArg, congrFun', id, inferInstance, rfl
Used by: irrational_phoneNumberInformation
phoneNumberInformation
def phoneNumberInformation : ℝ
Show details
| phoneNumberInformation = Real.logb 2 ↑(Fintype.card PhoneNumber)
Complexity: 113 (size of the value term)
Outer dependencies: (none)
Inner dependencies: PhoneNumber
Mathlib dependencies: Fintype.card, Real, Real.logb
phoneNumberInformation_eq
theorem phoneNumberInformation_eq : phoneNumberInformation = 15 + 15 * Real.logb 2 5
Show details
have h := cast (Eq.symm (Eq.trans (congrArg (Eq ↑(Fintype.card PhoneNumber)) (Nat.cast_pow._simp_1 10 15)) Nat.cast_inj._simp_1)) phoneNumber_cardinality; id (Eq.mpr (id (congrArg (fun _a => Real.logb 2 _a = 15 + 15 * Real.logb 2 5) h)) (have h10 := Eq.mpr (id (congrArg (fun _a => 10 ^ 15 = _a) (Eq.symm (mul_pow 2 5 15)))) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 10)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit1) Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 5)) (Eq.refl 10)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit1) Mathlib.Meta.NormNum.IsNatPowT.bit1)))); Eq.mpr (id (congrArg (fun _a => Real.logb 2 _a = 15 + 15 * Real.logb 2 5) h10)) (Eq.mpr (id (congrArg (fun _a => _a = 15 + 15 * Real.logb 2 5) (Real.logb_mul (ne_of_gt (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) 15)) (ne_of_gt (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 5)) (Eq.refl (Nat.ble 1 5))) 15))))) (Eq.mpr (id (congrArg (fun _a => _a + Real.logb 2 (5 ^ 15) = 15 + 15 * Real.logb 2 5) (Real.logb_pow 2 2 15))) (Eq.mpr (id (congrArg (fun _a => ↑15 * Real.logb 2 2 + _a = 15 + 15 * Real.logb 2 5) (Real.logb_pow 2 5 15))) (Eq.mpr (id (congrArg (fun _a => ↑15 * _a + ↑15 * Real.logb 2 5 = 15 + 15 * Real.logb 2 5) (Real.logb_self_eq_one (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_natCast 15 15 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 15) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1) (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.mul_zero (Nat.rawCast 15)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Nat.rawCast 15 + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_natCast 15 15 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)))) (Mathlib.Tactic.Ring.Common.atom_pf (Real.logb 2 5) rfl (Eq.mpr (id (congrArg (fun _a => Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 = Real.logb 2 5 ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_right (Real.logb 2 5) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 15) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1) (Eq.refl 15)))) (Mathlib.Tactic.Ring.Common.mul_zero (Nat.rawCast 15)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (Nat.rawCast 15) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.atom_pf (Real.logb 2 5) rfl (Eq.mpr (id (congrArg (fun _a => Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 = Real.logb 2 5 ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_right (Real.logb 2 5) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 15) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1) (Eq.refl 15)))) (Mathlib.Tactic.Ring.Common.mul_zero (Nat.rawCast 15)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (Nat.rawCast 15) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))))))))))
Complexity: 32915 (size of the value term)
Dependencies: phoneNumberInformation
Proof dependencies: PhoneNumber, phoneNumber_cardinality
Mathlib dependencies: Fintype.card, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.IsNatPowT.bit1, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.of_eq, Nat.cast_one, Nat.rawCast, Real, Real.logb, Real.logb_mul, Real.logb_pow, Real.logb_self_eq_one, mul_pow, ne_of_gt, pow_pos
Lean core dependencies: Bool, Eq, Eq.mpr, Eq.symm, Eq.trans, Fin, Nat, Nat.ble, Nat.cast, Nat.pow, cast, congrArg, id, rfl
Used by: irrational_phoneNumberInformation
irrational_phoneNumberInformation
theorem irrational_phoneNumberInformation : Irrational phoneNumberInformation
Show details
Eq.mpr (id (congrArg (fun _a => Irrational _a) phoneNumberInformation_eq)) (have h1 := Irrational.mul_natCast irrational_logb_two_five (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.IsNat.raw_refl 15) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)); have h2 := Irrational.add_natCast h1 15; have heq := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.Common.atom_pf (Real.logb 2 5) rfl (Eq.mpr (id (congrArg (fun _a => Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 = Real.logb 2 5 ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_left (Real.logb 2 5) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 15) (Eq.refl 15)))) (Mathlib.Tactic.Ring.Common.mul_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (Nat.rawCast 15 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Nat.rawCast 15) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 15))) (Mathlib.Tactic.Ring.Common.atom_pf (Real.logb 2 5) rfl (Eq.mpr (id (congrArg (fun _a => Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 = Real.logb 2 5 ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_mul (Mathlib.Tactic.Ring.Common.mul_add (Mathlib.Tactic.Ring.Common.mul_pf_right (Real.logb 2 5) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 15) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1) (Eq.refl 15)))) (Mathlib.Tactic.Ring.Common.mul_zero (Nat.rawCast 15)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0))) (Mathlib.Tactic.Ring.Common.zero_mul (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (Nat.rawCast 15) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (Real.logb 2 5 ^ Nat.rawCast 1 * Nat.rawCast 15 + 0)))); Eq.mp (congrArg (fun _a => Irrational _a) heq) h2)
Complexity: 18190 (size of the value term)
Dependencies: phoneNumberInformation
Proof dependencies: irrational_logb_two_five, phoneNumberInformation_eq
Mathlib dependencies: Irrational, Irrational.add_natCast, Irrational.mul_natCast, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Real, Real.logb
Used by: (none)
phoneNumber_bits_needed
theorem phoneNumber_bits_needed : Fintype.card PhoneNumber > 2 ^ 49 ∧ Fintype.card PhoneNumber ≤ 2 ^ 50
Show details
Eq.mpr (id (congrArg (fun _a => _a > 2 ^ 49 ∧ _a ≤ 2 ^ 50) phoneNumber_cardinality)) ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 49)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0) Mathlib.Meta.NormNum.IsNatPowT.bit0) (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNatPowT.bit1)))) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit1) Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Eq.refl false), Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 15)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit1) Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 50)) (Mathlib.Meta.NormNum.IsNatPowT.run (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0) Mathlib.Meta.NormNum.IsNatPowT.bit0) (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0)))) (Eq.refl true)⟩
Complexity: 2681 (size of the value term)
Dependencies: PhoneNumber
Proof dependencies: phoneNumber_cardinality
Mathlib dependencies: Fintype.card, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.IsNatPowT.bit1, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_pow
Used by: (none)
Discrete
def Discrete (α : Type) [Norm α] : Prop
Show details
| Discrete α = ∀ (x : α), ∃ n, ‖x‖ = ↑n
Complexity: 33 (size of the value term)
Outer dependencies: (none)
Discrete.size
def Discrete.size {α : Type} [Norm α] (h : Discrete α) (x : α) : ℕ
Show details
| h.size x = ⋯.choose
Complexity: 43 (size of the value term)
Outer dependencies: Discrete
Lean core dependencies: Eq, Exists.choose, Nat, Nat.cast
Used by: Discrete.pi, Discrete.prod, Discrete.size_eq
Discrete.size_eq
theorem Discrete.size_eq {α : Type} [Norm α] (h : Discrete α) (x : α) : ↑(h.size x) = ‖x‖
Show details
fun {α} [Norm α] h x => Eq.symm (Exists.choose_spec (h x))
Complexity: 91 (size of the value term)
Dependencies: Discrete, Discrete.size
Lean core dependencies: Eq, Eq.symm, Exists.choose, Exists.choose_spec, Nat, Nat.cast
Used by: Discrete.pi, Discrete.prod
NormNonneg
structure NormNonneg (α : Type) [Norm α] : Prop
nonneg : ∀ (x : α), 0 ≤ ‖x‖
Show details
Outer dependencies: (none)
Used by: InformationSystem.Environment.universe_isolated, InformationSystem.Step.bottom, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, InformationSystem.irreversible, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.reversible, InformationSystem.roundtrip_neutral, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous, InformationSystem.zero_run_le, instNormNonnegBit, instNormNonnegBool, instNormNonnegCell, instNormNonnegForallFin, instNormNonnegProd, instNormNonnegUnit
Bit
def Bit : Type
Show details
| Bit = Bool
Complexity: 1 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Bool
Used by: ApplicationLayer.interface, Bit.discrete, Bit.flip, BitFunction, BitFunction.IsFixedPoint, BitFunction.cardinality, BitFunction.cardinality_input_growth, BitFunction.cardinality_output_growth, BitFunction.comp, BitFunction.exists_settle, BitFunction.fixedPoint_isFixed, BitFunction.iterate, BitFunction.iterate_dominates_succ, BitFunction.iterate_stays, BitSequence, BitSequence.Dominates, BitSequence.Dominates.bot, BitSequence.cardinality, BitSequence.trueCount, BitSequence.trueCount_le, BitSequence.trueCount_strict, DataLinkLayer.network, DataLinkLayer.physical, Frame, Frame.make, Frame.make_valid, Frame.valid, InterfaceOld.Value.observeAll, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, PhysicalLayer.interface, Receiver.step, Receiver.step_correct, Sender.step, TransportLayer.application, TransportLayer.interface, instNonemptyFrame, instNormBit, instNormFrame, instNormNonnegBit, notRule, notRule_no_fixedPoint, trafficLight_approx_two_bits
instNormBit
instance instNormBit : Norm Bit
Show details
| instNormBit = { norm := fun x => 1 }
Complexity: 17 (size of the value term)
Outer dependencies: Bit
Used by: ApplicationLayer.interface, Bit.discrete, DataLinkLayer.network, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, PhysicalLayer.interface, Receiver.step, Sender.step, TransportLayer.application, TransportLayer.interface, instNormFrame, instNormNonnegBit
instNormNonnegBit
instance instNormNonnegBit : NormNonneg Bit
Show details
{ nonneg := fun x => id (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true)) }
Complexity: 163 (size of the value term)
Outer dependencies: Bit, NormNonneg, instNormBit
Mathlib dependencies: Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Nat.cast_zero, Real
Used by: (none)
Bit.discrete
theorem Bit.discrete : Discrete Bit
Show details
fun x => Exists.intro 1 (id (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_natCast 1 1 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))
Complexity: 211 (size of the value term)
Dependencies: Bit, Discrete, instNormBit
Mathlib dependencies: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Real
Used by: (none)
Bit.flip
BitSequence
abbrev BitSequence (n : ℕ) : Type
Show details
| BitSequence n = (Fin n → Bit)
Complexity: 7 (size of the value term)
Outer dependencies: (none)
Inner dependencies: Bit
Used by: ApplicationLayer.Value, ApplicationLayer.interface, BitFunction.IsFixedPoint, BitFunction.Monotone, BitFunction.cardinality, BitFunction.exists_isFixedPoint, BitFunction.exists_settle, BitFunction.fixedPoint, BitFunction.fixedPoint_isFixed, BitFunction.iterate, BitFunction.iterate_settles, BitFunction.iterate_stays, BitSequence.Dominates, BitSequence.Dominates.bot, BitSequence.cardinality, BitSequence.trueCount, BitSequence.trueCount_le, BitSequence.trueCount_strict, DataLinkLayer.network, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application, TransportLayer.interface, notRule_no_fixedPoint, trafficLight_approx_two_bits
BitSequence.cardinality
theorem BitSequence.cardinality (n : ℕ) : Fintype.card (BitSequence n) = 2 ^ n
Show details
fun n => have hbit := Fintype.card_bool; Eq.mpr (id (congrArg (fun _a => _a = 2 ^ n) Fintype.card_fun)) (Eq.mpr (id (congrArg (fun _a => _a ^ Fintype.card (Fin n) = 2 ^ n) hbit)) (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg (HPow.hPow 2) (Fintype.card_fin n))) (2 ^ n)) (eq_self (2 ^ n)))))
Complexity: 1484 (size of the value term)
Dependencies: Bit, BitSequence
Mathlib dependencies: Fintype.card, Fintype.card_bool, Fintype.card_fin, Fintype.card_fun
trafficLight_approx_two_bits
theorem trafficLight_approx_two_bits : ¬Fintype.card TrafficLightColor ≤ Fintype.card (BitSequence 1) ∧ Fintype.card TrafficLightColor ≤ Fintype.card (BitSequence 2)
Show details
Eq.mpr (id (congrArg (fun _a => ¬Fintype.card TrafficLightColor ≤ _a ∧ Fintype.card TrafficLightColor ≤ Fintype.card (BitSequence 2)) (BitSequence.cardinality 1))) (Eq.mpr (id (congrArg (fun _a => ¬Fintype.card TrafficLightColor ≤ 2 ^ 1 ∧ Fintype.card TrafficLightColor ≤ _a) (BitSequence.cardinality 2))) (of_decide_eq_true (id (Eq.refl true))))
Complexity: 2509 (size of the value term)
Dependencies: Bit, BitSequence, TrafficLightColor
Proof dependencies: BitSequence.cardinality
Mathlib dependencies: Fintype.card
Lean core dependencies: And, Bool, Decidable.decide, Eq, Eq.mpr, Fin, Nat, Not, congrArg, id, of_decide_eq_true
Used by: (none)
instNormForallFin_computerNetworks
instance instNormForallFin_computerNetworks.{u_1} {α : Type u_1} [Norm α] {n : ℕ} : Norm (Fin n → α)
Show details
| instNormForallFin_computerNetworks = { norm := fun f => ∑ i, ‖f i‖ }
Complexity: 55 (size of the value term)
Outer dependencies: (none)
Mathlib dependencies: Finset.sum, Finset.univ, Norm, Real
Used by: ApplicationLayer.interface, Channel, Component, Component.Arrow, Component.Arrow.Equiv, Component.Arrow.setoid, Component.Hom.tensor_id_id, Component.Simplex.toInformationSystem, Component.empty, Component.empty_parallel, Component.equivalent_of_stationary, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast, Component.recast_congr, Component.sequential, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, DataLinkLayer.network, Discrete.pi, InformationSystem.parallel_delta, InformationSystem.sequential_delta, InformationSystem.toSimplex, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, Receiver.step, Sender.step, TransportLayer.application, TransportLayer.interface, instNormFrame, instNormNonnegForallFin
instNormNonnegForallFin
instance instNormNonnegForallFin {α : Type} [Norm α] [NormNonneg α] {n : ℕ} : NormNonneg (Fin n → α)
Show details
fun {α} [Norm α] [NormNonneg α] {n} => { nonneg := fun f => Finset.sum_nonneg fun i x => NormNonneg.nonneg (f i) }
Complexity: 139 (size of the value term)
Outer dependencies: NormNonneg, instNormForallFin_computerNetworks
Mathlib dependencies: Finset, Finset.sum_nonneg, Finset.univ, Norm, Real
Used by: (none)
Discrete.pi
theorem Discrete.pi {α : Type} [Norm α] (h : Discrete α) {n : ℕ} : Discrete (Fin n → α)
Show details
fun {α} [Norm α] h {n} f => Exists.intro (∑ i, h.size (f i)) (id (Eq.mpr (id (congrArg (Eq (∑ i, ‖f i‖)) (Nat.cast_sum Finset.univ fun x => h.size (f x)))) (Finset.sum_congr rfl fun i x => Eq.symm (Discrete.size_eq h (f i)))))
Complexity: 931 (size of the value term)
Dependencies: Discrete, instNormForallFin_computerNetworks
Proof dependencies: Discrete.size, Discrete.size_eq
Mathlib dependencies: Finset, Finset.sum, Finset.sum_congr, Finset.univ, Nat.cast_sum, Norm, Real
Used by: (none)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.