-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
r : presM.R
w : Finsupp.{u_5, u_1} presM.R B
h_1 : r ∉ w.support
hw :
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    w
β : Finsupp.{u_6, u_3} presB.G A
h_2 : Ne.{u_1 + 1} (α := B) ((presB.π : (a : presB.G →₀ A) → B) β : B) (0 : B)
h :
  Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) 0) : Finsupp.{u_5, u_1} presM.R B)
⊢ Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) β) : Finsupp.{u_5, u_1} presM.R B)
have h₁ : ∀ (a : presB.G) (b : A) (f : Finsupp.{u_6, u_3} presB.G A),
  a ∉ f.support →
    b ≠ 0 →
      Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range
              fun
                (x :
                  Prod.{u_6, u_5}
                    (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
                    (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) f) : Finsupp.{u_5, u_1} presM.R B) →
        Membership.mem (α := Finsupp.{u_5, u_1} presM.R B) (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
          (Submodule.span A
            (Set.range
              fun
                (x :
                  Prod.{u_6, u_5}
                    (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
                    (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
              HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
          (Finsupp.single r ((presB.π : (a : presB.G →₀ A) → B) (Finsupp.single a b + f)) :
            Finsupp.{u_5, u_1} presM.R B)
Tactic: apply Finsupp.induction (motive := fun β ↦ Finsupp.single r (presB.π β) ∈ _)