-- Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
h :
  ∀ (w : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w ↔
      Membership.mem (γ := Subalgebra R (A ⊗[R] B))
        (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
            (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
              TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
          Subalgebra R (A ⊗[R] B))
        w
h₁ :
  ∀ (w : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w →
      Membership.mem (γ := Subalgebra R (A ⊗[R] B))
        (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
            (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
              TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
          Subalgebra R (A ⊗[R] B))
        w
h₂ h₃ :
  ∀ (w : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B))
        (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
            (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
              TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
          Subalgebra R (A ⊗[R] B))
        w →
      Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
classical
  ext w
  constructor
  · intro hw
    rw [mem_centralizer_iff] at hw
    let ℬ := Module.Free.chooseBasis R B
    obtain ⟨b, rfl⟩ := TensorProduct.eq_repr_basis_right ℬ w
    refine Subalgebra.sum_mem _ fun j hj => ⟨⟨b j, ?_⟩ ⊗ₜ[R] ℬ j, by simp⟩
    rw [Subalgebra.mem_centralizer_iff]
    intro x hx
    suffices x • b = b.mapRange (· * x) (by simp) from Finsupp.ext_iff.1 this j
    specialize hw (x ⊗ₜ[R] 1) ⟨x, hx, rfl⟩
    simp only [Finsupp.sum, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul, one_mul,
      Finset.sum_mul, mul_one] at hw
    refine TensorProduct.sum_tmul_basis_right_injective ℬ ?_
    simp only [Finsupp.coe_lsum]
    rw [sum_of_support_subset (s := b.support) (hs := Finsupp.support_smul) (h := by simp),
      sum_of_support_subset (s := b.support) (hs := support_mapRange) (h := by simp)]
    simpa only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, LinearMap.flip_apply,
      TensorProduct.mk_apply, Finsupp.mapRange_apply] using hw
  · rintro ⟨w, rfl⟩
    rw [Subalgebra.mem_centralizer_iff]
    rintro _ ⟨x, hx, rfl⟩
    induction w using TensorProduct.induction_on with
    | zero => simp
    | tmul b c =>
      simp [Subalgebra.mem_centralizer_iff _ |>.1 b.2 x hx]
    | add y z hy hz => rw [map_add, mul_add, hy, hz, add_mul]

Premises used: Finsupp.mapRange_apply, add_mul, Finset.mul_sum, TensorProduct.mk_apply, Finsupp.sum, map_add, Algebra.TensorProduct.tmul_mul_tmul, LinearMap.flip_apply, Finsupp.coe_lsum, Finsupp.coe_smul, mul_add, TensorProduct.tmul, smul_eq_mul, mul_one, one_mul, rfl, Finset.sum_mul, Pi.smul_apply, Subalgebra.mem_centralizer_iff