-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem algebraicIndependent_of_finite_type'
    (hinj : Injective (algebraMap R A))
    (H : ∀ t : Set ι, t.Finite → AlgebraicIndependent R (fun i : t ↦ x i) →
      ∀ i : ι, i ∉ t → Transcendental (adjoin R (x '' t)) (x i)) :
    AlgebraicIndependent R x

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
classical
refine algebraicIndependent_of_finite_type fun t hfin ↦ hfin.induction_on_subset _
  (algebraicIndependent_empty_type_iff.mpr hinj) fun {a u} ha hu ha' h ↦ ?_
convert ((Set.image_eq_range _ _ ▸ h.option_iff <| x a).2 <| H u (hfin.subset hu) h _ ha').comp _
  (Set.subtypeInsertEquivOption ha').injective with x
by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t
hu : u ⊆ t
ha' : a ∉ u
h : AlgebraicIndependent R fun i => x ↑i
⊢ AlgebraicIndependent R fun i => x ↑i

Tactic:
convert ((Set.image_eq_range _ _ ▸ h.option_iff <| x a).2 <| H u (hfin.subset hu) h _ ha').comp _
  (Set.subtypeInsertEquivOption ha').injective with x

Result:
case h.e'_4.h
ι : Type u_1
R : Type u_2
A : Type u_3
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x✝ ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t
hu : u ⊆ t
ha' : a ∉ u
h : AlgebraicIndependent R fun i => x✝ ↑i
x : ↑(insert a u)
⊢ x✝ ↑x = ((fun o => o.elim (x✝ a) fun i => x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption ha')) x

Proof state:
case h.e'_4.h
ι : Type u_1
R : Type u_2
A : Type u_3
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x✝ ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t
hu : u ⊆ t
ha' : a ∉ u
h : AlgebraicIndependent R fun i => x✝ ↑i
x : ↑(insert a u)
⊢ x✝ ↑x = ((fun o => o.elim (x✝ a) fun i => x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption ha')) x

Tactic:
by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
refine algebraicIndependent_of_finite_type fun t hfin ↦ hfin.induction_on_subset _
  (algebraicIndependent_empty_type_iff.mpr hinj) fun {a u} ha hu ha' h ↦ ?_

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hinj : Injective ⇑(algebraMap R A)
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i => x ↑i) → ∀ i ∉ t, Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t
hu : u ⊆ t
ha' : a ∉ u
h : AlgebraicIndependent R fun i => x ↑i
⊢ AlgebraicIndependent R fun i => x ↑i