awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (hypothesis)
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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
hw :
  ∀ (g : A ⊗[R] B),
    Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g →
      (g *
          b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
        (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
            m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) *
          g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b
have hw₁ : HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] 1)
    (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
      m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
  HMul.hMul (α := A ⊗[R] B)
    (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
      m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
    (x ⊗ₜ[R] 1)
Tactic: specialize hw (x ⊗ₜ[R] 1) ⟨x, hx, rfl⟩
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (hypothesis)
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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw :
  HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] 1)
      (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
        m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) =
    HMul.hMul (α := A ⊗[R] B)
      (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
        m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
      (x ⊗ₜ[R] 1)
⊢ x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b
have hw₁ : Eq (α := A ⊗[R] B)
  (∑ i ∈ b.support,
    HMul.hMul (β := A) x ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) ⊗ₜ[R]
      (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
  (∑ i ∈ b.support,
    HMul.hMul (α := A) ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) x ⊗ₜ[R]
      (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
Tactic: simp only [Finsupp.sum, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul, one_mul,
      Finset.sum_mul, mul_one] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw :
  Eq (α := A ⊗[R] B)
    (∑ i ∈ b.support,
      HMul.hMul (β := A) x ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) ⊗ₜ[R]
        (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
    (∑ i ∈ b.support,
      HMul.hMul (α := A) ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) x ⊗ₜ[R]
        (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
⊢ x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b
have h : Eq (α := A ⊗[R] B)
  (((lsum R :
            (a : Module.Free.ChooseBasisIndex R B → A →ₗ[R] A ⊗[R] B) →
              (Module.Free.ChooseBasisIndex R B →₀ A) →ₗ[R] A ⊗[R] B)
          fun (i : Module.Free.ChooseBasisIndex R B) ↦
          (LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
            ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) :
        (a : Module.Free.ChooseBasisIndex R B →₀ A) → A ⊗[R] B)
      (x • b) :
    A ⊗[R] B)
  (((lsum R :
            (a : Module.Free.ChooseBasisIndex R B → A →ₗ[R] A ⊗[R] B) →
              (Module.Free.ChooseBasisIndex R B →₀ A) →ₗ[R] A ⊗[R] B)
          fun (i : Module.Free.ChooseBasisIndex R B) ↦
          (LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
            ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) :
        (a : Module.Free.ChooseBasisIndex R B →₀ A) → A ⊗[R] B)
      (mapRange (fun (x_1 : A) ↦ x_1 * x) sorry b) :
    A ⊗[R] B)
Tactic: refine TensorProduct.sum_tmul_basis_right_injective ℬ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Finsupp.{u_3, u_2} (Module.Free.ChooseBasisIndex R B) A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw :
  Eq (α := A ⊗[R] B)
    (∑ i ∈ b.support,
      HMul.hMul (β := A) x ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) ⊗ₜ[R]
        (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
    (∑ i ∈ b.support,
      HMul.hMul (α := A) ((b : (a : Module.Free.ChooseBasisIndex R B) → A) i : A) x ⊗ₜ[R]
        (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
⊢ Eq (α := A ⊗[R] B)
    ((x • b).sum fun (i : Module.Free.ChooseBasisIndex R B) ↦
      (⇑((LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
              ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) :
            A →ₗ[R] A ⊗[R] B) :
        (a : A) → A ⊗[R] B))
    (sum (M := A) (mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b) fun (i : Module.Free.ChooseBasisIndex R B) ↦
      (⇑((LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
              ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i) :
            A →ₗ[R] A ⊗[R] B) :
        (a : A) → A ⊗[R] B))
have h : Eq (α := A ⊗[R] B)
  (∑ x_1 ∈ b.support,
    (((LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
            ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) x_1) :
          A →ₗ[R] A ⊗[R] B) :
        (a : A) → A ⊗[R] B)
      ((x • b : (a : Module.Free.ChooseBasisIndex R B) → A) x_1))
  (∑ x_1 ∈ b.support,
    (((LinearMap.flip (TensorProduct.mk R A B) : (a : B) → A →ₗ[R] A ⊗[R] B)
            ((ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) x_1) :
          A →ₗ[R] A ⊗[R] B) :
        (a : A) → A ⊗[R] B)
      ((mapRange (fun (x_2 : A) ↦ x_2 * x) sorry b : (a : Module.Free.ChooseBasisIndex R B) → A) x_1))
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
w : TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B
x : A
hx : x ∈ S
⊢ HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
have h : HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
    ((AlgHom.toRingHom
            (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) :
          (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
        0 :
      A ⊗[R] B) =
  HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
    ((AlgHom.toRingHom
            (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) :
          (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
        0 :
      A ⊗[R] B)
    ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
Tactic: 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]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
w : TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B
x : A
hx : x ∈ S
h :
  HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          0 :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          0 :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
⊢ HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
have h₁ : ∀ (b : ↥(centralizer R S)) (c : B),
  HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          (b ⊗ₜ[R] c) :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (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) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          (b ⊗ₜ[R] c) :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
Tactic: 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]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
⊢ 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))
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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
⊢ 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))
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (hypothesis)
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 B
inst_5 : Module.Free R A
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
have eq1 : Eq (α := Subalgebra R (B ⊗[R] A)) (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S) : Subalgebra R (B ⊗[R] A))
  (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
      (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
        TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
    Subalgebra R (B ⊗[R] A))
Tactic: have eq1 := centralizer_coe_image_includeLeft_eq_center_tensorProduct R B A S
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (hypothesis)
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 B
inst_5 : Module.Free R A
eq1 :
  Eq (α := Subalgebra R (B ⊗[R] A)) (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S) : Subalgebra R (B ⊗[R] A))
    (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
          TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A) :
      Subalgebra R (B ⊗[R] A))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
have eq1₁ : Eq (α := Subalgebra R (A ⊗[R] B))
  (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
    (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
  (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
    (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
      (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
        TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A)))
Tactic: apply_fun Subalgebra.comap (Algebra.TensorProduct.comm R A B).toAlgHom at eq1
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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 B
inst_5 : Module.Free R A
eq1 :
  Eq (α := Subalgebra R (A ⊗[R] B))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
          TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
have h : Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S))
  (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
    (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
Tactic: convert! eq1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Centralizer (goal)
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 B
inst_5 : Module.Free R A
eq1 :
  Eq (α := Subalgebra R (A ⊗[R] B))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
          TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A)))
h :
  Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))
have h₁ : Eq (α := Subalgebra R (A ⊗[R] B))
  (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S))
      (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R S)) :
        TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S) →ₐ[R] A ⊗[R] B) :
    Subalgebra R (A ⊗[R] B))
  (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (AlgHom.range (A := TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A)
        (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R A) :
          TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A →ₐ[R] B ⊗[R] A)) :
    Subalgebra R (A ⊗[R] B))
Tactic: convert! eq1