Theorem: PolynomialMap.exists_lift' (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
classical
choose A hA ht using TensorProduct.Algebra.exists_of_fg t
have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
  Subalgebra.fg_sup hA (Subalgebra.fg_adjoin_finset _)
choose gen hgen using Subalgebra.FG.exists_range_eq hB
have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
rw [← hgen] at hAB
choose p hp using exists_lift_of_le_rTensor_range M _ hAB t ht
have : 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)
choose q hq using this
use gen.card, φ R gen, p, q, hp, hq
State after:
no goals

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose A hA ht using TensorProduct.Algebra.exists_of_fg t
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
  Subalgebra.fg_sup hA (Subalgebra.fg_adjoin_finset _)
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose gen hgen using Subalgebra.FG.exists_range_eq hB
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
rw [← hgen] at hAB
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose p hp using exists_lift_of_le_rTensor_range M _ hAB t ht
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have : 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)
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
this : s ∈ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
this : s ∈ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose q hq using this
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
q : MvPolynomial (Fin gen.card) R
hq : (PolynomialMap.φ R gen).toRingHom q = s
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
q : MvPolynomial (Fin gen.card) R
hq : (PolynomialMap.φ R gen).toRingHom q = s
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
use gen.card, φ R gen, p, q, hp, hq
State after:
no goals

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ (PolynomialMap.φ R gen).range
Tactic:
rw [hgen]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}
Tactic:
apply Algebra.subset_adjoin
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ ↑A ⊔ ↑(Algebra.adjoin R ↑{s})

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ ↑A ⊔ ↑(Algebra.adjoin R ↑{s})
Tactic:
simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ∨ s ∈ Algebra.adjoin R {s}

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ∨ s ∈ Algebra.adjoin R {s}
Tactic:
exact Or.inr (Algebra.subset_adjoin rfl)
State after:
no goals