Theorem: PolynomialMap.Subalgebra.FG.exists_range_eq (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
B : Subalgebra R S
hB : B.FG
⊢ ∃ s, (PolynomialMap.φ R s).range = B
Tactic:
obtain ⟨s, hs⟩ := hB
State after:
case intro
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ ∃ s, (PolynomialMap.φ R s).range = B

State before:
case intro
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ ∃ s, (PolynomialMap.φ R s).range = B
Tactic:
use s
State after:
case h
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ (PolynomialMap.φ R s).range = B

State before:
case h
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ (PolynomialMap.φ R s).range = B
Tactic:
simp only [φ_range, hs]
State after:
no goals