awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B_1 : ι → Type u_5
inst_7 : (i : ι) → Semiring (B_1 i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B_1 i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
B : Type u_6
C : Type u_7
inst_11 : Semiring B
inst_12 : Semiring C
inst_13 : Algebra R B
inst_14 : Algebra R C
⊢ Eq (α := A ⊗[R] B × A ⊗[R] C)
    (((_root_.TensorProduct.prodRight R S A B C : A ⊗[R] (B × C) ≃ₗ[S] A ⊗[R] B × A ⊗[R] C) :
        (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
      1)
    1

Tactic:
simp [Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B_1 : ι → Type u_5
inst_7 : (i : ι) → Semiring (B_1 i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B_1 i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
B : Type u_6
C : Type u_7
inst_11 : Semiring B
inst_12 : Semiring C
inst_13 : Algebra R B
inst_14 : Algebra R C
x x_1 : A
x_2 x_3 : B × C
⊢ (((↑(_root_.TensorProduct.prodRight R S A B C) : A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
          A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
        (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
      ((x * x_1) ⊗ₜ[R] (x_2 * x_3)) =
    HMul.hMul (α := A ⊗[R] B × A ⊗[R] C) (β := A ⊗[R] B × A ⊗[R] C)
      ((((↑(_root_.TensorProduct.prodRight R S A B C) : A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
              A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
            (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
          (x ⊗ₜ[R] x_2) :
        A ⊗[R] B × A ⊗[R] C)
      ((((↑(_root_.TensorProduct.prodRight R S A B C) : A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
              A ⊗[R] (B × C) →ₗ[S] A ⊗[R] B × A ⊗[R] C) :
            (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
          (x_1 ⊗ₜ[R] x_3) :
        A ⊗[R] B × A ⊗[R] C)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst_7 : Semiring B
inst_8 : Semiring C
inst_9 : Algebra R B
inst_10 : Algebra R C
a : A
x : B × C
⊢ Eq (α := A ⊗[R] B × A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (a ⊗ₜ[R] x) :
      A ⊗[R] B × A ⊗[R] C)
    ((a ⊗ₜ[R] x.1, a ⊗ₜ[R] x.2) : A ⊗[R] B × A ⊗[R] C)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Function.prod, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst_7 : Semiring B
inst_8 : Semiring C
inst_9 : Algebra R B
inst_10 : Algebra R C
a : A
x : B × C
⊢ Eq (α := A ⊗[R] B)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (a ⊗ₜ[R] x)).1
    (a ⊗ₜ[R] x.1)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst_7 : Semiring B
inst_8 : Semiring C
inst_9 : Algebra R B
inst_10 : Algebra R C
a : A
x : B × C
⊢ Eq (α := A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (a ⊗ₜ[R] x)).2
    (a ⊗ₜ[R] x.2)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst_7 : Semiring B
inst_8 : Semiring C
inst_9 : Algebra R B
inst_10 : Algebra R C
a : A
b : B
c : C
a₁ :
  Eq (α := A ⊗[R] B × A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (((AlgEquiv.symm (prodRight R S A B C) : (A ⊗[R] B × A ⊗[R] C) ≃ₐ[S] A ⊗[R] (B × C)) :
            (a : A ⊗[R] B × A ⊗[R] C) → A ⊗[R] (B × C))
          (a ⊗ₜ[R] b, a ⊗ₜ[R] c)) :
      A ⊗[R] B × A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (a ⊗ₜ[R] (b, c)) :
      A ⊗[R] B × A ⊗[R] C)
⊢ Eq (α := A ⊗[R] (B × C))
    (((AlgEquiv.symm (prodRight R S A B C) : (A ⊗[R] B × A ⊗[R] C) ≃ₐ[S] A ⊗[R] (B × C)) :
          (a : A ⊗[R] B × A ⊗[R] C) → A ⊗[R] (B × C))
        (a ⊗ₜ[R] b, a ⊗ₜ[R] c) :
      A ⊗[R] (B × C))
    (a ⊗ₜ[R] (b, c) : A ⊗[R] (B × C))

Tactic:
apply (prodRight R S A B C).injective

Premises used: Algebra.TensorProduct.prodRight, AlgEquiv.injective
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst_7 : Semiring B
inst_8 : Semiring C
inst_9 : Algebra R B
inst_10 : Algebra R C
a : A
b : B
c : C
⊢ Eq (α := A ⊗[R] B × A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (((AlgEquiv.symm (prodRight R S A B C) : (A ⊗[R] B × A ⊗[R] C) ≃ₐ[S] A ⊗[R] (B × C)) :
            (a : A ⊗[R] B × A ⊗[R] C) → A ⊗[R] (B × C))
          (a ⊗ₜ[R] b, a ⊗ₜ[R] c)) :
      A ⊗[R] B × A ⊗[R] C)
    (((prodRight R S A B C : A ⊗[R] (B × C) ≃ₐ[S] A ⊗[R] B × A ⊗[R] C) : (a : A ⊗[R] (B × C)) → A ⊗[R] B × A ⊗[R] C)
        (a ⊗ₜ[R] (b, c)) :
      A ⊗[R] B × A ⊗[R] C)

Tactic:
simp [prodRight_tmul]

Premises used: Algebra.TensorProduct.prodRight_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
c : B
x : HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)
obtain :
  ∀ (u : B),
    ((↑(LinearEquiv.symm
                (tensorQuotEquivQuotSMul B I ≪≫ₗ
                    (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                      (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                  Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
            B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
          (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
        (HSMul.hSMul (β := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) c
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u :
            HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))) =
      HSMul.hSMul (β := B ⊗[A] (A ⧸ I)) c
        (((↑(LinearEquiv.symm
                    (tensorQuotEquivQuotSMul B I ≪≫ₗ
                        (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                          (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                      Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
                B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
              (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
            ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u) :
          B ⊗[A] (A ⧸ I))
⊢ ((↑(LinearEquiv.symm
              (tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
          B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
        (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
      (c • x) =
    HSMul.hSMul (β := B ⊗[A] (A ⧸ I)) c
      (((↑(LinearEquiv.symm
                  (tensorQuotEquivQuotSMul B I ≪≫ₗ
                      (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                        (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                    Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
              B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
            (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          x :
        B ⊗[A] (A ⧸ I))

Tactic:
obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
c u : B
⊢ ((↑(LinearEquiv.symm
              (tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
          B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
        (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
      (HSMul.hSMul (β := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) c
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))) =
    HSMul.hSMul (β := B ⊗[A] (A ⧸ I)) c
      (((↑(LinearEquiv.symm
                  (tensorQuotEquivQuotSMul B I ≪≫ₗ
                      (HSMul.hSMul (β := Submodule A B) I ⊤).quotEquivOfEq
                        (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) I)) ⋯ ≪≫ₗ
                    Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (F := A →+* B) (algebraMap A B) I))) :
              B ⧸ Ideal.map (algebraMap A B) I ≃+ B ⊗[A] (A ⧸ I)) :
            (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u) :
        B ⊗[A] (A ⧸ I))

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
b : B
⊢ Eq (α := B ⊗[A] (A ⧸ I))
    ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
          b) :
      B ⊗[A] (A ⧸ I))
    (b ⊗ₜ[A] 1 : B ⊗[A] (A ⧸ I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
x y : HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)
obtain :
  ∀ (u : B),
    (quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
        (HMul.hMul (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u :
            HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
          y) =
      HMul.hMul (α := B ⊗[A] (A ⧸ I)) (β := B ⊗[A] (A ⧸ I))
        ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
            ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u) :
          B ⊗[A] (A ⧸ I))
        ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I)) y :
          B ⊗[A] (A ⧸ I))
⊢ (quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I)) (x * y) =
    HMul.hMul (α := B ⊗[A] (A ⧸ I)) (β := B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I)) x :
        B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I)) y :
        B ⊗[A] (A ⧸ I))

Tactic:
obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
y : HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)
u : B
obtain :
  ∀ (v : B),
    (quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
        (HMul.hMul (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) (β :=
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u :
            HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              v :
            HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))) =
      HMul.hMul (α := B ⊗[A] (A ⧸ I)) (β := B ⊗[A] (A ⧸ I))
        ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
            ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              u) :
          B ⊗[A] (A ⧸ I))
        ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
            ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
                (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
              v) :
          B ⊗[A] (A ⧸ I))
⊢ (quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
      (HMul.hMul (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
        y) =
    HMul.hMul (α := B ⊗[A] (A ⧸ I)) (β := B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u) :
        B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I)) y :
        B ⊗[A] (A ⧸ I))

Tactic:
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
u v : B
simp_rw : (u * v) ⊗ₜ[A] 1 = HMul.hMul (α := B ⊗[A] (A ⧸ I)) (u ⊗ₜ[A] 1) (v ⊗ₜ[A] 1)
⊢ (quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
      (HMul.hMul (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) (β :=
        HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            v :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))) =
    HMul.hMul (α := B ⊗[A] (A ⧸ I)) (β := B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            u) :
        B ⊗[A] (A ⧸ I))
      ((quotIdealMapEquivTensorQuotAux B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            v) :
        B ⊗[A] (A ⧸ I))

Tactic:
simp_rw [← map_mul, quotIdealMapEquivTensorQuotAux_mk]

Premises used: map_mul, _private.0.Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux_mk
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
u v : B
⊢ (u * v) ⊗ₜ[A] 1 = HMul.hMul (α := B ⊗[A] (A ⧸ I)) (u ⊗ₜ[A] 1) (v ⊗ₜ[A] 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
b : B
⊢ Eq (α := B ⊗[A] (A ⧸ I))
    ((quotIdealMapEquivTensorQuot B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
          b) :
      B ⊗[A] (A ⧸ I))
    (b ⊗ₜ[A] 1 : B ⊗[A] (A ⧸ I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
b : B
a : A
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
    ((AlgEquiv.symm (quotIdealMapEquivTensorQuot B I) : (a : B ⊗[A] (A ⧸ I)) → B ⧸ Ideal.map (algebraMap A B) I)
        (b ⊗ₜ[A] (Ideal.Quotient.mk I : (a : A) → A ⧸ I) a) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I))
    (Submodule.Quotient.mk (a • b) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.map (F := A →+* B) (algebraMap A B) I))

Tactic:
rfl

Premises used: iInf, Quotient.liftOn', Set.Mem, AddCon.liftOn, Set.iInter, Submodule.Quotient.mk, Submodule.restrictScalars, setOf, Ideal.map, List.foldl, Quot.map, Submodule.span, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
x : A
this :
  Eq (α := (A ⧸ I) ⊗[A] B)
    ((TensorProduct.comm A B (A ⧸ I) : (a : B ⊗[A] (A ⧸ I)) → (A ⧸ I) ⊗[A] B)
        ((quotIdealMapEquivTensorQuot B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            ((algebraMap A B : (a : A) → B) x))) :
      (A ⧸ I) ⊗[A] B)
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x : (A ⧸ I) ⊗[A] B)
⊢ Eq (α := (A ⧸ I) ⊗[A] B)
    (Equiv.toFun
      (RingEquiv.toEquiv
        (RingEquiv.trans (AlgEquiv.toRingEquiv (quotIdealMapEquivTensorQuot B I))
          (AlgEquiv.toRingEquiv (TensorProduct.comm A B (A ⧸ I)))))
      ((algebraMap A (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) :
          (a : A) → B ⧸ Ideal.map (algebraMap A B) I)
        x))
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x)

Tactic:
simpa
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
x : A
suffices :
  Eq (α := (A ⧸ I) ⊗[A] B)
    ((TensorProduct.comm A B (A ⧸ I) : (a : B ⊗[A] (A ⧸ I)) → (A ⧸ I) ⊗[A] B)
        ((quotIdealMapEquivTensorQuot B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            ((algebraMap A B : (a : A) → B) x))) :
      (A ⧸ I) ⊗[A] B)
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x : (A ⧸ I) ⊗[A] B)
⊢ Eq (α := (A ⧸ I) ⊗[A] B)
    (Equiv.toFun
      (RingEquiv.toEquiv
        (RingEquiv.trans (AlgEquiv.toRingEquiv (quotIdealMapEquivTensorQuot B I))
          (AlgEquiv.toRingEquiv (TensorProduct.comm A B (A ⧸ I)))))
      ((algebraMap A (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) I)) :
          (a : A) → B ⧸ Ideal.map (algebraMap A B) I)
        x))
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x)

Tactic:
suffices Algebra.TensorProduct.comm A B (A ⧸ I) (quotIdealMapEquivTensorQuot B I
        (Ideal.Quotient.mk (I.map (algebraMap A B)) (algebraMap A B x))) =
          (algebraMap A (TensorProduct A (A ⧸ I) B)) x by simpa
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
x : A
rw :
  Eq (α := (A ⧸ I) ⊗[A] B)
    ((TensorProduct.comm A B (A ⧸ I) : (a : B ⊗[A] (A ⧸ I)) → (A ⧸ I) ⊗[A] B)
        (1 ⊗ₜ[A] (algebraMap A (A ⧸ I) : (a : A) → A ⧸ I) x) :
      (A ⧸ I) ⊗[A] B)
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x : (A ⧸ I) ⊗[A] B)
⊢ Eq (α := (A ⧸ I) ⊗[A] B)
    ((TensorProduct.comm A B (A ⧸ I) : (a : B ⊗[A] (A ⧸ I)) → (A ⧸ I) ⊗[A] B)
        ((quotIdealMapEquivTensorQuot B I : (a : B ⧸ Ideal.map (algebraMap A B) I) → B ⊗[A] (A ⧸ I))
          ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) I) :
              (a : B) → B ⧸ Ideal.map (algebraMap A B) I)
            ((algebraMap A B : (a : A) → B) x))) :
      (A ⧸ I) ⊗[A] B)
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x : (A ⧸ I) ⊗[A] B)

Tactic:
rw [quotIdealMapEquivTensorQuot_mk, tmul_one_eq_one_tmul]

Premises used: Algebra.TensorProduct.tmul_one_eq_one_tmul, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk
-- Module: Mathlib.RingTheory.TensorProduct.Quotient
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
I : Ideal A
x : A
⊢ Eq (α := (A ⧸ I) ⊗[A] B)
    ((TensorProduct.comm A B (A ⧸ I) : (a : B ⊗[A] (A ⧸ I)) → (A ⧸ I) ⊗[A] B)
        (1 ⊗ₜ[A] (algebraMap A (A ⧸ I) : (a : A) → A ⧸ I) x) :
      (A ⧸ I) ⊗[A] B)
    ((algebraMap A ((A ⧸ I) ⊗[A] B) : (a : A) → (A ⧸ I) ⊗[A] B) x : (A ⧸ I) ⊗[A] B)

Tactic:
simp