α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
⊢ False
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ False
have : Inhabited (∀ i : ι, (g i).out) := by
  refine' ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 _⟩
  rw [mk_out]
  exact (H i).ne_bot
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
⊢ False
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
⊢ False
let G := invFun F
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
⊢ False
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
⊢ False
have sG : Surjective G := invFun_surjective F.2
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
⊢ False
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
⊢ False
choose C hc using
  show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
    intro i
    simp only [not_exists.symm, not_forall.symm]
    refine' fun h => (H i).not_le _
    rw [← mk_out (f i), ← mk_out (g i)]
    exact ⟨Embedding.ofSurjective _ h⟩
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
i : ι
a : Quotient.out (f i)
h : G { fst := i, snd := a } = C
⊢ False
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
⊢ False
let ⟨⟨i, a⟩, h⟩ := sG C
no goals
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ C i
i : ι
a : Quotient.out (f i)
h : G { fst := i, snd := a } = C
⊢ False
exact hc i a (congr_fun h _)
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ (#Quotient.out (g i)) ≠ 0
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ Inhabited ((i : ι) → Quotient.out (g i))
refine' ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 _⟩
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ (#Quotient.out (g i)) ≠ 0
rw [mk_out]
no goals
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0
exact (H i).ne_bot
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ∃ b, ∀ (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ b
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
⊢ ∀ (i : ι), ∃ b, ∀ (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ b
intro i
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ∃ b, ∀ (a : Quotient.out (f i)), G { fst := i, snd := a } i ≠ b
simp only [not_exists.symm, not_forall.symm]
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ g i ≤ f i
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
refine' fun h => (H i).not_le _
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ (#Quotient.out (g i)) ≤ (#Quotient.out (f i))
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ g i ≤ f i
rw [← mk_out (f i), ← mk_out (g i)]
no goals
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ↑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, invFun ↑F { fst := i, snd := x_1 } i = x
⊢ (#Quotient.out (g i)) ≤ (#Quotient.out (f i))
exact ⟨Embedding.ofSurjective _ h⟩