awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₁ : Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₂ :
  Eq.{u_4 + 1} (α := B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) fun (i : ι) ↦
            ((↑g : A →+* B) : (a : A) → B) (x i) :
          (a : MvPolynomial ι R) → B)
        q :
      B)
    (0 : B)
rwa₃ :
  Eq.{u_4 + 1} (α := B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S)) fun (i : ι) ↦
            ((↑g : A →+* B) : (a : A) → B) (x i) :
          (a : MvPolynomial ι R) → B)
        q :
      B)
    (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa₄ : Eq.{u_4 + 1} (α := B)
  ((eval₂Hom (algebraMap S B) fun (i : ι) ↦ ((↑g : A →+* B) : (a : A) → B) (x i) : (a : MvPolynomial ι S) → B)
      ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S) :
    B)
  (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₁ : Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₂ :
  Eq.{u_4 + 1} (α := B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) fun (i : ι) ↦
            ((↑g : A →+* B) : (a : A) → B) (x i) :
          (a : MvPolynomial ι R) → B)
        q :
      B)
    (0 : B)
rwa₃ :
  Eq.{u_4 + 1} (α := B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S)) fun (i : ι) ↦
            ((↑g : A →+* B) : (a : A) → B) (x i) :
          (a : MvPolynomial ι R) → B)
        q :
      B)
    (0 : B)
rwa₄ :
  Eq.{u_4 + 1} (α := B)
    ((eval₂Hom (algebraMap S B) fun (i : ι) ↦ ((↑g : A →+* B) : (a : A) → B) (x i) : (a : MvPolynomial ι S) → B)
        ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S) :
      B)
    (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa₅ : Eq.{u_4 + 1} (α := B)
  ((aeval fun (i : ι) ↦ ((↑g : A →+* B) : (a : A) → B) (x i) : (a : MvPolynomial ι S) → B)
      ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S) :
    B)
  (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
⊢ Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
have rw : Eq (α := MvPolynomial ι S) ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) 0) 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
have rw₁ : Eq (α := MvPolynomial ι S) 0 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
⊢ (↑x : A) ∈ s
have 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
Tactic: obtain ⟨x, h⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x h) : A) ∈ s
have h₁ : ∃ a ∈ t, (Embedding.subtype fun (x : A) ↦ x ∈ s : (a : { x : A // x ∈ s }) → A) a = x
Tactic: rw [Finset.mem_map] at h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t) x h_1) : A) ∈ s
have 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)
Tactic: obtain ⟨a, _, rfl⟩ := h
Cleared hypotheses: x, h_1, h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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.{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))
have convert! : Injective f
Tactic: convert! AlgebraicIndependent.comp li f _
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_map] at hx hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨a, _, rfl⟩ := hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
⊢ 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
have 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))
Tactic: obtain ⟨b, _, rfl⟩ := hy
Cleared hypotheses: y, hy_1, hy
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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))
⊢ Cardinal.mk (↑s : Type v) ≤ (↑n : Cardinal.{v})
have H₁ : ∀ (s_1 : Finset (↑s : Type v)), s_1.card ≤ n
Tactic: apply Cardinal.card_le_of
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
⊢ t.card ≤ n
have H₁ : (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t).card ≤ n
Tactic: rw [← Finset.card_map (Embedding.subtype (· ∈ s))]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
⊢ (Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t).card ≤ n
have H₁ : AlgebraicIndependent R (A := A) fun (i : ↥(Finset.map (Embedding.subtype fun (x : A) ↦ x ∈ s) t)) ↦ (↑i : A)
Tactic: apply H
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have 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))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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))
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have 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))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ IsTranscendenceBasis.{v, u_2, v} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have inl : ∀ (hx : Nonempty ι), Subsingleton R → Nonempty.{v + 1} { x_1 : A // x_1 ∈ range x }
Tactic: rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
have refine : ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range x ⊆ s → range x = s
Tactic: refine ⟨(AlgHom.algebraicIndependent_iff f h).mp H.1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)
have rw : Subset.{v'} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)
Tactic: rw [Set.range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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
⊢ range x = s
have this : 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')