awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
rw :
  Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
    (⇑(↑(tensorEquivEnd R) : R ⊗[R] Rᵐᵒᵖ →ₐ[R] Module.End R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)
⊢ Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
    (⇑(AlgHom.mulLeftRight R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)

Tactic:
rw [← coe_tensorEquivEnd]

Premises used: IsAzumaya.coe_tensorEquivEnd
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
    (⇑(↑(tensorEquivEnd R) : R ⊗[R] Rᵐᵒᵖ →ₐ[R] Module.End R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)

Tactic:
tensorEquivEnd R |>.bijective

Premises used: IsAzumaya.tensorEquivEnd, AlgEquiv.bijective
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
    (⇑(↑(tensorEquivEnd R) : R ⊗[R] Rᵐᵒᵖ →ₐ[R] Module.End R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)

Tactic:
exact tensorEquivEnd R |>.bijective

Premises used: IsAzumaya.tensorEquivEnd, AlgEquiv.bijective
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
ha :
  ∀ (x : A) (x_1 : B),
    Eq (α := B)
      ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                    (AlgHom.comp (AlgHom.mulLeftRight R B)
                      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ))
                    Algebra.TensorProduct.includeLeft :
                  (a : A) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
      (((((AlgHom.comp
                      (AlgHom.comp
                        (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                        (AlgHom.mulLeftRight R A))
                      Algebra.TensorProduct.includeLeft :
                    AlgHom.{u_1, u_2, u_3} R A (Module.End R B)) :
                  (a : A) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
hb :
  ∀ (x : Aᵐᵒᵖ) (x_1 : B),
    Eq (α := B)
      ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                    (AlgHom.restrictScalars R
                      (AlgHom.comp (AlgHom.mulLeftRight R B)
                        (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                          A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ)))
                    Algebra.TensorProduct.includeRight :
                  (a : Aᵐᵒᵖ) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
      (((((AlgHom.comp
                      (AlgHom.restrictScalars R
                        (AlgHom.comp
                          (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                          (AlgHom.mulLeftRight R A)))
                      Algebra.TensorProduct.includeRight :
                    AlgHom.{u_1, u_2, u_3} R Aᵐᵒᵖ (Module.End R B)) :
                  (a : Aᵐᵒᵖ) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
⊢ AlgHom.comp (AlgHom.mulLeftRight R B)
      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ) =
    AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
      (AlgHom.mulLeftRight R A)

Tactic:
ext
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
x : A
x_1 : B
⊢ Eq (α := B)
    ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                  (AlgHom.comp (AlgHom.mulLeftRight R B)
                    (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                      A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ))
                  Algebra.TensorProduct.includeLeft :
                (a : A) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
    (((((AlgHom.comp
                    (AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                      (AlgHom.mulLeftRight R A))
                    Algebra.TensorProduct.includeLeft :
                  AlgHom.{u_1, u_2, u_3} R A (Module.End R B)) :
                (a : A) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)

Tactic:
simp
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
x : Aᵐᵒᵖ
x_1 : B
⊢ Eq (α := B)
    ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                  (AlgHom.restrictScalars R
                    (AlgHom.comp (AlgHom.mulLeftRight R B)
                      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ)))
                  Algebra.TensorProduct.includeRight :
                (a : Aᵐᵒᵖ) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
    (((((AlgHom.comp
                    (AlgHom.restrictScalars R
                      (AlgHom.comp
                        (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                        (AlgHom.mulLeftRight R A)))
                    Algebra.TensorProduct.includeRight :
                  AlgHom.{u_1, u_2, u_3} R Aᵐᵒᵖ (Module.End R B)) :
                (a : Aᵐᵒᵖ) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)

Tactic:
simp
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
inst_5 : IsAzumaya R A
h : Module.Projective R B := ⋯
h_1 : FaithfulSMul R B := ⋯
h_2 : Module.Finite R B := ⋯
rw :
  Function.Bijective.{u_2 + 1, u_3 + 1} (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R B)
    (⇑(AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
          (AlgHom.mulLeftRight R A)) :
      (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R B)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R B)
    (Function.comp (β := B ⊗[R] Bᵐᵒᵖ) (⇑(AlgHom.mulLeftRight R B) : (a : B ⊗[R] Bᵐᵒᵖ) → Module.End R B)
      (⇑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e) :
            AlgEquiv.{u_1, u_2, u_3} R (A ⊗[R] Aᵐᵒᵖ) (B ⊗[R] Bᵐᵒᵖ)) :
        (a : A ⊗[R] Aᵐᵒᵖ) → B ⊗[R] Bᵐᵒᵖ))

Tactic:
rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]

Premises used: IsAzumaya.mulLeftRight_comp_congr, AlgHom.coe_comp, AlgEquiv.coe_algHom
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
inst_5 : IsAzumaya R A
h : Module.Projective R B := ⋯
h_1 : FaithfulSMul R B := ⋯
h_2 : Module.Finite R B := ⋯
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R B)
    (⇑(AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
          (AlgHom.mulLeftRight R A)) :
      (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R B)

Tactic:
simp [AlgHom.mulLeftRight_bij]

Premises used: IsAzumaya.AlgHom.mulLeftRight_bij
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : IsAzumaya R A
⊢ IsCentral R A

Tactic:
have := of_algEquiv R _ _ (AlgEquiv.ofBijective (.mulLeftRight R A) IsAzumaya.bij).symm
  left_of_tensor R A Aᵐᵒᵖ <| FaithfulSMul.algebraMap_injective _ _

Premises used: AlgEquiv.symm, Algebra.IsCentral.of_algEquiv, AlgEquiv.ofBijective, MulOpposite, IsAzumaya.bij, FaithfulSMul.algebraMap_injective, AlgHom.mulLeftRight, TensorProduct, Module.End, Algebra.IsCentral.left_of_tensor
-- Module: Mathlib.Algebra.Azumaya.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
change :
  (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (r • ab) : A →ₗ[R] A) : (a : A) → A) a =
    HSMul.hSMul (β := A) r ((((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) ab : A →ₗ[R] A) : (a : A) → A) a : A)
⊢ (r • ab) • a = r • ab • a

Tactic:
change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _

Premises used: TensorProduct.Algebra.moduleAux, DFunLike.coe
-- Module: Mathlib.Algebra.Azumaya.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (r • ab) : A →ₗ[R] A) : (a : A) → A) a =
    HSMul.hSMul (β := A) r ((((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) ab : A →ₗ[R] A) : (a : A) → A) a : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Azumaya.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
simp : HSMul.hSMul (α := A ⊗[R] Aᵐᵒᵖ) (a ⊗ₜ[R] b) x = a * x * MulOpposite.unop b
⊢ (((mulLeftRight R A : (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R A) (a ⊗ₜ[R] b) : Module.End R A) : (a : A) → A) x =
    a * x * MulOpposite.unop b

Tactic:
simp only [AlgHom.mulLeftRight, Algebra.lsmul_coe]

Premises used: AlgHom.mulLeftRight, Algebra.lsmul_coe
-- Module: Mathlib.Algebra.Azumaya.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
change :
  (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (a ⊗ₜ[R] b) : A →ₗ[R] A) : (a : A) → A) x =
    a * x * MulOpposite.unop b
⊢ HSMul.hSMul (α := A ⊗[R] Aᵐᵒᵖ) (a ⊗ₜ[R] b) x = a * x * MulOpposite.unop b

Tactic:
change TensorProduct.Algebra.moduleAux _ _ = _

Premises used: TensorProduct.Algebra.moduleAux, DFunLike.coe
-- Module: Mathlib.Algebra.Azumaya.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (a ⊗ₜ[R] b) : A →ₗ[R] A) : (a : A) → A) x =
    a * x * MulOpposite.unop b

Tactic:
simp [TensorProduct.Algebra.moduleAux, ← mul_assoc]

Premises used: mul_assoc, TensorProduct.Algebra.moduleAux
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f1 f2 : Module.End R (Matrix n n R)
⊢ (∑ x : (n × n) × n × n,
      match (motive := (n × n) × n × n → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) x with
      | ((i, j), k, l) =>
        HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
          ((f1 + f2 : (a : Matrix n n R) → Matrix n n R) (single j k 1) i l : R)
          (single i j 1 ⊗ₜ[R] op (single k l 1))) =
    HAdd.hAdd (α := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
      (∑ x : (n × n) × n × n,
        match (motive := (n × n) × n × n → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) x with
        | ((i, j), k, l) =>
          HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
            ((f1 : (a : Matrix n n R) → Matrix n n R) (single j k 1) i l : R) (single i j 1 ⊗ₜ[R] op (single k l 1)))
      (∑ x : (n × n) × n × n,
        match (motive := (n × n) × n × n → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) x with
        | ((i, j), k, l) =>
          HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
            ((f2 : (a : Matrix n n R) → Matrix n n R) (single j k 1) i l : R) (single i j 1 ⊗ₜ[R] op (single k l 1)))

Tactic:
simp [add_smul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
r : R
f : Module.End R (Matrix n n R)
⊢ (∑ x : (n × n) × n × n,
      match (motive := (n × n) × n × n → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) x with
      | ((i, j), k, l) =>
        HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
          ((r • f : (a : Matrix n n R) → Matrix n n R) (single j k 1) i l : R) (single i j 1 ⊗ₜ[R] op (single k l 1))) =
    HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) ((RingHom.id R : (a : R) → R) r : R)
      (∑ x : (n × n) × n × n,
        match (motive := (n × n) × n × n → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) x with
        | ((i, j), k, l) =>
          HSMul.hSMul (α := R) (β := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
            ((f : (a : Matrix n n R) → Matrix n n R) (single j k 1) i l : R) (single i j 1 ⊗ₜ[R] op (single k l 1)))

Tactic:
simp [mul_smul, Finset.smul_sum]

Premises used: Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
x : (n × n) × n × n
i0 j0 k0 l0 : n
⊢ Eq (α := Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
    ((mulLeftRightMatrix_inv R n ∘ₗ toLinearMap (mulLeftRight R (Matrix n n R)) :
          (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
        (((Module.Basis.tensorProduct (stdBasis R n n) (Module.Basis.map (stdBasis R n n) (opLinearEquiv R)) :
              Module.Basis ((n × n) × n × n) R (Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)) :
            (a : (n × n) × n × n) → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
          ((i0, j0), k0, l0)) :
      Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
    ((LinearMap.id : (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
        (((Module.Basis.tensorProduct (stdBasis R n n) (Module.Basis.map (stdBasis R n n) (opLinearEquiv R)) :
              Module.Basis ((n × n) × n × n) R (Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)) :
            (a : (n × n) × n × n) → Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)
          ((i0, j0), k0, l0)) :
      Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ)

Tactic:
simp [stdBasis_eq_single, ite_and, Fintype.sum_prod_type,
      mulLeftRight_apply, single, Matrix.mul_apply]

Premises used: Matrix.mul_apply, AlgHom.mulLeftRight_apply, Matrix.stdBasis_eq_single, ite_and, Fintype.sum_prod_type, Matrix.single
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
h :
  ∀ (f : Module.End R (Matrix n n R)),
    Eq (α := Module.End R (Matrix n n R))
      ((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
            (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
          f :
        Module.End R (Matrix n n R))
      ((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f : Module.End R (Matrix n n R))
⊢ Eq (α := Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))
    (toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
      Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))
    (LinearMap.id : Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))

Tactic:
ext f : 1
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
h :
  ∀ (i : n × n),
    Eq (α := Matrix n n R)
      ((((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
                  (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
                f :
              Module.End R (Matrix n n R)) :
            (a : Matrix n n R) → Matrix n n R)
          ((stdBasis R n n : (a : n × n) → Matrix n n R) i) :
        Matrix n n R)
      ((((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f :
              Module.End R (Matrix n n R)) :
            (a : Matrix n n R) → Matrix n n R)
          ((stdBasis R n n : (a : n × n) → Matrix n n R) i) :
        Matrix n n R)
⊢ Eq (α := Module.End R (Matrix n n R))
    ((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
          (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
        f :
      Module.End R (Matrix n n R))
    ((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f : Module.End R (Matrix n n R))

Tactic:
apply (Matrix.stdBasis _ _ _).ext

Premises used: Matrix.stdBasis, Module.Basis.ext
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
h :
  Eq (α := Matrix n n R)
    (∑ x : (n × n) × n × n,
        HSMul.hSMul (α := R) (β := Matrix n n R)
          ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
          ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                      (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                    (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                  Module.End R (Matrix n n R)) :
                (a : Matrix n n R) → Matrix n n R)
              (single i j 1) :
            Matrix n n R) :
      Matrix n n R)
    ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) : Matrix n n R)
⊢ Eq (α := Matrix n n R)
    ((((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
                (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
              f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) (i, j)) :
      Matrix n n R)
    ((((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) (i, j)) :
      Matrix n n R)

Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
    map_smul, stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply,
    LinearMap.smul_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.coe_mk, LinearMap.smul_apply, LinearMap.id_coe, Finset.sum_apply, LinearMap.coe_sum, map_sum, Matrix.stdBasis_eq_single, LinearMap.coe_comp, Function.comp_apply, AddHom.coe_mk, map_smul, id_eq
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
h :
  ∀ (k l : n),
    Eq.{u_1 + 1} (α := R)
      ((∑ x : (n × n) × n × n,
            HSMul.hSMul (α := R) (β := Matrix n n R)
              ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
              ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                          (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                        (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                      Module.End R (Matrix n n R)) :
                    (a : Matrix n n R) → Matrix n n R)
                  (single i j 1) :
                Matrix n n R))
          k l :
        R)
      ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) k l : R)
⊢ Eq (α := Matrix n n R)
    (∑ x : (n × n) × n × n,
        HSMul.hSMul (α := R) (β := Matrix n n R)
          ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
          ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                      (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                    (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                  Module.End R (Matrix n n R)) :
                (a : Matrix n n R) → Matrix n n R)
              (single i j 1) :
            Matrix n n R) :
      Matrix n n R)
    ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) : Matrix n n R)

Tactic:
ext k l
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
i j k l : n
⊢ Eq.{u_1 + 1} (α := R)
    ((∑ x : (n × n) × n × n,
          HSMul.hSMul (α := R) (β := Matrix n n R)
            ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
            ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                        (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                      (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                    Module.End R (Matrix n n R)) :
                  (a : Matrix n n R) → Matrix n n R)
                (single i j 1) :
              Matrix n n R))
        k l :
      R)
    ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) k l : R)

Tactic:
simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]

Premises used: Matrix.sum_apply, Matrix.mul_apply, ite_and, Fintype.sum_prod_type, Matrix.single
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
h : Nontrivial R
m₁ m₂ : R
⊢ (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
eq_of_smul_eq_smul

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.Algebra.Azumaya.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
h : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
exact eq_of_smul_eq_smul

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod

Tactic:
simpa using h
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s : Multiset ι
f : ι → M₀
h : p ∣ (Multiset.map f s).prod
⊢ ∃ a ∈ s, p ∣ f a

Tactic:
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
    hp.exists_mem_multiset_dvd h

Premises used: Multiset.mem_map, Prime.exists_mem_multiset_dvd, exists_prop, exists_exists_and_eq_and
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s : Finset ι
f : ι → M₀
⊢ p ∣ s.prod f → ∃ i ∈ s, p ∣ f i

Tactic:
hp.exists_mem_multiset_map_dvd

Premises used: Prime.exists_mem_multiset_map_dvd, Set.Mem, setOf, Finset.prod, Multiset.Mem