-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma EssFiniteType.aux (σ : Subalgebra R S)
    (hσ : ∀ s : S, ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ)
    (τ : Set T) (t : T) (ht : t ∈ Algebra.adjoin S τ) :
    ∃ s ∈ σ, IsUnit s ∧ s • t ∈ σ.map (IsScalarTower.toAlgHom R S T) ⊔ Algebra.adjoin R τ

Proof state:
case refine_2.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
⊢ (algebraMap S T) (s * s') ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ

Tactic:
exact ⟨_, hs₃, rfl⟩

Result:
no goals

Proof state:
case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (x y : T),
    x ∈ adjoin S τ →
      y ∈ adjoin S τ →
        (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
          (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
            ∃ s ∈ σ, IsUnit s ∧ s • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
rintro x y - - ⟨sx, hsx, hsx', hsx''⟩ ⟨sy, hsy, hsy', hsy''⟩

Result:
case refine_3.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx * sy) • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]

Result:
case refine_4.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sx • x * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Proof state:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
s : S
⊢ ∃ s_1 ∈ σ, IsUnit s_1 ∧ s_1 • (algebraMap S T) s ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
obtain ⟨s', hs₁, hs₂, hs₃⟩ := hσ s

Result:
case refine_2.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
⊢ ∃ s_1 ∈ σ, IsUnit s_1 ∧ s_1 • (algebraMap S T) s ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Proof state:
case refine_3.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx * sy) • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
rw [smul_add, mul_smul, mul_smul, Algebra.smul_def sx (sy • y), smul_comm,
  Algebra.smul_def sy (sx • x)]

Result:
case refine_3.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sy * sx • x + (algebraMap S T) sx * sy • y ∈
    Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩

Result:
case refine_4.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx * sy) • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ