-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
/--
Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ B`, the centralizer of `1 ⊗ S ⊆ A ⊗ B` is `A ⊗ C_B(S)` where `C_B(S)` is the
centralizer of `S` in `B`.
-/
lemma centralizer_coe_image_includeRight_eq_center_tensorProduct
    (S : Set B) [Module.Free R A] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.includeRight '' S) =
    (Algebra.TensorProduct.map (AlgHom.id R A)
      (Subalgebra.centralizer R (S : Set B)).val).range

Proof state:
case h.e'_3.h.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x) →
    ∃ x_1, (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.e'_3.h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] ↥(centralizer R S)
⊢ ∃ x_1,
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 =
      (Algebra.TensorProduct.comm R A B) ((Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x)

Proof state:
case h.e'_2.h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ x ∈ centralizer R (⇑includeRight '' S) ↔
    x ∈ comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S))

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⟩

Result:
no goals

Proof state:
case h.e'_3.h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x) ↔
    ∃ x_1, (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x

Tactic:
constructor

Result:
case h.e'_3.h.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x) →
    ∃ x_1, (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x

case h.e'_3.h.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1,
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x) →
    ∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x

Proof state:
case h.e'_3.h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ x ∈ (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val).range ↔
    x ∈
      comap (↑(Algebra.TensorProduct.comm R A B))
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range

Tactic:
simp only [AlgHom.mem_range, AlgEquiv.toAlgHom_eq_coe, mem_comap, AlgHom.coe_coe]

Result:
case h.e'_3.h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x) ↔
    ∃ x_1, (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
h : ∀ a ∈ S, a ⊗ₜ[R] 1 * (Algebra.TensorProduct.comm R A B) x = (Algebra.TensorProduct.comm R A B) x * a ⊗ₜ[R] 1
b : B
hb : b ∈ S
⊢ (Algebra.TensorProduct.comm R A B) (1 ⊗ₜ[R] b * x) = (Algebra.TensorProduct.comm R A B) (x * 1 ⊗ₜ[R] b)

Tactic:
aesop

Result:
no goals

Proof state:
case h.e'_3.h.mpr.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ (Algebra.TensorProduct.comm R A B)
      ((Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val)
        ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A) y)) =
    (Algebra.TensorProduct.comm R A B) x

Tactic:
rw [← hy, comm_comp_map_apply, ← comm_symm, AlgEquiv.symm_apply_apply]

Result:
no goals