awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst_3 : CommRing S
inst_4 : CommRing B
inst_5 : Algebra S B
inst_6 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : MvPolynomial ι R
hp :
  Eq.{u_4 + 1} (α := B)
    ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
        ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S) :
      B)
    (0 : B)
rw : Eq (α := MvPolynomial ι S) ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) 0) 0
rw₁ rw₂ : Eq (α := MvPolynomial ι S) 0 0
⊢ Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S)
    (0 : MvPolynomial ι S)

Tactic:
rw [H q (hg (by rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom])), map_zero]

Premises used: map_zero
-- 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 : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst_3 : CommRing S
inst_4 : CommRing B
inst_5 : Algebra S B
inst_6 : EquivLike FRS R S
inst_7 : RingEquivClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
⊢ AlgebraicIndependent.{u, u_3, u_4} S (A := B) ((⇑g : (a : A) → B) ∘ x) ↔ AlgebraicIndependent R x

Tactic:
⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.injective f) h,
    fun H ↦ H.ringHom_of_comp_eq f g (EquivLike.surjective f) hg h⟩

Premises used: AlgebraicIndependent.of_ringHom_of_comp_eq, Iff.intro, EquivLike.surjective, EquivLike.injective, AlgebraicIndependent.ringHom_of_comp_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
s : Set A
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
obtain :
  ∀ (x : A) (h : x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t),
    (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x h) : A) ∈ s
⊢ (↑x : A) ∈ s

Tactic:
obtain ⟨x, h⟩ := x
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
x : A
h : x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
⊢ ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = x

Tactic:
rw [Finset.mem_map] at h

Premises used: Finset.mem_map
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
x : A
h_1 : x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
h : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = x
obtain :
  ∀ a ∈ t,
    ∀
      (h :
        Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a : A)),
      Membership.mem (α := A) s
        ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
                ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) h) :
            A) :
          A)
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x h_1) : A) ∈ s

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

Premises used: rfl
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
a : { x : A // x ∈ s }
left : a ∈ t
h :
  Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
    ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a : A)
⊢ Membership.mem (α := A) s
    ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
            ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) h) :
        A) :
      A)

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

Premises used: Subtype.coe_prop, Function.Embedding.coe_subtype
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
⊢ AlgebraicIndependent R (Subtype.val (p := fun (x : A) ↦ x ∈ s) ∘ f)

Tactic:
AlgebraicIndependent.comp li f _

Premises used: AlgebraicIndependent.comp
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
convert! : Injective f
⊢ AlgebraicIndependent.{v, u_2, v} (ι := ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) R
    (Subtype.val (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))

Tactic:
convert! AlgebraicIndependent.comp li f _

Premises used: AlgebraicIndependent.comp
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
x : A
hx : x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
y : A
hy : y ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
rw :
  ∀ (hx_1 : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = x) (y : A)
    (hy : y ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
    (hy_1 : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = y),
    f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx) =
        f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy) →
      Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx =
        Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy
⊢ f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx) =
      f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy) →
    Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx =
      Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy

Tactic:
rw [Finset.mem_map] at hx hy

Premises used: Finset.mem_map
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
x : A
hx_1 : x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
hx : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = x
y : A
hy_1 : y ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
hy : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = y
obtain :
  ∀ a ∈ t,
    ∀
      (hx :
        Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a : A)),
      f
            (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
              ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx) =
          f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1) →
        Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
            ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx =
          Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1
⊢ f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx_1) =
      f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1) →
    Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x hx_1 =
      Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1

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

Premises used: rfl
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
y : A
hy_1 : y ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t
hy : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = y
a : { x : A // x ∈ s }
left : a ∈ t
hx :
  Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
    ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a : A)
obtain :
  ∀ b ∈ t,
    ∀
      (hy :
        Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b : A)),
      f
            (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
              ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx) =
          f
            (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
              ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b) hy) →
        Eq (α := ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))
          (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
              ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx :
            ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))
          (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
              ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b) hy :
            ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))
⊢ f
        (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx) =
      f (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1) →
    Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
        ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx =
      Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) y hy_1

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

Premises used: rfl
-- 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
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
f : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) → (↑s : Type v) :=
  fun (x : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ s) (↑x : A) ⋯
a : { x : A // x ∈ s }
left : a ∈ t
hx :
  Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
    ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a : A)
b : { x : A // x ∈ s }
left_1 : b ∈ t
hy :
  Membership.mem (α := A) (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
    ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b : A)
⊢ f
        (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx) =
      f
        (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b) hy) →
    Eq (α := ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))
      (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a) hx :
        ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))
      (Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)
          ((Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) b) hy :
        ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t))

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

Premises used: imp_self, Subtype.mk_eq_mk
-- 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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R (A := A) fun (i : ↥s) ↦ (↑i : A)) → s.card ≤ n
s : Set A
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
H₁ : ∀ (s_1 : Finset (↑s : Type v)), s_1.card ≤ n
⊢ Cardinal.mk (↑s : Type v) ≤ (↑n : Cardinal.{v})

Tactic:
apply Cardinal.card_le_of

Premises used: Cardinal.card_le_of
-- 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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R (A := A) fun (i : ↥s) ↦ (↑i : A)) → s.card ≤ n
s : Set A
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
H₁ : (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t).card ≤ n
⊢ t.card ≤ n

Tactic:
rw [← Finset.card_map (Embedding.subtype (· ∈ s))]

Premises used: Finset.card_map, Membership.mem, Function.Embedding.subtype
-- 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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R (A := A) fun (i : ↥s) ↦ (↑i : A)) → s.card ≤ n
s : Set A
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
H₁ : AlgebraicIndependent R (A := A) fun (i : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ (↑i : A)
⊢ (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t).card ≤ n

Tactic:
apply H
-- 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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R (A := A) fun (i : ↥s) ↦ (↑i : A)) → s.card ≤ n
s : Set A
li : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
t : Finset (↑s : Type v)
⊢ AlgebraicIndependent R (A := A) fun (i : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ (↑i : A)

Tactic:
apply algebraicIndependent_finset_map_embedding_subtype _ li

Premises used: algebraicIndependent_finset_map_embedding_subtype
-- 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 ι
hs : AlgebraicIndependent (ι := (↑s : Type u)) R (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
⊢ AlgebraicIndependent R (s.restrict (π := fun (a : ι) ↦ A) x)

Tactic:
hs

Premises used: Set.restrict
-- 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
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // Membership.mem (γ := Set A) ∅ x }) R
      (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) ∅ x)) ↔
    Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → 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
hx : AlgebraicIndependent R x
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
hx : AlgebraicIndependent R x
h : Nontrivial R
rwa rwa₁ rwa₂ rwa₃ : AlgebraicIndependent R x
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
rwa [algebraicIndependent_subtype_range hx.injective]

Premises used: algebraicIndependent_subtype_range, AlgebraicIndependent.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
hx : AlgebraicIndependent R x
t : Set A
ht : range x = t
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
ht ▸ hx.to_subtype_range

Premises used: Eq.rec, 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
hx : IsTranscendenceBasis R x
inl :
  Subsingleton R →
    IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
      (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
inr :
  Nontrivial R →
    IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
      (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
hx : IsTranscendenceBasis R x
h : Subsingleton R
inl : ∀ (hx : Nonempty ι), Subsingleton R → Nonempty.{v + 1} { x_1 : A // x_1 ∈ range x }
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢

Premises used: isTranscendenceBasis_iff_of_subsingleton
-- 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
hx : Nonempty ι
h : Subsingleton R
⊢ Nonempty.{v + 1} { x_1 : A // x_1 ∈ range x }

Tactic:
infer_instance
-- 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
hx : IsTranscendenceBasis R x
h : Nontrivial R
inr inr₁ inr₂ inr₃ : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
rwa [isTranscendenceBasis_subtype_range hx.1.injective]

Premises used: isTranscendenceBasis_subtype_range, And.left, AlgebraicIndependent.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
hx : IsTranscendenceBasis R x
t : Set A
ht : range x = t
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
ht ▸ hx.to_subtype_range

Premises used: Eq.rec, IsTranscendenceBasis.to_subtype_range
-- 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)
⊢ IsTranscendenceBasis R x

Tactic:
⟨(AlgHom.algebraicIndependent_iff f h).mp H.1, ?_⟩

Premises used: IsTranscendenceBasis, And.left, AlgHom.algebraicIndependent_iff, And.intro, Iff.mp
-- 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)
refine : ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range x ⊆ s → range x = s
⊢ IsTranscendenceBasis R x

Tactic:
refine ⟨(AlgHom.algebraicIndependent_iff f h).mp H.1, ?_⟩
-- 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
rw : Subset.{v'} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)
⊢ Subset.{v'} (α := Set A') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)

Tactic:
rw [Set.range_comp]

Premises used: Set.range_comp