-- Mathlib/RingTheory/Algebraic/Cardinality.lean
theorem lift_cardinalMk_le_sigma_polynomial :
    lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L })

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
⊢ (fun x =>
          let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        x =
      (fun x =>
          let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        y →
    x = y

Tactic:
intro h

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  (fun x =>
        let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      x =
    (fun x =>
        let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      y
⊢ x = y

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
this : lift.{max v u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × ↑{x | x ∈ p.aroots L})
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
rwa [lift_umax, lift_id'.{v}] at this

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯
⊢ x ∈ {x_1 | x_1 ∈ (↑p).aroots L}

Tactic:
dsimp

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯
⊢ x ∈ (↑p).aroots L

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧
    HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩
⊢ x = y

Tactic:
refine (Subtype.heq_iff_coe_eq ?_).1 h.2

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧
    HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩
⊢ ∀ (x_1 : L),
    x_1 ∈ (↑(Classical.indefiniteDescription (fun x_2 => ¬x_2 = 0 ∧ (Polynomial.aeval x) x_2 = 0) ⋯)).aroots L ↔
      x_1 ∈ (↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯)).aroots L

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯
⊢ x ∈ (↑p).aroots L

Tactic:
have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯
this : Polynomial.map (algebraMap R L) ↑p ≠ 0
⊢ x ∈ (↑p).aroots L

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧
    HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩
⊢ ∀ (x_1 : L),
    x_1 ∈ (↑(Classical.indefiniteDescription (fun x_2 => ¬x_2 = 0 ∧ (Polynomial.aeval x) x_2 = 0) ⋯)).aroots L ↔
      x_1 ∈ (↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯)).aroots L

Tactic:
simp only [h.1, forall_true_iff]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯
this : Polynomial.map (algebraMap R L) ↑p ≠ 0
⊢ x ∈ (↑p).aroots L

Tactic:
rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
  ← Polynomial.aeval_def, p.2.2]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
have := @lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
  (fun x : L =>
    let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
    ⟨p.1, x, by
      dsimp
      have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
      rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
        ← Polynomial.aeval_def, p.2.2]⟩)
  fun x y => by
    intro h
    simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h
    refine (Subtype.heq_iff_coe_eq ?_).1 h.2
    simp only [h.1, forall_true_iff]

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
this : lift.{max v u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × ↑{x | x ∈ p.aroots L})
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  (fun x =>
        let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      x =
    (fun x =>
        let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      y
⊢ x = y

Tactic:
simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧
    HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩
⊢ x = y