awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ℬ : 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)
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) ⋯ b) :
      A ⊗[R] B)
⊢ x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b

Tactic:
refine TensorProduct.sum_tmul_basis_right_injective ℬ ?_

Premises used: TensorProduct.sum_tmul_basis_right_injective
-- 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
ℬ : 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)
⊢ ∀ i ∈ b.support,
    Eq (α := A ⊗[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)
        0)
      0

Tactic:
simp
-- 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
ℬ : 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)
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) ⋯ b : (a : Module.Free.ChooseBasisIndex R B) → A) x_1))
⊢ 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))

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)]

Premises used: Finsupp.support_mapRange, Finsupp.support_smul, Finsupp.sum_of_support_subset
-- 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
ℬ : 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_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) ⋯ b : (a : Module.Free.ChooseBasisIndex R B) → A) x_1))

Tactic:
simpa only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, LinearMap.flip_apply,
      TensorProduct.mk_apply, Finsupp.mapRange_apply] using hw

Premises used: Finsupp.mapRange_apply, TensorProduct.mk_apply, LinearMap.flip_apply, Finsupp.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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
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)
          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:
simp
-- 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
x : A
hx : x ∈ S
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:
simp [Subalgebra.mem_centralizer_iff _ |>.1 b.2 x hx]

Premises used: Iff.mp, Subtype.property, Subalgebra.mem_centralizer_iff
-- 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 B
inst_5 : Module.Free R A
⊢ 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
-- 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 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))
    (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

Premises used: AlgEquiv.toAlgHom, Algebra.TensorProduct.comm, Subalgebra.comap
-- 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 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))
    (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:
eq1
-- 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 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)))
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))
⊢ 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))

Tactic:
convert! eq1
-- 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 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 :
  ∀ (x : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S)) x ↔
      Membership.mem (γ := 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)))
        x
⊢ 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:
ext x
-- 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 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)))
x : A ⊗[R] B
h : ∀ a ∈ S, 1 ⊗ₜ[R] a * x = x * 1 ⊗ₜ[R] a
b : B
hb : b ∈ S
⊢ Eq (α := A ⊗[R] B)
    ((AlgEquiv.symm (Algebra.TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B)
        (HMul.hMul (α := B ⊗[R] A) (β := B ⊗[R] A) (b ⊗ₜ[R] 1)
          ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)) :
      A ⊗[R] B)
    ((AlgEquiv.symm (Algebra.TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B)
        (HMul.hMul (α := B ⊗[R] A) (β := B ⊗[R] A)
          ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A) (b ⊗ₜ[R] 1)) :
      A ⊗[R] B)

Tactic:
aesop
-- 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 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)))
x : A ⊗[R] B
h :
  ∀ a ∈ S,
    HMul.hMul (α := B ⊗[R] A) (β := B ⊗[R] A) (a ⊗ₜ[R] 1)
        ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A) =
      HMul.hMul (α := B ⊗[R] A) (β := B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A) (a ⊗ₜ[R] 1)
b : B
hb : b ∈ S
⊢ Eq (α := B ⊗[R] A) ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (1 ⊗ₜ[R] b * x) : B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x * 1 ⊗ₜ[R] b) : B ⊗[R] A)

Tactic:
aesop
-- 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 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)))
x : A ⊗[R] B
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeRight : (a : B) → A ⊗[R] B) '' S)) x ↔
    Membership.mem (γ := 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)))
      x

Tactic:
simpa [mem_centralizer_iff] using
      ⟨fun h b hb ↦ (Algebra.TensorProduct.comm R A B).symm.injective <| by aesop, fun h b hb ↦
        (Algebra.TensorProduct.comm R A B).injective <| by aesop⟩

Premises used: Subalgebra.mem_centralizer_iff
-- 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 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 :
  ∀ (x : A ⊗[R] B),
    Membership.mem (γ := 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))
        x ↔
      Membership.mem (γ := 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)))
        x
⊢ 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:
ext x