awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 1

Tactic:
simp only [Set.mem_setOf_eq, map_one]

Premises used: Set.mem_setOf_eq, map_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₄ rw₅ :
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x + y)

Tactic:
rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]

Premises used: map_add, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 0

Tactic:
simp only [Set.mem_setOf_eq, map_zero]

Premises used: map_zero, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x : R
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A)
    {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    ((algebraMap R A : (a : R) → A) x : A)

Tactic:
simp only [Set.mem_setOf_eq, AlgHomClass.commutes]

Premises used: Set.mem_setOf_eq, AlgHomClass.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
x : A
⊢ Membership.mem (γ := Subalgebra R A) (equalizer φ ψ) x ↔
    Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
⊢ Eq (α := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (equalizer φ ψ) : Submodule R A)
    (LinearMap.eqLocus.{u_1, u_1, u_2, u_3, u_4} (R₂ := R) (M₂ := B) (τ₁₂ := RingHom.id R) φ ψ : Submodule R A)

Tactic:
rfl

Premises used: setOf, LinearMap.eqLocus, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
φ ψ : F
S : Subalgebra R A
⊢ S ≤ equalizer φ ψ ↔ Set.EqOn.{u_2, u_3} (β := B) (⇑φ : (a : A) → B) (⇑ψ : (a : A) → B) (↑S : Set A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.EqOn
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : Subalgebra R A
⊢ comap f (map f S) = S

Tactic:
SetLike.coe_injective (Set.preimage_image_eq _ hf)

Premises used: SetLike.coe_injective, Set.preimage_image_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
mk :
  ∀ (toSubsemiring : Subsemiring A)
    (algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)),
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' :
              Subalgebra R A }.toNonUnitalSubalgebra.toSubalgebra
        ⋯ =
      { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' }
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
⊢ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' :
            Subalgebra R A }.toNonUnitalSubalgebra.toSubalgebra
      ⋯ =
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' }

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
mk :
  ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring A)
    (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier)
    (h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }),
    ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }.toSubalgebra
          h1).toNonUnitalSubalgebra =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' }
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
toNonUnitalSubsemiring : NonUnitalSubsemiring A
smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' : NonUnitalSubalgebra R A }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' }

Tactic:
rfl
-- 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
S T : Subalgebra R A
⊢ S ≤ centralizer R (↑T : Set A) ↔ T ≤ centralizer R (↑S : Set A)

Tactic:
⟨fun h t ht _ hs ↦ (h hs t ht).symm, fun h s hs _ ht ↦ (h ht s hs).symm⟩

Premises used: Iff.intro, Eq.symm
-- 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
S T K : Subalgebra R A
simp_rw : S ⊔ T ≤ centralizer R (↑K : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
simp_rw₁ :
  S ≤ centralizer R (↑K : Set A) ∧ T ≤ centralizer R (↑K : Set A) ↔
    K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)
simp_rw₂ :
  S ≤ centralizer R (↑K : Set A) ∧ T ≤ centralizer R (↑K : Set A) ↔
    K ≤ centralizer R (↑S : Set A) ∧ K ≤ centralizer R (↑T : Set A)
⊢ K ≤ centralizer R (↑(S ⊔ T) : Set A) ↔ K ≤ centralizer R (↑S : Set A) ⊓ centralizer R (↑T : Set A)

Tactic:
simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]

Premises used: Subalgebra.le_centralizer_iff, le_inf_iff, sup_le_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
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
simp_rw :
  LE.le (α := Subalgebra R A) (⨆ (i : ι), S i) (centralizer R (↑K : Set A)) ↔
    K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
simp_rw₁ : (∀ (i : ι), S i ≤ centralizer R (↑K : Set A)) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)
simp_rw₂ : (∀ (i : ι), S i ≤ centralizer R (↑K : Set A)) ↔ ∀ (i : ι), K ≤ centralizer R (↑(S i) : Set A)
⊢ K ≤ centralizer R (↑(⨆ (i : ι), S i) : Set A) ↔ K ≤ ⨅ (i : ι), centralizer R (↑(S i) : Set A)

Tactic:
simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]

Premises used: Subalgebra.le_centralizer_iff, le_iInf_iff, iSup_le_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 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))

Tactic:
ext w
-- 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
w : A ⊗[R] B
h :
  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₁ :
  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
⊢ 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:
constructor
-- 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
w : A ⊗[R] B
hw : Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S)) w
⊢ ∀ (g : A ⊗[R] B), Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g → g * w = w * g

Tactic:
rw [mem_centralizer_iff] at hw

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 A
inst_5 : Module.Free R B
w : A ⊗[R] B
hw : ∀ (g : A ⊗[R] B), Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' S) g → g * w = w * g
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
h :
  ∀ (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),
    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))
      (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
        m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)
⊢ 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:
obtain ⟨b, rfl⟩ := TensorProduct.eq_repr_basis_right ℬ w

Premises used: rfl, TensorProduct.eq_repr_basis_right
-- 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
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
⊢ Eq (α := 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)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (centralizer R S) x)
            ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j) ⋯ ⊗ₜ[R]
          (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) j) :
      A ⊗[R] B)
    ((fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
          (m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i : A ⊗[R] B))
        j ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j) :
      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
ℬ : 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
h :
  ∀ (j : Module.Free.ChooseBasisIndex R B) (hj : j ∈ b.support),
    Membership.mem (α := A) (γ := Subalgebra R A) (centralizer R S)
      ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A)
⊢ 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))
    (b.sum fun (i : Module.Free.ChooseBasisIndex R B) (m : A) ↦
      m ⊗ₜ[R] (ℬ : (a : Module.Free.ChooseBasisIndex R B) → B) i)

Tactic:
refine Subalgebra.sum_mem _ fun j hj => ⟨⟨b j, ?_⟩ ⊗ₜ[R] ℬ j, by 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
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
⊢ Eq.{u_2 + 1} (α := A) ((fun (x_1 : A) ↦ x_1 * x) 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
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
h : x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b
⊢ HMul.hMul (β := A) x ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A) =
    HMul.hMul (α := A) ((b : (a : Module.Free.ChooseBasisIndex R B) → A) j : A) x

Tactic:
suffices x • b = b.mapRange (· * x) (by simp) from Finsupp.ext_iff.1 this j
-- 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
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
⊢ 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⟩

Premises used: And.intro, Exists.intro, TensorProduct.tmul, OfNat.ofNat, rfl
-- 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 :
  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)
⊢ 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

Premises used: Finset.mul_sum, Finsupp.sum, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, Finset.sum_mul
-- 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)
⊢ x • b = mapRange (fun (x_1 : A) ↦ x_1 * x) ⋯ b

Tactic:
TensorProduct.sum_tmul_basis_right_injective ℬ ?_

Premises used: TensorProduct.sum_tmul_basis_right_injective