/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil
namespace Erdos313
This set contains all solutions (m, P) to the Erdős problem 313.
A solution is a pair where m is an integer ≥ 2 and P is a non-empty, finite set of
distinct prime numbers, such that the sum of the reciprocals of the primes in P equals 1 - 1/m.
def erdos313Solutions : Set (ℕ × Finset ℕ) :=
{(m, P) | 2 ≤ m ∧ P.Nonempty ∧ (∀ p ∈ P, p.Prime) ∧ ∑ p ∈ P, (1 : ℚ) / p = 1 - 1 / m}
Are there infinitely many pairs (m, P) where m ≥ 2 is an integer
and P is a set of distinct primes such that the following equation holds:
$\sum_{p \in P} \frac{1}{p} = 1 - \frac{1}{m}$?
@[category research open, AMS 11]
theorem erdos_313 : answer(sorry) ↔ erdos313Solutions.Infinite := ⊢ True ↔ erdos313Solutions.Infinite
All goals completed! 🐙
@[category test, AMS 11]
theorem erdos_313.variants.solution_6_2_3 : (6, {2, 3}) ∈ erdos313Solutions := ⊢ (6, {2, 3}) ∈ erdos313Solutions
All goals completed! 🐙
@[category test, AMS 11]
theorem erdos_313.variants.solution_42_2_3_7 : (42, {2, 3, 7}) ∈ erdos313Solutions := ⊢ (42, {2, 3, 7}) ∈ erdos313Solutions
All goals completed! 🐙
An integer n is a primary pseudoperfect number if it is the denominator m in a
solution (m, P) to the Erdős 313 problem.
def IsPrimaryPseudoperfect (n : ℕ) : Prop := ∃ P, (n, P) ∈ erdos313Solutions
It is conjectured that the set of primary pseudoperfect numbers is infinite.
@[category research open, AMS 11]
theorem erdos_313.variants.primary_pseudoperfect_are_infinite :
Set.Infinite {n | IsPrimaryPseudoperfect n} := ⊢ {n | IsPrimaryPseudoperfect n}.Infinite
All goals completed! 🐙
There are at least 8 primary pseudoperfect numbers. The first eight terms of A54377 are exhibited together with their explicit prime decompositions.
@[category textbook, AMS 11]
theorem erdos_313.variants.exists_at_least_eight_primary_pseudoperfect :
8 ≤ (Set.encard {n | IsPrimaryPseudoperfect n}) := ⊢ 8 ≤ {n | IsPrimaryPseudoperfect n}.encard
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 8 ≤ {n | IsPrimaryPseudoperfect n}.encard
have hS : (↑S : Set ℕ) ⊆ {n | IsPrimaryPseudoperfect n} := ⊢ 8 ≤ {n | IsPrimaryPseudoperfect n}.encard
intro x S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}x:ℕhx:x ∈ ↑S⊢ x ∈ {n | IsPrimaryPseudoperfect n}
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}x:ℕhx:x = 2 ∨ x = 6 ∨ x = 42 ∨ x = 1806 ∨ x = 47058 ∨ x = 2214502422 ∨ x = 52495396602 ∨ x = 8490421583559688410706771261086⊢ x ∈ {n | IsPrimaryPseudoperfect n}
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 2 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 6 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 42 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 1806 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 47058 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 2214502422 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 52495396602 ∈ {n | IsPrimaryPseudoperfect n}S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 8490421583559688410706771261086 ∈ {n | IsPrimaryPseudoperfect n}
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 2 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (2, {2}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 6 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (6, {2, 3}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 42 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 7}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (42, {2, 3, 7}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 1806 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 7, 43}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (1806, {2, 3, 7, 43}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 47058 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 11, 23, 31}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (47058, {2, 3, 11, 23, 31}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 2214502422 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 11, 23, 31, 47059}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (2214502422, {2, 3, 11, 23, 31, 47059}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 52495396602 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 11, 17, 101, 149, 3109}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (52495396602, {2, 3, 11, 17, 101, 149, 3109}) ∈ erdos313Solutions All goals completed! 🐙⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 8490421583559688410706771261086 ∈ {n | IsPrimaryPseudoperfect n} exact ⟨{2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ (8490421583559688410706771261086, {2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}) ∈ erdos313Solutions
refine ⟨S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ 2 ≤ 8490421583559688410706771261086 All goals completed! 🐙, S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ {2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}.Nonempty All goals completed! 🐙, ?_, ?_⟩
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ ∀ p ∈ {2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}, Nat.Prime p intro p S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}p:ℕhp:p ∈ {2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}⊢ Nat.Prime p
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 2S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 3S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 11S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 23S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 31S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 47059S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 2217342227S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 1729101023519 S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 2S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 3S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 11S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 23S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 31S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 47059S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 2217342227S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ Nat.Prime 1729101023519 All goals completed! 🐙
S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}⊢ ∑ p ∈ {2, 3, 11, 23, 31, 47059, 2217342227, 1729101023519}, 1 / ↑p = 1 - 1 / ↑8490421583559688410706771261086 All goals completed! 🐙⟩
calc (8 : ℕ∞)
= ((S.card : ℕ) : ℕ∞) := S:Finset ℕ := {2, 6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086}hS:↑S ⊆ {n | IsPrimaryPseudoperfect n} :=
fun ⦃x⦄ hx =>
Or.casesOn
(Eq.mp
(Eq.trans
(Eq.trans
(congrArg (fun x_1 => x ∈ x_1)
(Eq.trans
(Finset.coe_insert 2 {6, 42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086})
(congrArg (insert 2)
(Eq.trans
(Finset.coe_insert 6 {42, 1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086})
(congrArg (insert 6)
(Eq.trans
(Finset.coe_insert 42 {1806, 47058, 2214502422, 52495396602, 8490421583559688410706771261086})
(congrArg (insert 42)
(Eq.trans
(Finset.coe_insert 1806 {47058, 2214502422, 52495396602, 8490421583559688410706771261086})
(congrArg (insert 1806)
(Eq.trans
(Finset.coe_insert 47058 {2214502422, 52495396602, 8490421583559688410706771261086})
(congrArg (insert 47058)
(Eq.trans (Finset.coe_insert 2214502422 {52495396602, 8490421583559688410706771261086})
(congrArg (insert 2214502422)
(Eq.trans (Finset.coe_insert 52495396602 {8490421583559688410706771261086})
(congrArg (insert 52495396602)
(Finset.coe_singleton 8490421583559688410706771261086))))))))))))))))
exists_at_least_eight_primary_pseudoperfect._simp_1)
(congrArg (Or (x = 2))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 6))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 42))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 1806))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 47058))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 2214502422))
(Eq.trans exists_at_least_eight_primary_pseudoperfect._simp_1
(congrArg (Or (x = 52495396602))
exists_at_least_eight_primary_pseudoperfect._simp_2))))))))))))))
hx)
(fun h =>
Eq.symm h ▸
Exists.intro {2}
(of_eq_true
(Eq.trans
(congrArg (fun x => (2, {2}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr (congrArg And (Eq.trans (Finset.singleton_nonempty._simp_1 2) (eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr Finset.mem_singleton._simp_1 (Eq.refl (Nat.Prime p)))
forall_eq._simp_1)
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2 (Mathlib.Meta.NormNum.IsNat.raw_refl 2)
(Eq.refl 0))))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans (Finset.sum_singleton (fun x => (↑x)⁻¹) 2)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast (2, {2}).1 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))))
(Eq.refl (Int.ofNat 1)) (Eq.refl 2)))
(Eq.refl 1) (Eq.refl 2)))
(eq_self (1 / 2)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
Eq.symm h ▸
Exists.intro {2, 3}
(of_eq_true
(Eq.trans
(congrArg (fun x => (6, {2, 3}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr (congrArg And (Eq.trans (Finset.insert_nonempty._simp_1 2 {3}) (eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2)) Finset.mem_singleton._simp_1))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq._simp_1
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3 (Eq.refl true) (Eq.refl 1))
(Eq.refl false))))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {3})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_singleton._simp_1)
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl false)))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans (Finset.sum_singleton (fun x => (↑x)⁻¹) 3)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Eq.refl 5) (Eq.refl 6))
(Eq.refl 5) (Eq.refl 6)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast (6, {2, 3}).1 6
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))))))
(Eq.refl (Int.ofNat 5)) (Eq.refl 6)))
(Eq.refl 5) (Eq.refl 6)))
(eq_self (5 / 6)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
Eq.symm h ▸
Exists.intro {2, 3, 7}
(of_eq_true
(Eq.trans
(congrArg (fun x => (42, {2, 3, 7}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 42)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr
(congrArg And (Eq.trans (Finset.insert_nonempty._simp_1 2 {3, 7}) (eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 3)) Finset.mem_singleton._simp_1))))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3 (Eq.refl true)
(Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq._simp_1
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 7)
(Mathlib.Meta.NormNum.minFacHelper_0 7 (Eq.refl true)
(Eq.refl 1))
(Eq.refl false))))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {3, 7})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl false))))
(Eq.trans Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {7})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl 3)))
Finset.mem_singleton._simp_1)
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))
(Eq.refl false)))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3)))
(Eq.trans (Finset.sum_singleton (fun x => (↑x)⁻¹) 7)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 7 7
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7)))))
(Eq.refl 1) (Eq.refl 7))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 7))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 7)))
(Eq.refl 10) (Eq.refl 21))
(Eq.refl 10) (Eq.refl 21)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 10)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 21))))
(Eq.refl (Nat.mul 10 1)) (Eq.refl 21)))
(Eq.refl 41) (Eq.refl 42))
(Eq.refl 41) (Eq.refl 42)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast (42, {2, 3, 7}).1 42
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 42))))))
(Eq.refl (Int.ofNat 41)) (Eq.refl 42)))
(Eq.refl 41) (Eq.refl 42)))
(eq_self (41 / 42)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
Eq.symm h ▸
Exists.intro {2, 3, 7, 43}
(of_eq_true
(Eq.trans
(congrArg (fun x => (1806, {2, 3, 7, 43}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1806)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans (Finset.insert_nonempty._simp_1 2 {3, 7, 43}) (eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 3))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 7)) Finset.mem_singleton._simp_1))))))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3 (Eq.refl true)
(Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 7)
(Mathlib.Meta.NormNum.minFacHelper_0 7
(Eq.refl true) (Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq._simp_1
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 43))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 43)
(Mathlib.Meta.NormNum.minFacHelper_3 (Eq.refl 7)
(Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0 43
(Eq.refl true) (Eq.refl 1))))
(Eq.refl false))))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {3, 7, 43})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 7))
(Eq.refl false))))
(Eq.trans Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 43))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {7, 43})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl 3)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 7))
(Eq.refl false))))
(Eq.trans Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 43))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {43})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 7))
(Eq.refl 7)))
Finset.mem_singleton._simp_1)
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 7))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 43))
(Eq.refl false)))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 7 7
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 7)))))
(Eq.refl 1) (Eq.refl 7)))
(Eq.trans (Finset.sum_singleton (fun x => (↑x)⁻¹) 43)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 43 43
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 43)))))
(Eq.refl 1) (Eq.refl 43))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 7))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 7)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 43))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 43)))
(Eq.refl 50) (Eq.refl 301))
(Eq.refl 50) (Eq.refl 301)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 50)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 301))))
(Eq.refl (Nat.mul 50 1)) (Eq.refl 301)))
(Eq.refl 451) (Eq.refl 903))
(Eq.refl 451) (Eq.refl 903)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 451)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 903))))
(Eq.refl (Nat.mul 451 1)) (Eq.refl 903)))
(Eq.refl 1805) (Eq.refl 1806))
(Eq.refl 1805) (Eq.refl 1806)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast (1806, {2, 3, 7, 43}).1 1806
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1806))))))
(Eq.refl (Int.ofNat 1805)) (Eq.refl 1806)))
(Eq.refl 1805) (Eq.refl 1806)))
(eq_self (1805 / 1806)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
Eq.symm h ▸
Exists.intro {2, 3, 11, 23, 31}
(of_eq_true
(Eq.trans
(congrArg (fun x => (47058, {2, 3, 11, 23, 31}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 47058)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans (Finset.insert_nonempty._simp_1 2 {3, 11, 23, 31}) (eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 3))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 11))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 23))
Finset.mem_singleton._simp_1))))))))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3 (Eq.refl true)
(Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 11)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0 11
(Eq.refl true) (Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 23))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
23)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0
23 (Eq.refl true) (Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq._simp_1
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 31))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
31)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 7) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0
31 (Eq.refl true) (Eq.refl 1))))
(Eq.refl false))))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {3, 11, 23, 31})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans
Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {11, 23, 31})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl 3)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {23, 31})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl 11)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 11))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans Finset.mem_singleton._simp_1
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 11))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Eq.refl false)))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 11 11
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11)))))
(Eq.refl 1) (Eq.refl 11)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {31})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl 23)))
Finset.mem_singleton._simp_1)
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 23))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 31))
(Eq.refl false)))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 23
23
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 23)))))
(Eq.refl 1) (Eq.refl 23)))
(Eq.trans
(Finset.sum_singleton (fun x => (↑x)⁻¹) 31)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 31
31
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 31)))))
(Eq.refl 1) (Eq.refl 31))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 23))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 23)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 31))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 31)))
(Eq.refl 54) (Eq.refl 713))
(Eq.refl 54) (Eq.refl 713)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 11))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 11)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 54)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 713))))
(Eq.refl (Nat.mul 54 1)) (Eq.refl 713)))
(Eq.refl 1307) (Eq.refl 7843))
(Eq.refl 1307) (Eq.refl 7843)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1307)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 7843))))
(Eq.refl (Nat.mul 1307 1)) (Eq.refl 7843)))
(Eq.refl 11764) (Eq.refl 23529))
(Eq.refl 11764) (Eq.refl 23529)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 11764)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 23529))))
(Eq.refl (Nat.mul 11764 1)) (Eq.refl 23529)))
(Eq.refl 47057) (Eq.refl 47058))
(Eq.refl 47057) (Eq.refl 47058)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
(47058, {2, 3, 11, 23, 31}).1 47058
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 47058))))))
(Eq.refl (Int.ofNat 47057)) (Eq.refl 47058)))
(Eq.refl 47057) (Eq.refl 47058)))
(eq_self (47057 / 47058)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
Eq.symm h ▸
Exists.intro {2, 3, 11, 23, 31, 47059}
(of_eq_true
(Eq.trans
(congrArg (fun x => (2214502422, {2, 3, 11, 23, 31, 47059}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2214502422)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans (Finset.insert_nonempty._simp_1 2 {3, 11, 23, 31, 47059})
(eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 3))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 11))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 23))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 31))
Finset.mem_singleton._simp_1))))))))))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3
(Eq.refl true) (Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 11)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0 11
(Eq.refl true) (Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 23))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
23)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0
23 (Eq.refl true) (Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
31)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 7)
(Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5)
(Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0
31 (Eq.refl true)
(Eq.refl 1))))
(Eq.refl false)))))
(Eq.trans forall_eq._simp_1
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 47059))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
47059)
⋯ (Eq.refl false))))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {3, 11, 23, 31, 47059})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans
Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans ⋯ (or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {11, 23, 31, 47059})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl 3)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans (congr ⋯ ⋯)
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg (Membership.mem {23, 31, 47059})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl 11)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 11))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr (congrArg Or ⋯)
(Eq.trans
Finset.mem_singleton._simp_1
⋯))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 11 11
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11)))))
(Eq.refl 1) (Eq.refl 11)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem {31, 47059})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 23))
(Eq.refl 23)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr (congrArg Or (eq_false ⋯))
(Eq.trans
Finset.mem_singleton._simp_1
(eq_false ⋯)))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 23
23
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 23)))))
(Eq.refl 1) (Eq.refl 23)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem {47059})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Eq.refl 31)))
Finset.mem_singleton._simp_1)
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 47059))
(Eq.refl false)))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
31 31
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 31)))))
(Eq.refl 1) (Eq.refl 31)))
(Eq.trans
(Finset.sum_singleton
(fun x => (↑x)⁻¹) 47059)
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
47059 47059
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 47059)))))
(Eq.refl 1) (Eq.refl 47059))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 31))))
(Eq.refl (Nat.mul 1 1))
(Eq.refl 31)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 47059))))
(Eq.refl (Nat.mul 1 1))
(Eq.refl 47059)))
(Eq.refl 47090) (Eq.refl 1458829))
(Eq.refl 47090) (Eq.refl 1458829)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 23))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 23)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 47090)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1458829))))
(Eq.refl (Nat.mul 47090 1))
(Eq.refl 1458829)))
(Eq.refl 2541899) (Eq.refl 33553067))
(Eq.refl 2541899) (Eq.refl 33553067)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 11))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 11)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 2541899)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 33553067))))
(Eq.refl (Nat.mul 2541899 1))
(Eq.refl 33553067)))
(Eq.refl 61513956) (Eq.refl 369083737))
(Eq.refl 61513956) (Eq.refl 369083737)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 61513956)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 369083737))))
(Eq.refl (Nat.mul 61513956 1)) (Eq.refl 369083737)))
(Eq.refl 553625605) (Eq.refl 1107251211))
(Eq.refl 553625605) (Eq.refl 1107251211)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 553625605)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1107251211))))
(Eq.refl (Nat.mul 553625605 1)) (Eq.refl 1107251211)))
(Eq.refl 2214502421) (Eq.refl 2214502422))
(Eq.refl 2214502421) (Eq.refl 2214502422)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_sub (Eq.refl HSub.hSub)
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
(2214502422, {2, 3, 11, 23, 31, 47059}).1 2214502422
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2214502422))))))
(Eq.refl (Int.ofNat 2214502421)) (Eq.refl 2214502422)))
(Eq.refl 2214502421) (Eq.refl 2214502422)))
(eq_self (2214502421 / 2214502422)))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))
(and_self True))
(eq_true True.intro)))))
fun h =>
Or.casesOn h
(fun h =>
⋯ ▸
Exists.intro {2, 3, 11, 17, 101, 149, 3109}
(of_eq_true
(Eq.trans
(congrArg (fun x => (52495396602, {2, 3, 11, 17, 101, 149, 3109}) ∈ setOf x)
(funext fun x =>
congrArg (fun x_1 => 2 ≤ x.1 ∧ x.2.Nonempty ∧ (∀ p ∈ x.2, Nat.Prime p) ∧ x_1)
(congr (congrArg Eq (Finset.sum_congr (Eq.refl x.2) fun x_1 a => one_div ↑x_1))
(congrArg (HSub.hSub 1) (one_div ↑x.1)))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 52495396602)) (Eq.refl true))))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans (Finset.insert_nonempty._simp_1 2 {3, 11, 17, 101, 149, 3109})
(eq_true True.intro)))
(Eq.trans
(Eq.trans
(congr
(congrArg And
(Eq.trans
(Eq.trans
(forall_congr fun p =>
implies_congr
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 2))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 3))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 11))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 17))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 101))
(Eq.trans Finset.mem_insert._simp_1
(congrArg (Or (p = 149))
Finset.mem_singleton._simp_1))))))))))))
(Eq.refl (Nat.Prime p)))
forall_eq_or_imp._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_2
(Mathlib.Meta.NormNum.IsNat.raw_refl 2) (Eq.refl 0)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 3)
(Mathlib.Meta.NormNum.minFacHelper_0 3
(Eq.refl true) (Eq.refl 1))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl 11)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0 11
(Eq.refl true) (Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg And
(eq_true
(Mathlib.Meta.NormNum.isNat_prime_2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 17))
(Eq.refl true)
(Mathlib.Meta.NormNum.isNat_minFac_4
(Mathlib.Meta.NormNum.IsNat.raw_refl
17)
(Mathlib.Meta.NormNum.minFacHelper_3
(Eq.refl 5) (Eq.refl false)
(Mathlib.Meta.NormNum.minFacHelper_0
17 (Eq.refl true)
(Eq.refl 1)))
(Eq.refl false)))))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans
(Eq.trans
(congr (congrArg And (eq_true ⋯))
(Eq.trans forall_eq_or_imp._simp_1
(Eq.trans ⋯
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(and_self True))
(eq_true True.intro))))
(Eq.trans
(Eq.trans
(congr
(congrArg Eq
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem {3, 11, 17, 101, 149, 3109})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl 2)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr (congrArg Or ⋯)
(Eq.trans
Finset.mem_insert._simp_1 ⋯))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 2 2
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))))
(Eq.refl 1) (Eq.refl 2)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem {11, 17, 101, 149, 3109})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Eq.refl 3)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans
(congr (congrArg Or (eq_false ⋯))
(Eq.trans
Finset.mem_insert._simp_1
(Eq.trans ⋯
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 3 3
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 3)))))
(Eq.refl 1) (Eq.refl 3)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem {17, 101, 149, 3109})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11))
(Eq.refl 11)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans
(congr
(congrArg Or
(eq_false
(Mathlib.Meta.NormNum.isNat_eq_false
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 11))
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 17))
(Eq.refl false))))
(Eq.trans Finset.mem_insert._simp_1
(Eq.trans
(Eq.trans ⋯ (or_self False))
(eq_false not_false))))
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 11 11
(Mathlib.Meta.NormNum.isNat_ofNat ℕ
(Eq.refl 11)))))
(Eq.refl 1) (Eq.refl 11)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not
(Eq.trans
(Eq.trans
(congrArg
(Membership.mem
{101, 149, 3109})
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 17))
(Eq.refl 17)))
Finset.mem_insert._simp_1)
(Eq.trans
(Eq.trans (congr ⋯ ⋯)
(or_self False))
(eq_false not_false))))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
17 17
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 17)))))
(Eq.refl 1) (Eq.refl 17)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg Not (Eq.trans ⋯ ⋯))
not_false_eq_true)
(eq_true True.intro))))
(Eq.trans
(congr
(congrArg HAdd.hAdd
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast
101 101
(Mathlib.Meta.NormNum.isNat_ofNat
ℕ (Eq.refl 101)))))
(Eq.refl 1) (Eq.refl 101)))
(Eq.trans
(Finset.sum_insert
(of_eq_true
(Eq.trans ⋯
(eq_true True.intro))))
(Eq.trans
(congr (congrArg HAdd.hAdd ⋯)
(Eq.trans
(Finset.sum_singleton
(fun x => (↑x)⁻¹) 3109)
⋯))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd) ⋯ ⋯
(Eq.refl 3258)
(Eq.refl 463241))
(Eq.refl 3258)
(Eq.refl 463241)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 101))))
(Eq.refl (Nat.mul 1 1))
(Eq.refl 101)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 3258)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 463241))))
(Eq.refl (Nat.mul 3258 1))
(Eq.refl 463241)))
(Eq.refl 792299) (Eq.refl 46787341))
(Eq.refl 792299)
(Eq.refl 46787341)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 17))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 17)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 792299)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat
ℚ (Eq.refl 46787341))))
(Eq.refl (Nat.mul 792299 1))
(Eq.refl 46787341)))
(Eq.refl 60256424) (Eq.refl 795384797))
(Eq.refl 60256424) (Eq.refl 795384797)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add
(Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 11))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 11)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 60256424)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 795384797))))
(Eq.refl (Nat.mul 60256424 1))
(Eq.refl 795384797)))
(Eq.refl 1458205461) (Eq.refl 8749232767))
(Eq.refl 1458205461) (Eq.refl 8749232767)))))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 3))))
(Eq.refl (Nat.mul 1 1)) (Eq.refl 3)))
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul
(Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 1458205461)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ
(Eq.refl 8749232767))))
(Eq.refl (Nat.mul 1458205461 1))
(Eq.refl 8749232767)))
(Eq.refl ⋯) ⋯)
⋯ ⋯))))
⋯)))
⋯)
⋯)
⋯))
⋯)
⋯))
⋯)
⋯))
⋯)
⋯))))
⋯⊢ 8 = ↑S.card All goals completed! 🐙
_ = (↑S : Set ℕ).encard := (Set.encard_coe_eq_coe_finsetCard S).symm
_ ≤ Set.encard {n | IsPrimaryPseudoperfect n} := Set.encard_le_encard hS
end Erdos313