awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
⊢ ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t
have suffices : Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
  (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
Tactic: suffices h_surj : Function.Surjective ((φ.rangeRestrict.toLinearMap).rTensor M) by
    obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
    use p
    rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
⊢ ∃ (a : lifts R M S), π R M S a = t
have obtain : ∀ (B : Subalgebra R S) (hB : B.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
  ∃ (a : lifts R M S), π R M S a = t
Tactic: obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
⊢ ∃ (a : lifts R M S), π R M S a = t
have obtain : ∀ (s : Finset S) (hs : AlgHom.range (φ R s) = B), ∃ (a : lifts R M S), π R M S a = t
Tactic: obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
s : Finset S
hs : AlgHom.range (φ R s) = B
⊢ ∃ (a : lifts R M S), π R M S a = t
have obtain : ∀ (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t),
  ∃ (a : lifts R M S), π R M S a = t
Tactic: obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
⊢ Function.Surjective (α := lifts R M S) (β := S ⊗[R] M) (π R M S)
have intro : ∀ (t : S ⊗[R] M), ∃ (a : lifts R M S), π R M S a = t
Tactic: classical
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
intro : ∀ (t : S ⊗[R] M), ∃ (a : lifts R M S), π R M S a = t
⊢ Function.Surjective (α := lifts R M S) (β := S ⊗[R] M) (π R M S)
have intro₁ : ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
  ∃ (a : lifts R M S), π R M S a = t
Tactic: classical
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
intro : ∀ (t : S ⊗[R] M), ∃ (a : lifts R M S), π R M S a = t
intro₁ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
    ∃ (a : lifts R M S), π R M S a = t
⊢ Function.Surjective (α := lifts R M S) (β := S ⊗[R] M) (π R M S)
have intro₂ : ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t) (s : Finset S)
  (hs : AlgHom.range (φ R s) = B), ∃ (a : lifts R M S), π R M S a = t
Tactic: classical
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
intro : ∀ (t : S ⊗[R] M), ∃ (a : lifts R M S), π R M S a = t
intro₁ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
    ∃ (a : lifts R M S), π R M S a = t
intro₂ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t) (s : Finset S)
    (hs : AlgHom.range (φ R s) = B), ∃ (a : lifts R M S), π R M S a = t
⊢ Function.Surjective (α := lifts R M S) (β := S ⊗[R] M) (π R M S)
have intro₃ : ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t) (s : Finset S)
  (hs : AlgHom.range (φ R s) = B) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t),
  ∃ (a : lifts R M S), π R M S a = t
Tactic: classical
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
have obtain : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
have w : ℕ
Tactic: use s.card, φ R s, p, ha
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
w : ℕ
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
have w₁ : MvPolynomial (Fin s.card) R →ₐ[R] S
Tactic: use s.card, φ R s, p, ha
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
w : ℕ
w₁ : MvPolynomial (Fin s.card) R →ₐ[R] S
w₂ : MvPolynomial (Fin s.card) R ⊗[R] M
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
have h : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t
Tactic: use s.card, φ R s, p, ha
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain : ∀ (A : Subalgebra R S) (hA : A.FG)
  (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
Tactic: have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain : ∀ (gen : Finset S) (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have hAB : A ≤ A ⊔ Algebra.adjoin R (↑{s} : Set S)
Tactic: have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ A ⊔ Algebra.adjoin R (↑{s} : Set S)
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have hAB₁ : A ≤ AlgHom.range (φ R gen)
Tactic: rw [← hgen] at hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have obtain : ∀ (p : MvPolynomial (Fin gen.card) R ⊗[R] M)
  (hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t),
  ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
Tactic: obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
have rw : s ∈ A ⊔ Algebra.adjoin R (↑{s} : Set S)
Tactic: rw [hgen]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R (↑{s} : Set S)
have a : s ∈ (↑A : Set S) ⊔ (↑(Algebra.adjoin R (↑{s} : Set S)) : Set S)
Tactic: apply Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ s ∈ (↑A : Set S) ⊔ (↑(Algebra.adjoin R (↑{s} : Set S)) : Set S)
have a : s ∈ A ∨ Membership.mem (γ := Subalgebra R S) R[s] s
Tactic: simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
Tactic: have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have w : ℕ
Tactic: use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
w : ℕ
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have w₁ : MvPolynomial (Fin gen.card) R →ₐ[R] S
Tactic: use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
w : ℕ
w₁ : MvPolynomial (Fin gen.card) R →ₐ[R] S
w₂ : MvPolynomial (Fin gen.card) R ⊗[R] M
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have w₃ : MvPolynomial (Fin gen.card) R
Tactic: use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG
gen : Finset S
hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)
hAB : A ≤ AlgHom.range (φ R gen)
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s
w : ℕ
w₁ : MvPolynomial (Fin gen.card) R →ₐ[R] S
w₂ : MvPolynomial (Fin gen.card) R ⊗[R] M
w₃ : MvPolynomial (Fin gen.card) R
left : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
have right : (φ R gen : (a : MvPolynomial (Fin gen.card) R) → S)
    (Exists.choose (p := fun (y : MvPolynomial (Fin gen.card) R) ↦
      (toRingHom (φ R gen) : (a : MvPolynomial (Fin gen.card) R) → S) y = s) hs) =
  s
Tactic: use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec