-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_finset_map_embedding_subtype (s : Set A)
    (li : AlgebraicIndependent R ((↑) : s → A)) (t : Finset s) :
    AlgebraicIndependent R ((↑) : Finset.map (Embedding.subtype s) t → A)

Proof state:
case mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h : x ∈ Finset.map (Embedding.subtype s) t
⊢ ↑⟨x, h⟩ ∈ s

Tactic:
rw [Finset.mem_map] at h

Result:
case mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h✝ : x ∈ Finset.map (Embedding.subtype s) t
h : ∃ a ∈ t, (Embedding.subtype s) a = x
⊢ ↑⟨x, h✝⟩ ∈ s

Proof state:
case mk.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
a : Subtype s
left✝ : a ∈ t
h : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ ↑⟨(Embedding.subtype s) a, h⟩ ∈ s

Tactic:
simp only [Subtype.coe_prop, Embedding.coe_subtype]

Result:
no goals

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : { x // x ∈ Finset.map (Embedding.subtype s) t }
⊢ ↑x ∈ s

Tactic:
obtain ⟨x, h⟩ := x

Result:
case mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h : x ∈ Finset.map (Embedding.subtype s) t
⊢ ↑⟨x, h⟩ ∈ s

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
⊢ AlgebraicIndependent R Subtype.val

Tactic:
convert AlgebraicIndependent.comp li f _

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
⊢ Injective f

Proof state:
case mk.mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
x : A
hx✝ : x ∈ Finset.map (Embedding.subtype s) t
hx : ∃ a ∈ t, (Embedding.subtype s) a = x
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a ∈ t, (Embedding.subtype s) a = y
⊢ f ⟨x, hx✝⟩ = f ⟨y, hy✝⟩ → ⟨x, hx✝⟩ = ⟨y, hy✝⟩

Tactic:
obtain ⟨a, _, rfl⟩ := hx

Result:
case mk.mk.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a ∈ t, (Embedding.subtype s) a = y
a : Subtype s
left✝ : a ∈ t
hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨y, hy✝⟩ → ⟨(Embedding.subtype s) a, hx⟩ = ⟨y, hy✝⟩

Proof state:
case mk.mk.intro.intro.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
a : Subtype s
left✝¹ : a ∈ t
hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
b : Subtype s
left✝ : b ∈ t
hy : (Embedding.subtype s) b ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨(Embedding.subtype s) b, hy⟩ →
    ⟨(Embedding.subtype s) a, hx⟩ = ⟨(Embedding.subtype s) b, hy⟩

Tactic:
simp only [f, imp_self, Subtype.mk_eq_mk]

Result:
no goals

Proof state:
case mk.mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
x : A
hx : x ∈ Finset.map (Embedding.subtype s) t
y : A
hy : y ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨x, hx⟩ = f ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
rw [Finset.mem_map] at hx hy

Result:
case mk.mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
x : A
hx✝ : x ∈ Finset.map (Embedding.subtype s) t
hx : ∃ a ∈ t, (Embedding.subtype s) a = x
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a ∈ t, (Embedding.subtype s) a = y
⊢ f ⟨x, hx✝⟩ = f ⟨y, hy✝⟩ → ⟨x, hx✝⟩ = ⟨y, hy✝⟩

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R Subtype.val

Tactic:
let f : t.map (Embedding.subtype s) → s := fun x =>
  ⟨x.1, by
    obtain ⟨x, h⟩ := x
    rw [Finset.mem_map] at h
    obtain ⟨a, _, rfl⟩ := h
    simp only [Subtype.coe_prop, Embedding.coe_subtype]⟩

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
⊢ AlgebraicIndependent R Subtype.val

Proof state:
case mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h✝ : x ∈ Finset.map (Embedding.subtype s) t
h : ∃ a ∈ t, (Embedding.subtype s) a = x
⊢ ↑⟨x, h✝⟩ ∈ s

Tactic:
obtain ⟨a, _, rfl⟩ := h

Result:
case mk.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
a : Subtype s
left✝ : a ∈ t
h : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ ↑⟨(Embedding.subtype s) a, h⟩ ∈ s

Proof state:
case mk.mk.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a ∈ t, (Embedding.subtype s) a = y
a : Subtype s
left✝ : a ∈ t
hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨y, hy✝⟩ → ⟨(Embedding.subtype s) a, hx⟩ = ⟨y, hy✝⟩

Tactic:
obtain ⟨b, _, rfl⟩ := hy

Result:
case mk.mk.intro.intro.intro.intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
a : Subtype s
left✝¹ : a ∈ t
hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
b : Subtype s
left✝ : b ∈ t
hy : (Embedding.subtype s) b ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨(Embedding.subtype s) b, hy⟩ →
    ⟨(Embedding.subtype s) a, hx⟩ = ⟨(Embedding.subtype s) b, hy⟩