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 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 :
  (∃ (x_1 : 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) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          x_1 =
        x) →
    ∃ (x_1 : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A),
      Eq (α := B ⊗[R] 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) :
              (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
            x_1 :
          B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
h₁ :
  (∃ (x_1 : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A),
      Eq (α := B ⊗[R] 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) :
              (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
            x_1 :
          B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)) →
    ∃ (x_1 : 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) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          x_1 =
        x
⊢ (∃ (x_1 : 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) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          x_1 =
        x) ↔
    ∃ (x_1 : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A),
      Eq (α := B ⊗[R] 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) :
              (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
            x_1 :
          B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)

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 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 : TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S)
rw rw₁ :
  Eq (α := B ⊗[R] 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) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A ↥(centralizer R S) :
            (a : A ⊗[R] ↥(centralizer R S)) → ↥(centralizer R S) ⊗[R] A)
          x) :
      B ⊗[R] 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) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A ↥(centralizer R S) :
            (a : A ⊗[R] ↥(centralizer R S)) → ↥(centralizer R S) ⊗[R] A)
          x) :
      B ⊗[R] A)
⊢ Eq (α := B ⊗[R] 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) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        ((Algebra.TensorProduct.comm R A ↥(centralizer R S) :
            (a : A ⊗[R] ↥(centralizer R S)) → ↥(centralizer R S) ⊗[R] A)
          x) :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A)
        (((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) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          x) :
      B ⊗[R] A)

Tactic:
rw [Algebra.TensorProduct.comm_comp_map_apply]

Premises used: Algebra.TensorProduct.comm_comp_map_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 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 : TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S)
⊢ ∃ (x_1 : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A),
    Eq (α := B ⊗[R] 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) :
            (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
          x_1 :
        B ⊗[R] A)
      ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A)
          (((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) :
              (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
            x) :
        B ⊗[R] A)

Tactic:
exact ⟨(Algebra.TensorProduct.comm R _ _) x,
        by rw [Algebra.TensorProduct.comm_comp_map_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 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
y : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A
hy :
  Eq (α := B ⊗[R] 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) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
⊢ ∃ (x_1 : 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) :
          (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
        x_1 =
      x

Tactic:
⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).injective ?_⟩

Premises used: Algebra.TensorProduct.comm, Exists.intro, AlgEquiv.injective, DFunLike.coe
-- 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
y : TensorProduct.{u_1, u_3, u_2} R (↥(centralizer R S)) A
hy :
  Eq (α := B ⊗[R] 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) :
          (a : ↥(centralizer R S) ⊗[R] A) → B ⊗[R] A)
        y :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
h :
  Eq (α := B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A)
        (((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) :
            (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
          ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A :
              (a : ↥(centralizer R S) ⊗[R] A) → A ⊗[R] ↥(centralizer R S))
            y)) :
      B ⊗[R] A)
    ((Algebra.TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
⊢ ∃ (x_1 : 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) :
          (a : A ⊗[R] ↥(centralizer R S)) → A ⊗[R] B)
        x_1 =
      x

Tactic:
refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).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 : Subalgebra R A
inst_5 : Module.Free R B
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeLeft S) : Set (A ⊗[R] B)) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R (↑S : Set A))) B)
        (Algebra.TensorProduct.map (val (centralizer R (↑S : Set A))) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R (↑S : Set A))) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
centralizer_coe_image_includeLeft_eq_center_tensorProduct R A B S

Premises used: Set.Mem, setOf, SetLike.coe, Set.image, TensorProduct.tmul, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, AddCon.toQuotient
-- 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 : Subalgebra R B
inst_5 : Module.Free R A
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeRight S) : Set (A ⊗[R] B)) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R (↑S : Set B)))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (centralizer R (↑S : Set B))) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R (↑S : Set B)) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
centralizer_coe_image_includeRight_eq_center_tensorProduct R A B S

Premises used: Set.Mem, setOf, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, SetLike.coe, Set.image, TensorProduct.tmul, AddCon.toQuotient
-- 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
inst_5 : Module.Free R B
rw :
  Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(center R A)) B)
        (Algebra.TensorProduct.map (val (center R A)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(center R A)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := A),
    ← centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤]

Premises used: Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, Algebra.coe_top, Subalgebra.centralizer_univ, Top.top
-- 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
inst_5 : Module.Free R B
h :
  ∀ (x : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B))) x ↔
      Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B))) x
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B)))

Tactic:
ext
-- 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
inst_5 : Module.Free R B
x : A ⊗[R] B
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B))) x ↔
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B))) x

Tactic:
simp [includeLeft, includeLeftRingHom]

Premises used: Algebra.TensorProduct.includeLeftRingHom, Algebra.TensorProduct.includeLeft
-- 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
inst_5 : Module.Free R A
rw :
  Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)) : Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(center R B))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (center R B)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(center R B) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B),
    ← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]

Premises used: Algebra.coe_top, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, Subalgebra.centralizer_univ, Top.top
-- 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
inst_5 : Module.Free R A
h :
  ∀ (x : A ⊗[R] B),
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))) x ↔
      Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B))) x
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B)))

Tactic:
ext
-- 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
inst_5 : Module.Free R A
x : A ⊗[R] B
⊢ Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))) x ↔
    Membership.mem (γ := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B))) x

Tactic:
simp [includeRight]

Premises used: Algebra.TensorProduct.includeRight
-- 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
inst_5 : Module.Free R B
rw :
  Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
      (↑(AlgHom.range (A := A ⊗[R] R)
              (Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) :
            Subalgebra R (A ⊗[R] B)) :
        Set (A ⊗[R] B)))
    (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
        (↑(AlgHom.range (A := A ⊗[R] R)
                (Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) :
              Subalgebra R (A ⊗[R] B)) :
          Set (A ⊗[R] B)) :
      Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R (↥(center R A)) B)
        (Algebra.TensorProduct.map (val (center R A)) (AlgHom.id R B) :
          TensorProduct.{u_1, u_2, u_3} R (↥(center R A)) B →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
rw [← centralizer_coe_range_includeLeft_eq_center_tensorProduct]

Premises used: Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct
-- 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
inst_5 : Module.Free R B
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
      (↑(AlgHom.range (A := A ⊗[R] R)
              (Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B) : A ⊗[R] R →ₐ[R] A ⊗[R] B) :
            Subalgebra R (A ⊗[R] B)) :
        Set (A ⊗[R] B)))
    (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))

Tactic:
simp [Algebra.TensorProduct.map_range]

Premises used: Algebra.TensorProduct.map_range
-- 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
inst_5 : Module.Free R A
rw :
  Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
      (↑(AlgHom.range (A := R ⊗[R] B)
              (Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B) : R ⊗[R] B →ₐ[R] A ⊗[R] B) :
            Subalgebra R (A ⊗[R] B)) :
        Set (A ⊗[R] B)))
    (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
        (↑(AlgHom.range (A := R ⊗[R] B)
                (Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B) : R ⊗[R] B →ₐ[R] A ⊗[R] B) :
              Subalgebra R (A ⊗[R] B)) :
          Set (A ⊗[R] B)) :
      Subalgebra R (A ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R A ↥(center R B))
        (Algebra.TensorProduct.map (AlgHom.id R A) (val (center R B)) :
          TensorProduct.{u_1, u_2, u_3} R A ↥(center R B) →ₐ[R] A ⊗[R] B) :
      Subalgebra R (A ⊗[R] B))

Tactic:
rw [← centralizer_range_includeRight_eq_center_tensorProduct]

Premises used: Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct
-- 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
inst_5 : Module.Free R A
⊢ Eq (α := Subalgebra R (A ⊗[R] B))
    (centralizer R
      (↑(AlgHom.range (A := R ⊗[R] B)
              (Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B) : R ⊗[R] B →ₐ[R] A ⊗[R] B) :
            Subalgebra R (A ⊗[R] B)) :
        Set (A ⊗[R] B)))
    (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))

Tactic:
simp [Algebra.TensorProduct.map_range]

Premises used: Algebra.TensorProduct.map_range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Type u_4
inst_3 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
s : Subalgebra R A :=
  let __spread.0 := Subsemiring.copy (⨆ (i : ι), (K i).toSubsemiring) (⋃ (i : ι), (↑(K i).toSubsemiring : Set A)) ⋯;
  { toSubsemiring := __spread.0, algebraMap_mem' := ⋯ }
⊢ iSup K = s

Tactic:
have : iSup K = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Type u_4
inst_3 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
s : Subalgebra R A :=
  let __spread.0 := Subsemiring.copy (⨆ (i : ι), (K i).toSubsemiring) (⋃ (i : ι), (↑(K i).toSubsemiring : Set A)) ⋯;
  { toSubsemiring := __spread.0, algebraMap_mem' := ⋯ }
this : iSup K = s
⊢ (↑(iSup K) : Set A) = ⋃ (i : ι), (↑(K i) : Set A)

Tactic:
simp [this, s]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Type u_4
inst_3 : Nonempty ι
S : ι → Subalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemiring.coe_iSup_of_directed dir] using Subsemiring.isMulCommutative_iSup dir

Premises used: Subalgebra.coe_iSup_of_directed, Subsemiring.coe_iSup_of_directed, Subsemiring.isMulCommutative_iSup, SetLike.mem_coe, isMulCommutative_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
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
S_1 : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
inst_6 : Preorder ι
inst_7 : IsDirectedOrder ι
S : OrderHom.{u_4, u_2} ι (Subalgebra R A)
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥((S : (a : ι) → Subalgebra R A) i : Subalgebra R A)
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), (S : (a : ι) → Subalgebra R A) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Subalgebra.isMulCommutative_iSup, Monotone.directed_le