From 3b57d61f37e28c7ea44ed6618773b306774c12a2 Mon Sep 17 00:00:00 2001
From: acmepjz <acme_pjz@hotmail.com>
Date: Wed, 30 Oct 2024 18:23:47 +0800
Subject: [PATCH] add `algebraicIndependent_of_finite_type'`

---
 Mathlib/RingTheory/AlgebraicIndependent.lean | 24 ++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/Mathlib/RingTheory/AlgebraicIndependent.lean b/Mathlib/RingTheory/AlgebraicIndependent.lean
index f92865083dda4..74b086dc8a41c 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent.lean
@@ -468,6 +468,30 @@ theorem algebraicIndependent_of_finite' (s : Set A)
   ext x
   by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]
 
+/-- `Type` version of `algebraicIndependent_of_finite'`. -/
+theorem algebraicIndependent_of_finite_type'
+    (hinj : Injective (algebraMap R A))
+    (H : ∀ t : Set ι, t.Finite → ∀ i : ι, i ∉ t → Transcendental (adjoin R (x '' t)) (x i)) :
+    AlgebraicIndependent R x := by
+  nontriviality R
+  haveI := hinj.nontrivial
+  have hx : Injective x := by
+    simp_rw [Transcendental] at H
+    contrapose! H
+    obtain ⟨i, j, h1, h2⟩ := not_injective_iff.1 H
+    refine ⟨{j}, by simp, i, by simp [h2], ?_⟩
+    rw [h1, Set.image_singleton]
+    exact isAlgebraic_algebraMap (⟨x j, Algebra.self_mem_adjoin_singleton R _⟩ : adjoin R {x j})
+  rw [← Set.coe_comp_rangeFactorization x]
+  refine .comp (algebraicIndependent_of_finite' _ hinj fun t ht hfin a ha ha' ↦ ?_) _
+    (Set.rightInverse_rangeSplitting hx).injective
+  change Finite t at hfin
+  have := H (x ⁻¹' t) (Finite.of_injective _ (hx.restrictPreimage t))
+    ((Equiv.ofInjective _ hx).symm ⟨_, ha⟩)
+    (by rwa [Set.mem_preimage, Equiv.apply_ofInjective_symm hx])
+  rwa [Set.image_preimage_eq_inter_range, Set.inter_eq_self_of_subset_left ht,
+    Equiv.apply_ofInjective_symm hx] at this
+
 variable (R)
 
 /-- A family is a transcendence basis if it is a maximal algebraically independent subset. -/