awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b : A
⊢ (((mul R A : (a : A) → A →ₗ[R] A) a : A →ₗ[R] A) : (a : A) → A) b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b : A
⊢ (mul' R A : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] b) = a * b

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Module S A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower S A A
inst_9 : CompatibleSMul A A R S
a : A
h :
  ∀ (x : A),
    Eq (α := A)
      (((↑R :
                {S : Type u_4} →
                  {M M₂ : Type u_2} →
                    [inst : Semiring R] →
                      [inst_10 : Semiring S] →
                        [inst_11 : AddCommMonoid M] →
                          [inst_12 : AddCommMonoid M₂] →
                            [inst_13 : Module R M] →
                              [inst_14 : Module R M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S) ((mul S A : (a : A) → A →ₗ[S] A) a) :
            (a : A) → A)
          x :
        A)
      ((((mul R A : (a : A) → A →ₗ[R] A) a : A →ₗ[R] A) : (a : A) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A →ₗ[R] A)
    ((↑R :
        {S : Type u_4} →
          {M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_10 : Semiring S] →
                [inst_11 : AddCommMonoid M] →
                  [inst_12 : AddCommMonoid M₂] →
                    [inst_13 : Module R M] →
                      [inst_14 : Module R M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) ((mul S A : (a : A) → A →ₗ[S] A) a))
    ((mul R A : (a : A) → A →ₗ[R] A) a)

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Module S A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower S A A
inst_9 : CompatibleSMul A A R S
a x : A
⊢ Eq (α := A)
    (((↑R :
              {S : Type u_4} →
                {M M₂ : Type u_2} →
                  [inst : Semiring R] →
                    [inst_10 : Semiring S] →
                      [inst_11 : AddCommMonoid M] →
                        [inst_12 : AddCommMonoid M₂] →
                          [inst_13 : Module R M] →
                            [inst_14 : Module R M₂] →
                              [inst_15 : Module S M] →
                                [inst_16 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((mul S A : (a : A) → A →ₗ[S] A) a) :
          (a : A) → A)
        x :
      A)
    ((((mul R A : (a : A) → A →ₗ[R] A) a : A →ₗ[R] A) : (a : A) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
H :
  ∀ (x : R) (y : M),
    Eq.{u_4 + 1} (α := M) ((lift (lsmul R M ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) r) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] y) : M)
      (((lsmul R M : (a : R) → M →ₗ[R] M) r ∘ₗ lift (lsmul R M) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] y) : M)
⊢ Eq (α := R ⊗[R] M →ₗ[R] M) (lift (lsmul R M ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) r))
    ((lsmul R M : (a : R) → M →ₗ[R] M) r ∘ₗ lift (lsmul R M))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
r x : R
a : M
⊢ Eq.{u_4 + 1} (α := M) ((lift (lsmul R M ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) r) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] a) : M)
    (((lsmul R M : (a : R) → M →ₗ[R] M) r ∘ₗ lift (lsmul R M) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] a) : M)

Tactic:
simp [← mul_smul, mul_comm]

Premises used: mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
⊢ Eq (α := (a : A) → End R A) (⇑(NonUnitalAlgHom.lmul R A) : (a : A) → End R A) (⇑(mul R A) : (a : A) → A →ₗ[R] A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b : A
h :
  ∀ (c : A),
    Eq (α := A) ((HMul.hMul (α := A →ₗ[R] A) (mulLeft R a) (mulRight R b) : (a : A) → A) c : A)
      ((HMul.hMul (α := A →ₗ[R] A) (mulRight R b) (mulLeft R a) : (a : A) → A) c : A)
⊢ Commute (S := A →ₗ[R] A) (mulLeft R a) (mulRight R b)

Tactic:
ext c
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b c : A
⊢ Eq (α := A) ((HMul.hMul (α := A →ₗ[R] A) (mulLeft R a) (mulRight R b) : (a : A) → A) c : A)
    ((HMul.hMul (α := A →ₗ[R] A) (mulRight R b) (mulLeft R a) : (a : A) → A) c : A)

Tactic:
(mul_assoc a c b).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b c : A
⊢ Eq (α := A) ((HMul.hMul (α := A →ₗ[R] A) (mulLeft R a) (mulRight R b) : (a : A) → A) c : A)
    ((HMul.hMul (α := A →ₗ[R] A) (mulRight R b) (mulLeft R a) : (a : A) → A) c : A)

Tactic:
exact (mul_assoc a c b).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : NonUnitalSemiring B
inst_3 : Module R B
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
f : A →ₗ[R] B
⊢ (∀ (x y : A),
      (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) ↔
    compr₂ (mul R A) f = (mul R B ∘ₗ f).compl₂ f

Tactic:
Iff.symm LinearMap.ext_iff₂

Premises used: LinearMap.ext_iff₂, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulLeft R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulLeft R 1)
rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
rw₃ rw₄ : Eq.{u_2 + 1} (α := A →ₗ[R] A) id id
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulLeft R a) 0 = mulLeft R (HPow.hPow (β := ℕ) a 0)

Tactic:
rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]

Premises used: Module.End.one_eq_id, pow_zero, LinearMap.mulLeft_one
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n * a)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
rw₄ rw₅ : Eq (α := A →ₗ[R] A) (mulLeft R (a ^ n) ∘ₗ mulLeft R a) (mulLeft R (a ^ n) ∘ₗ mulLeft R a)
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]

Premises used: Module.End.mul_eq_comp, pow_succ, LinearMap.mulLeft_mul
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulRight R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulRight R 1)
rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
rw₃ rw₄ : Eq.{u_2 + 1} (α := A →ₗ[R] A) id id
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulRight R a) 0 = mulRight R (HPow.hPow (β := ℕ) a 0)

Tactic:
rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]

Premises used: Module.End.one_eq_id, pow_zero, LinearMap.mulRight_one
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a * a ^ n)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
rw₄ rw₅ : Eq (α := A →ₗ[R] A) (mulRight R (a ^ n) ∘ₗ mulRight R a) (mulRight R (a ^ n) ∘ₗ mulRight R a)
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]

Premises used: Module.End.mul_eq_comp, pow_succ, LinearMap.mulRight_mul, pow_succ'
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : A) → End R A) (⇑(Algebra.lmul R A) : (a : A) → End R A) (⇑(mul R A) : (a : A) → A →ₗ[R] A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
h :
  Eq (α := End R A) ((Algebra.lmul R A : (a : A) → End R A) a₁ : End R A)
    ((Algebra.lmul R A : (a : A) → End R A) a₂ : End R A)
⊢ a₁ = a₂

Tactic:
simpa using DFunLike.congr_fun h 1

Premises used: DFunLike.congr_fun, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw :
  IsUnit x ↔ Function.Bijective (α := A) (β := A) (⇑((Algebra.lmul R A : (a : A) → End R A) x : End R A) : (a : A) → A)
⊢ IsUnit (M := End R A) ((Algebra.lmul R A : (a : A) → End R A) x : End R A) ↔ IsUnit x

Tactic:
rw [Module.End.isUnit_iff, Iff.comm]

Premises used: Module.End.isUnit_iff, Iff.comm
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective (α := A) (β := A) (⇑((Algebra.lmul R A : (a : A) → End R A) x : End R A) : (a : A) → A)

Tactic:
IsUnit.isUnit_iff_mulLeft_bijective

Premises used: IsUnit.isUnit_iff_mulLeft_bijective
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective (α := A) (β := A) (⇑((Algebra.lmul R A : (a : A) → End R A) x : End R A) : (a : A) → A)

Tactic:
exact IsUnit.isUnit_iff_mulLeft_bijective

Premises used: IsUnit.isUnit_iff_mulLeft_bijective
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Eq.{u_2 + 1} (α := A) ((toSpanSingleton R A 1 : (a : R) → A) 1 : A) ((Algebra.linearMap R A : (a : R) → A) 1 : A)
⊢ Eq (α := R →ₗ[R] A) (toSpanSingleton R A 1) (Algebra.linearMap R A)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_2 + 1} (α := A) ((toSpanSingleton R A 1 : (a : R) → A) 1 : A) ((Algebra.linearMap R A : (a : R) → A) 1 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Bilinear
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
a : A
x : A ⊗[R] A
⊢ AddHom.toFun (toAddHom (mul' R A)) (HSMul.hSMul (β := A ⊗[R] A) a 0) =
    HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (AddHom.toFun (M := A ⊗[R] A) (toAddHom (mul' R A)) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Bilinear
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
a : A
x : A ⊗[R] A
⊢ ∀ (x y : A),
    AddHom.toFun (toAddHom (mul' R A)) (HSMul.hSMul (β := A ⊗[R] A) a (x ⊗ₜ[R] y)) =
      HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A)
        (AddHom.toFun (M := A ⊗[R] A) (toAddHom (mul' R A)) (x ⊗ₜ[R] y))

Tactic:
simp +contextual [mul', smul_tmul', mul_assoc]

Premises used: mul_assoc, TensorProduct.smul_tmul', LinearMap.mul'
-- Module: Mathlib.Algebra.Algebra.Bilinear
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
a : A
x : A ⊗[R] A
⊢ ∀ (x y : A ⊗[R] A),
    AddHom.toFun (toAddHom (mul' R A)) (a • x) =
        HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (AddHom.toFun (toAddHom (mul' R A)) x) →
      AddHom.toFun (toAddHom (mul' R A)) (a • y) =
          HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (AddHom.toFun (toAddHom (mul' R A)) y) →
        AddHom.toFun (toAddHom (mul' R A)) (a • (x + y)) =
          HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (AddHom.toFun (toAddHom (mul' R A)) (x + y))

Tactic:
simp +contextual [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
h :
  ∀ (x x_1 : A),
    Eq (α := A) ((((flip (mul R A) : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)
      ((((mul R A : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)
⊢ Eq (α := A →ₗ[R] A →ₗ[R] A) (flip (mul R A)) (mul R A)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
x x_1 : A
⊢ Eq (α := A) ((((flip (mul R A) : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)
    ((((mul R A : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
⊢ Eq (α := A ⊗[R] A →ₗ[R] A) (mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) (mul' R A)

Tactic:
simp [mul', lift_comp_comm_eq]

Premises used: LinearMap.mul', TensorProduct.lift_comp_comm_eq
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
x : A ⊗[R] A
⊢ Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A) ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A) x : A ⊗[R] A) : A)
    ((mul' R A : (a : A ⊗[R] A) → A) x : A)

Tactic:
congr($mul'_comp_comm _)

Premises used: LinearMap.mul'_comp_comm, congrArg, id, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
f : A →ₙₐ[R] B
⊢ ∀ (x y : A),
    Eq.{u_3 + 1} (α := B)
      (((↑f : [inst_9 : FunLike (A →ₙₐ[R] B) A B] → [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
              LinearMap.mul' R A :
            (a : A ⊗[R] A) → B)
          (x ⊗ₜ[R] y) :
        B)
      ((LinearMap.mul' R B ∘ₗ
              ((↑f :
                  [inst_9 : FunLike (A →ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) ⊗ₘ
                (↑f :
                  [inst_9 : FunLike (A →ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
            (a : A ⊗[R] A) → B)
          (x ⊗ₜ[R] y) :
        B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Bilinear
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (x y : A),
    Eq.{u_3 + 1} (α := B) ((f.toLinearMap ∘ₗ LinearMap.mul' R A : (a : A ⊗[R] A) → B) (x ⊗ₜ[R] y) : B)
      ((LinearMap.mul' R B ∘ₗ (f.toLinearMap ⊗ₘ f.toLinearMap) : (a : A ⊗[R] A) → B) (x ⊗ₜ[R] y) : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
α : Type u
⊢ (↑(free.obj α) : Type u) = FreeAbelianGroup α

Tactic:
rfl

Premises used: Additive, FreeAbelianGroup, Abelianization, rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
α β : Type u
f : α ⟶ β
x : FreeAbelianGroup α
⊢ Eq (α := (↑(free.obj β) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            (free.map f) :
          (a : (↑(free.obj α) : Type u)) → (↑(free.obj β) : Type u))
        x :
      (↑(free.obj β) : Type u))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β) <$> x :
      FreeAbelianGroup ((fun (X : Type u) ↦ X) β))

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : Type u
Y : AddCommGrpCat
refine :
  ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) (free.obj X) Y ≃
    (X →
      Functor.obj
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          carrier))
        Y)
⊢ (free.obj X ⟶ Y) ≃
    (X ⟶
      Functor.obj
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          carrier))
        Y)

Tactic:
refine ConcreteCategory.homEquiv.trans (Equiv.trans ?_ TypeCat.homEquiv.symm)

Premises used: Equiv.trans, TypeCat.homEquiv, Equiv.symm, CategoryTheory.ConcreteCategory.homEquiv
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : Type u
Y : AddCommGrpCat
⊢ ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) (free.obj X) Y ≃
    (X →
      Functor.obj
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          carrier))
        Y)

Tactic:
exact FreeAbelianGroup.lift.symm

Premises used: FreeAbelianGroup.lift, Equiv.symm
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
hf :
  ∀ (x : (↑(free.obj X') : Type u)),
    Eq (α := (↑Y : Type u))
      ((Hom.hom
              ((Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X' ⟶ (forget AddCommGrpCat).obj Y) → free.obj X' ⟶ Y)
                (f ≫ g)) :
            (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((Hom.hom
              (free.map f ≫
                (Equiv.symm
                      (Equiv.trans
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                          (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                        (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                    (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
                  g) :
            (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ Eq (α := free.obj X' ⟶ Y)
    ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                (CC := carrier))
              (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget AddCommGrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g) :
      free.obj X' ⟶ Y)
    (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                  (CC := carrier))
                (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
          g :
      free.obj X' ⟶ Y)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
x : (↑(free.obj X') : Type u)
hf :
  Eq (α := (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X')) Y) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X → ToType Y) → ToHom (of (FreeAbelianGroup X)) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X)) Y) :
          (a : FreeAbelianGroup X) → (↑Y : Type u))
        ((FreeAbelianGroup.map (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X) :
              (a : FreeAbelianGroup X') → FreeAbelianGroup X)
            x :
          FreeAbelianGroup X) :
      (↑Y : Type u))
⊢ Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (Equiv.trans
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                    (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                (a : X' ⟶ (forget AddCommGrpCat).obj Y) → free.obj X' ⟶ Y)
              (f ≫ g)) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((Hom.hom
            (free.map f ≫
              (Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
                g) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
dsimp [ConcreteCategory.homEquiv]

Premises used: CategoryTheory.ConcreteCategory.homEquiv