-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
let let₁ let₂ : ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
let₃ :
  let s := image₂ f (x ∪ y * y) y;
  ∀
    (hxy :
      ∀ xi ∈ x,
        Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi),
    ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
let₄ :
  let s := image₂ f (x ∪ y * y) y;
  ∀
    (hxy :
      ∀ xi ∈ x,
        Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi)
    (hyy :
      HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
        span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)),
    ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
let₅ :
  let s := image₂ f (x ∪ y * y) y;
  ∀
    (hxy :
      ∀ xi ∈ x,
        Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi)
    (hyy :
      HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
        span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)),
    Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤
convert_3 :
  let s := image₂ f (x ∪ y * y) y;
  ∀
    (hxy :
      ∀ xi ∈ x,
        Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi)
    (hyy :
      HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
        span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)),
    Eq (α := Submodule A C)
      (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
        (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)))
      (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B))) ⊤)
convert_3₁ :
  let s := image₂ f (x ∪ y * y) y;
  ∀
    (hxy :
      ∀ xi ∈ x,
        Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi)
    (hyy :
      HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
        span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)),
    (↑(Submonoid.closure (↑x : Set C)) : Set C) ⊆
      (↑(restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
            (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))) :
        Set C)
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
classical
  let s : Finset B := Finset.image₂ f (x ∪ y * y) y
  have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
  have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
  refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
  convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
  rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
  refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr

Premises used: eq_top_iff, Submodule.restrictScalars_top, Algebra.top_toSubmodule, Algebra.adjoin_eq_span, Submodule.span_le