awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    (comap (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
      (centralizer R ((⇑includeLeft : (a : B) → B ⊗[R] A) '' S)))
have 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
Tactic: ext x
-- 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))
    (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))
have 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
Tactic: ext x
-- 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)))
x : A ⊗[R] B
⊢ (∃ (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)
have 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)
Tactic: constructor
-- 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)))
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)
⊢ (∃ (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)
have 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
Tactic: constructor
-- 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)))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(centralizer R S)
⊢ 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)
have 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)
Tactic: rw [Algebra.TensorProduct.comm_comp_map_apply]
-- 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)))
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
have 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)
Tactic: refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).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 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)
⊢ 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)
have 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.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)
Tactic: rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]
-- 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
inst_5 : Module.Free 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))
have rw : Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))
  (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B)))
Tactic: rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := A),
    ← centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤]
-- 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
inst_5 : Module.Free R B
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeLeft) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeLeft ⊤) : Set (A ⊗[R] B)))
have 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
Tactic: ext
-- 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
inst_5 : Module.Free R A
⊢ 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))
have rw : Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))
  (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B)))
Tactic: rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B),
    ← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]
-- 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
inst_5 : Module.Free R A
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (centralizer R (↑(AlgHom.range includeRight) : Set (A ⊗[R] B)))
    (centralizer R (↑(map includeRight ⊤) : Set (A ⊗[R] B)))
have 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
Tactic: ext
-- 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
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)) :
      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))
have 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)))
Tactic: rw [← centralizer_coe_range_includeLeft_eq_center_tensorProduct]
-- 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
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)) :
      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))
have 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)))
Tactic: rw [← centralizer_range_includeRight_eq_center_tensorProduct]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (hypothesis)
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) : Set A) = ⋃ (i : ι), (↑(K i) : Set A)
have this : 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 _)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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 : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ (↑(K i) : Set A)
hxj : x ∈ (↑(K j) : Set A)
⊢ Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B)
have rcases : ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B)
Tactic: rcases dir i j with ⟨k, hik, hjk⟩