awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ Subset.{v'} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)

Tactic:
Set.image_mono hs'

Premises used: Set.image_mono
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ Subset.{v'} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)

Tactic:
exact Set.image_mono hs'

Premises used: Set.image_mono
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ Eq.{v' + 1} (α := Set A') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)

Tactic:
have := H.2 (f '' s)
    ((algebraicIndependent_image h.injOn).mp ((AlgHom.algebraicIndependent_iff f h).mpr hs))
    (by rw [Set.range_comp]; exact Set.image_mono hs')
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
this : Eq.{v' + 1} (α := Set A') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)
rwa : ∀ (this : Eq.{v' + 1} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)), range x = s
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : range x = s), range x = s
⊢ range x = s

Tactic:
rwa [Set.range_comp, (Set.image_injective.mpr h).eq_iff] at this

Premises used: Iff.mpr, Set.range_comp, Set.image_injective, Function.Injective.eq_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
inst_7 : FaithfulSMul A A'
x : ι → A
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑(algebraMap A A') : (a : A) → A') ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
.of_comp (IsScalarTower.toAlgHom R A A') (FaithfulSMul.algebraMap_injective A A') H

Premises used: IsScalarTower.toAlgHom, IsTranscendenceBasis.of_comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R x

Tactic:
hx
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
h :
  Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) = x
⊢ IsTranscendenceBasis.{u, u_2, v} R (A := A)
    (Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x))

Tactic:
convert! hx
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
h :
  ∀ (x_1 : ι),
    Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
        x_1 =
      x x_1
⊢ Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) = x

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
x_1 : ι
⊢ Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
      x_1 =
    x x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
⊢ IsTranscendenceBasis.{u, u_2, v} R (A := A)
    (Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x))

Tactic:
e.symm.isTranscendenceBasis hx

Premises used: AlgEquiv.symm, AlgEquiv.isTranscendenceBasis
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
h : x = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
convert! e.symm.isTranscendenceBasis hx

Premises used: AlgEquiv.symm, AlgEquiv.isTranscendenceBasis
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
h :
  ∀ (x_1 : ι),
    x x_1 = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) x_1
⊢ x = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
x_1 : ι
⊢ x x_1 = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : AlgebraicIndependent R x
rw : #(↑(range x) : Type v) ≤ trdeg R A
⊢ lift.{v, u} #ι ≤ lift.{u, v} (trdeg R A)

Tactic:
rw [lift_mk_eq'.mpr ⟨.ofInjective _ hx.injective⟩, lift_le]

Premises used: Iff.mpr, Cardinal.lift_mk_eq', Nonempty.intro, Equiv.ofInjective, AlgebraicIndependent.injective, Cardinal.lift_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : AlgebraicIndependent R x
⊢ #(↑(range x) : Type v) ≤ trdeg R A

Tactic:
le_ciSup_of_le bddAbove_of_small ⟨_, hx.to_subtype_range⟩ le_rfl

Premises used: le_rfl, le_ciSup_of_le, Algebra.trdeg, Subtype.mk, Cardinal.bddAbove_of_small, AlgebraicIndependent.to_subtype_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : AlgebraicIndependent R x
⊢ #(↑(range x) : Type v) ≤ trdeg R A

Tactic:
exact le_ciSup_of_le bddAbove_of_small ⟨_, hx.to_subtype_range⟩ le_rfl

Premises used: le_rfl, le_ciSup_of_le, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
rw : lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)
⊢ #ι ≤ trdeg R A

Tactic:
rw [← (#ι).lift_id, ← (trdeg R A).lift_id]

Premises used: Cardinal.mk, Algebra.trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)

Tactic:
hx.lift_cardinalMk_le_trdeg

Premises used: AlgebraicIndependent.lift_cardinalMk_le_trdeg
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)

Tactic:
exact hx.lift_cardinalMk_le_trdeg

Premises used: AlgebraicIndependent.lift_cardinalMk_le_trdeg
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
rw :
  ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{v', v} #(↑(↑i : Set A) : Type v) ≤
    lift.{v, v'} (trdeg R A')
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')

Tactic:
rw [trdeg, lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Algebra.trdeg, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{v', v} #(↑(↑i : Set A) : Type v) ≤
    lift.{v, v'} (trdeg R A')

Tactic:
ciSup_le' fun i ↦ (i.2.map' hf).lift_cardinalMk_le_trdeg

Premises used: AlgebraicIndependent.map', ciSup_le', AlgebraicIndependent.lift_cardinalMk_le_trdeg, Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{v', v} #(↑(↑i : Set A) : Type v) ≤
    lift.{v, v'} (trdeg R A')

Tactic:
exact ciSup_le' fun i ↦ (i.2.map' hf).lift_cardinalMk_le_trdeg

Premises used: ciSup_le'
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective (α := A) (β := A') (⇑f : (a : A) → A')
rw : lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')
⊢ trdeg R A ≤ trdeg R A'

Tactic:
rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]

Premises used: Algebra.trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')

Tactic:
lift_trdeg_le_of_injective f hf

Premises used: lift_trdeg_le_of_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')

Tactic:
exact lift_trdeg_le_of_injective f hf

Premises used: lift_trdeg_le_of_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
rw :
  ⨆ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }), lift.{v, v'} #(↑(↑i : Set A') : Type v') ≤
    lift.{v', v} (trdeg R A)
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
rw [trdeg, lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Algebra.trdeg, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ ⨆ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }), lift.{v, v'} #(↑(↑i : Set A') : Type v') ≤
    lift.{v', v} (trdeg R A)

Tactic:
ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <|
    of_comp f ?_)

Premises used: ciSup_le', AlgebraicIndependent.lift_cardinalMk_le_trdeg, AlgebraicIndependent.of_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
refine :
  ∀ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }),
    AlgebraicIndependent.{v', u_2, v'} (ι := (↑(↑i : Set A') : Type v')) R (A := A')
      (Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A') fun (a : (↑(↑i : Set A') : Type v')) ↦
        invFun (⇑f : (a : A) → A') (↑a : A'))
⊢ ⨆ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }), lift.{v, v'} #(↑(↑i : Set A') : Type v') ≤
    lift.{v', v} (trdeg R A)

Tactic:
refine ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <|
    of_comp f ?_)

Premises used: ciSup_le'
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
i : { s : Set A' // AlgebraicIndepOn R _root_.id s }
⊢ AlgebraicIndepOn R _root_.id (↑i : Set A')

Tactic:
i.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h_1 : Nontrivial R
i : { s : Set A' // AlgebraicIndepOn R _root_.id s }
h :
  ∀ (x : (↑(↑i : Set A') : Type v')),
    Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A')
        (fun (a : (↑(↑i : Set A') : Type v')) ↦ invFun (⇑f : (a : A) → A') (↑a : A')) x =
      _root_.id (↑x : A')
⊢ AlgebraicIndependent.{v', u_2, v'} (ι := (↑(↑i : Set A') : Type v')) R (A := A')
    (Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A') fun (a : (↑(↑i : Set A') : Type v')) ↦
      invFun (⇑f : (a : A) → A') (↑a : A'))

Tactic:
convert! i.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
i : { s : Set A' // AlgebraicIndepOn R _root_.id s }
x : (↑(↑i : Set A') : Type v')
⊢ Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A')
      (fun (a : (↑(↑i : Set A') : Type v')) ↦ invFun (⇑f : (a : A) → A') (↑a : A')) x =
    _root_.id (↑x : A')

Tactic:
simp [invFun_eq (hf _)]

Premises used: Function.invFun_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective (α := A) (β := A') (⇑f : (a : A) → A')
rw : lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)
⊢ trdeg R A' ≤ trdeg R A

Tactic:
rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]

Premises used: Algebra.trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)

Tactic:
lift_trdeg_le_of_surjective f hf

Premises used: lift_trdeg_le_of_surjective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)

Tactic:
exact lift_trdeg_le_of_surjective f hf

Premises used: lift_trdeg_le_of_surjective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
⊢ lift.{v', v} (trdeg R A) = lift.{v, v'} (trdeg R A')

Tactic:
(lift_trdeg_le_of_injective e.toAlgHom e.injective).antisymm
    (lift_trdeg_le_of_surjective e.toAlgHom e.surjective)

Premises used: AlgEquiv.toAlgHom, lift_trdeg_le_of_injective, LE.le.antisymm, lift_trdeg_le_of_surjective, AlgEquiv.injective, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
rw : lift.{v, v} (trdeg R A) = trdeg R A'
rw₁ : lift.{v, v} (trdeg R A') = trdeg R A'
rw₂ rw₃ : trdeg R A' = trdeg R A'
⊢ trdeg R A = trdeg R A'

Tactic:
rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]

Premises used: Algebra.trdeg, AlgEquiv.lift_trdeg_eq, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
hf :
  ∀ (i : (↑s : Type u)),
    Eq.{v + 1} (α := A)
      ((aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type u) R) → A) (X i) : A)
      ((AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))) :
            (a : MvPolynomial (↑s : Type u) R) → A)
          (X i) :
        A)
⊢ Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
i : (↑s : Type u)
⊢ Eq.{v + 1} (α := A)
    ((aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type u) R) → A) (X i) : A)
    ((AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type u) R) → A)
        (X i) :
      A)

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
⊢ Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))

Tactic:
have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
this :
  Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))
⊢ ∀ (p : MvPolynomial.{u, u_2} (↑s : Type u) R),
    Eq (α := MvPolynomial ι R)
        ((rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial { x : ι // x ∈ s } R) → MvPolynomial ι R)
            p :
          MvPolynomial ι R)
        (0 : MvPolynomial ι R) ↔
      p = 0

Tactic:
have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
    (injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
      (rename_injective _ Subtype.val_injective)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
this_1 :
  Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))
this :
  ∀ (p : MvPolynomial.{u, u_2} (↑s : Type u) R),
    Eq (α := MvPolynomial ι R)
        ((rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial { x : ι // x ∈ s } R) → MvPolynomial ι R)
            p :
          MvPolynomial ι R)
        (0 : MvPolynomial ι R) ↔
      p = 0
⊢ AlgebraicIndependent (ι := (↑s : Type u)) R (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔
    ∀ (p : MvPolynomial ι R),
      Membership.mem (γ := Subalgebra R (MvPolynomial ι R)) (supported R s) p →
        Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0

Tactic:
simp [algebraicIndependent_iff, supported_eq_range_rename, *]

Premises used: algebraicIndependent_iff, MvPolynomial.supported_eq_range_rename
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) ↔
    ∀ (p : MvPolynomial A R),
      Membership.mem (γ := Subalgebra R (MvPolynomial A R)) (supported R s) p →
        Eq.{v + 1} (α := A) ((aeval _root_.id : (a : MvPolynomial A R) → A) p : A) (0 : A) → p = 0

Tactic:
apply @algebraicIndependent_comp_subtype _ _ _ id

Premises used: algebraicIndependent_comp_subtype