[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ lift #R[X] * ℵ₀
[PROOFSTEP]
rw [← mk_uLift, ← mk_uLift]
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #(ULift { x // IsAlgebraic R x }) ≤ #(ULift R[X]) * ℵ₀
[PROOFSTEP]
choose g hg₁ hg₂ using fun x : {x : A | IsAlgebraic R x} => x.coe_prop
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
⊢ #(ULift { x // IsAlgebraic R x }) ≤ #(ULift R[X]) * ℵ₀
[PROOFSTEP]
refine' lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => _
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ lift #↑(g ⁻¹' {f}) ≤ ℵ₀
[PROOFSTEP]
rw [lift_le_aleph0, le_aleph0_iff_set_countable]
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ Set.Countable (g ⁻¹' {f})
[PROOFSTEP]
suffices : MapsTo (↑) (g ⁻¹' { f }) (f.rootSet A)
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
this : MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
⊢ Set.Countable (g ⁻¹' {f})
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
[PROOFSTEP]
exact this.countable_of_injOn (Subtype.coe_injective.injOn _) (f.rootSet_finite A).countable
[GOAL]
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
[PROOFSTEP]
rintro x (rfl : g x = f)
[GOAL]
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
x : ↑{x | IsAlgebraic R x}
⊢ ↑x ∈ rootSet (g x) A
[PROOFSTEP]
exact mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift (max #R ℵ₀) * ℵ₀ ≤ max (lift #R) ℵ₀
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ Set.Countable {x | IsAlgebraic R x}
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, ← lift_le]
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift #↑{x | IsAlgebraic R x} ≤ lift ℵ₀
[PROOFSTEP]
apply (cardinal_mk_lift_le_max R A).trans
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ max (lift #R) ℵ₀ ≤ lift ℵ₀
[PROOFSTEP]
simp
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀
[PROOFSTEP]
rw [← lift_id #_, ← lift_id #(R[X])]
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ lift #R[X] * ℵ₀
[PROOFSTEP]
exact cardinal_mk_lift_le_mul R A
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ max #R ℵ₀
[PROOFSTEP]
rw [← lift_id #_, ← lift_id #R]
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ max (lift #R) ℵ₀
[PROOFSTEP]
exact cardinal_mk_lift_le_max R A
