awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (hypothesis)
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)
have this : AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
  (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
    (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
Tactic: have := hs.sumElim_comp ht
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)
have refine : #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
      (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
  lift.{u, v}
    #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                  (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                    (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                      _root_.id (↑i : S))))
                sorry) :
            Set A) :
        Type v)
Tactic: refine le_ciSup_of_le bddAbove_of_small ⟨_, this.to_subtype_range⟩ ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
have rw : #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
      (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
  lift.{max v u, v}
    #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                  (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                    (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                      _root_.id (↑i : S))))
                sorry) :
            Set A) :
        Type v)
Tactic: rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
rw :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{max v u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
have rw₁ : #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
      (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
  lift.{v, max u v} #(Sum.{v, u} (↑t : Type v) (↑s : Type u))
Tactic: rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
rw :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{max v u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
rw₁ :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{v, max u v} #(Sum.{v, u} (↑t : Type v) (↑s : Type u))
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
have rw₂ : #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
      (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
      (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u))
Tactic: rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type u
inst_4 : CommRing A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S A
inst_9 : IsScalarTower R S A
⊢ trdeg R S + trdeg S A ≤ trdeg R A
have rw : Cardinal.lift.{u, u} (trdeg R S) + Cardinal.lift.{u, u} (trdeg S A) ≤ Cardinal.lift.{u, u} (trdeg R A)
Tactic: rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
⊢ AlgebraicIndependent R x
have refine : ∀ (t : Set ι),
  t.Finite →
    (AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
      ∀ (i : ι) (hi : i ∉ t), Transcendental (↥(adjoin R (x '' t))) (x i)
Tactic: refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
⊢ adjoin R (x '' t) ≤ supported R t
have rw : t ⊆ x ⁻¹' (↑(supported R t) : Set (MvPolynomial ι R))
Tactic: rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h_1 : t.Finite
h_2 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
a : ι
h : a ∈ t
⊢ x a ∈ (↑(supported R t) : Set (MvPolynomial ι R))
have refine : Subset (α := Set (MvPolynomial ι R)) {X a} (X '' t)
Tactic: refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h_1 : t.Finite
h_2 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
a : ι
h : a ∈ t
⊢ Subset (α := Set (MvPolynomial ι R)) {X a} (X '' t)
have simp_rw : Membership.mem (γ := Set (MvPolynomial ι R)) (X '' t) (X a)
Tactic: simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)
have hle : adjoin R (x '' t) ≤ supported R t
Tactic: have hle : adjoin R (x '' t) ≤ supported R t := by
    rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
    intro _ h
    rw [Set.mem_preimage]
    refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
    simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : ι) ↦ (Polynomial.aeval (x i) : (a : Polynomial R) → A) (f i)
have h : ∀ (x_1 : ι),
  Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((Polynomial.aeval (X x_1) : (a : Polynomial R) → MvPolynomial ι R) (f x_1) : MvPolynomial ι R) :
      A)
Tactic: convert! aeval_of_algebraicIndependent hx (algebraicIndependent_polynomial_aeval_X _ hf)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((Polynomial.aeval (X x_1) : (a : Polynomial R) → MvPolynomial ι R) (f x_1) : MvPolynomial ι R) :
      A)
have h : Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
  ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) (f x_1) : A)
Tactic: rw [← AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) (f x_1) : A)
have h : Eq (α := Polynomial R →ₐ[R] A) (Polynomial.aeval (x x_1)) (AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
⊢ Eq (α := Polynomial R →ₐ[R] A) (Polynomial.aeval (x x_1)) (AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)))
have h : Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) Polynomial.X : A)
  ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) Polynomial.X : A)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Algebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra.IsIntegral R A
⊢ Eq (α := Submonoid A) (IsUnit.submonoid A : Submonoid A) (A⁰ : Submonoid A)
have h : ∀ (x : A),
  Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ↔ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
⊢ IsArtinian S M
have apply : Submodule S M ↪o Submodule R M
Tactic: apply (OrderEmbedding.wellFoundedLT (β := Submodule R M))
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
⊢ Submodule S M ↪o Submodule R M
have refine_1 : Submodule S M → Submodule R M
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
refine_1 : Submodule S M → Submodule R M
⊢ Submodule S M ↪o Submodule R M
have refine_2 : Function.Injective (β := Submodule R M) fun (N : Submodule S M) ↦
  let __AddSubmonoid := N.toAddSubmonoid;
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry }
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
refine_1 : Submodule S M → Submodule R M
refine_2 :
  Function.Injective (β := Submodule R M) fun (N : Submodule S M) ↦
    let __AddSubmonoid := N.toAddSubmonoid;
    { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ Submodule S M ↪o Submodule R M
have refine_3 : ∀ {a b : Submodule S M},
  LE.le (α := Submodule R M)
      (({
              toFun := fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry },
              inj' := sorry } :
            (a : Submodule S M) → Submodule R M)
          a :
        Submodule R M)
      (({
              toFun := fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry },
              inj' := sorry } :
            (a : Submodule S M) → Submodule R M)
          b :
        Submodule R M) ↔
    a ≤ b
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
⊢ Submodule R M
have refine_1 : ∀ (c : R) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier
Tactic: refine { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
c : R
x : M
hx : x ∈ N.carrier
⊢ c • x ∈ N.carrier
have refine_1 : ∀ (r : S), HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈ N.carrier
Tactic: obtain ⟨r, rfl⟩ := H c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈ N.carrier
have refine_1 : r • x ∈ N
Tactic: suffices r • x ∈ N by simpa [Algebra.algebraMap_eq_smul_one, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N1 N2 : Submodule S M
h :
  Eq.{u_2 + 1} (α := Submodule R M)
    ((fun (N : Submodule S M) ↦
        let __AddSubmonoid := N.toAddSubmonoid;
        ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
      N1)
    ((fun (N : Submodule S M) ↦
        let __AddSubmonoid := N.toAddSubmonoid;
        ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
      N2)
⊢ N1 = N2
have refine_2 : ∀
  (h :
    ∀ (x : M),
      Membership.mem (γ := Submodule R M)
          ((fun (N : Submodule S M) ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry } : Submodule R M))
            N1)
          x ↔
        Membership.mem (γ := Submodule R M)
          ((fun (N : Submodule S M) ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry } : Submodule R M))
            N2)
          x)
  (x : M), x ∈ N1 ↔ x ∈ N2
Tactic: rwa [Submodule.ext_iff] at h ⊢
Cleared hypotheses: h