-- Mathlib/Algebra/Polynomial/Roots.lean
theorem bUnion_roots_finite {R S : Type*} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S]
    (m : R →+* S) (d : ℕ) {U : Set R} (h : U.Finite) :
    (⋃ (f : R[X]) (_ : f.natDegree ≤ d ∧ ∀ i, f.coeff i ∈ U),
        ((f.map m).roots.toFinset.toSet : Set S)).Finite :=
  Set.Finite.biUnion
    (by
      -- We prove that the set of polynomials under consideration is finite because its
      -- image by the injective map `π` is finite
      let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i
      refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
      · exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i
      · refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
        exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩)
    fun _ _ => Finset.finite_toSet _

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ Set.InjOn π fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_

Result:
case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
x : R[X]
hx : x ∈ fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
y : R[X]
hy : y ∈ fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
hxy : π x = π y
i : ℕ
hi : i ≤ d
⊢ x.coeff i = y.coeff i

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
⊢ Set.Finite fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i

Result:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ Set.Finite fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ (π '' fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆ Set.univ.pi fun x => U

Tactic:
exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i

Result:
no goals

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
x : R[X]
hx : x ∈ fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
y : R[X]
hy : y ∈ fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
hxy : π x = π y
i : ℕ
hi : i ≤ d
⊢ x.coeff i = y.coeff i

Tactic:
exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ Set.Finite fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ (π '' fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆ Set.univ.pi fun x => U

case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i
⊢ Set.InjOn π fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U