-- Mathlib/Algebra/Azumaya/Basic.lean
/--
The following diagram commutes:
```
          e ⊗ eᵒᵖ
A ⊗ Aᵐᵒᵖ  ------------> B ⊗ Bᵐᵒᵖ
  |                        |
  |                        |
  | mulLeftRight R A       | mulLeftRight R B
  |                        |
  V                        V
End R A   ------------> End R B
          e.conj
```
-/
lemma mulLeftRight_comp_congr (e : A ≃ₐ[R] B) :
    (AlgHom.mulLeftRight R B).comp (Algebra.TensorProduct.congr e e.op).toAlgHom =
    (e.toLinearEquiv.algConj).toAlgHom.comp (AlgHom.mulLeftRight R A)

Proof state:
case H.tmul.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
a : A
a' : Aᵐᵒᵖ
x✝ : B
⊢ (((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) (a ⊗ₜ[R] a')) x✝ =
    (((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) (a ⊗ₜ[R] a')) x✝

Tactic:
simp [AlgHom.mulLeftRight_apply, LinearEquiv.algConj, LinearEquiv.conj]

Result:
no goals

Proof state:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
a : A ⊗[R] Aᵐᵒᵖ
⊢ ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) a =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) a

Tactic:
induction a using TensorProduct.induction_on with
| zero => simp
| tmul a a' =>
  ext; simp [AlgHom.mulLeftRight_apply, LinearEquiv.algConj, LinearEquiv.conj]
| add _ _ _ _ => simp_all [map_add]

Result:
no goals

Proof state:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ ∀ (x : A ⊗[R] Aᵐᵒᵖ),
    ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) x =
      ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) x

Tactic:
intro a

Result:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
a : A ⊗[R] Aᵐᵒᵖ
⊢ ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) a =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) a

Proof state:
case H.add
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
x✝ y✝ : A ⊗[R] Aᵐᵒᵖ
a✝¹ :
  ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) x✝ =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) x✝
a✝ :
  ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) y✝ =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) y✝
⊢ ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) (x✝ + y✝) =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) (x✝ + y✝)

Tactic:
simp_all [map_add]

Result:
no goals

Proof state:
case H.zero
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) 0 =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) =
    (↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)

Tactic:
apply AlgHom.ext

Result:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ ∀ (x : A ⊗[R] Aᵐᵒᵖ),
    ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) x =
      ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) x

Proof state:
case H.tmul
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
a : A
a' : Aᵐᵒᵖ
⊢ ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) (a ⊗ₜ[R] a') =
    ((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) (a ⊗ₜ[R] a')

Tactic:
ext

Result:
case H.tmul.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
a : A
a' : Aᵐᵒᵖ
x✝ : B
⊢ (((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))) (a ⊗ₜ[R] a')) x✝ =
    (((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A)) (a ⊗ₜ[R] a')) x✝