awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
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 : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
y : A ⊗[R] ((i : ι) → B i)
x : A
y_1 : (i : ι) → B i
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y_1 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
have tmul : ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
      (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
    (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y_1) 0) =
  HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
    (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        (x ⊗ₜ[R] y_1) :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        0 :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
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 : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
y : A ⊗[R] ((i : ι) → B i)
x : A
y_1 : (i : ι) → B i
tmul :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y_1) 0) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          0 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y_1 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
have tmul₁ : ∀ (x_1 : A) (y : (i : ι) → B i),
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y_1) (x_1 ⊗ₜ[R] y)) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
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 : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x : A
y : (i : ι) → B i
x_1 : A
y_1 : (i : ι) → B i
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) (x_1 ⊗ₜ[R] y_1)) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
have tmul : ∀ (j : ι),
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) (x_1 ⊗ₜ[R] y_1)) j =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      j
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
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 × 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))
have 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)
Tactic: apply (prodRight R S A B C).injective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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)
⊢ ((↑(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))
have 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)) sorry ≪≫ₗ
                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)) sorry ≪≫ₗ
                    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: obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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)
⊢ (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))
have 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))
Tactic: obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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
⊢ (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))
have 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))
Tactic: obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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
⊢ (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))
have simp_rw : (u * v) ⊗ₜ[A] 1 = HMul.hMul (α := B ⊗[A] (A ⧸ I)) (u ⊗ₜ[A] 1) (v ⊗ₜ[A] 1)
Tactic: simp_rw [← map_mul, quotIdealMapEquivTensorQuotAux_mk]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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)
    (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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
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)
        ((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)
have 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)
Tactic: rw [quotIdealMapEquivTensorQuot_mk, tmul_one_eq_one_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ LinearMap.range ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)) =
    HSMul.hSMul (β := Submodule R M) I ⊤
have rw : Eq (α := Submodule R (R ⊗[R] M)) (LinearMap.ker (M₂ := (R ⧸ I) ⊗[R] M) (LinearMap.rTensor M (Submodule.mkQ I)))
  (LinearMap.range (LinearMap.rTensor M (Submodule.subtype I)))
Tactic: rw [← Submodule.ker_mkQ (I • (⊤ : Submodule R M)), LinearMap.range_comp,
    ← Submodule.map_symm_eq_iff, ← Submodule.comap_equiv_eq_map_symm, ← LinearMap.ker_comp,
    ← TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, LinearEquiv.ker_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
⊢ IsFiniteSplit T (T ⊗[R] S)
have obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), IsFiniteSplit T (T ⊗[R] S)
Tactic: obtain ⟨n, ⟨e⟩⟩ := Algebra.IsFiniteSplit.nonempty_algEquiv_fun R S
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ IsFiniteSplit T (T ⊗[R] S)
have refine : T ⊗[R] S ≃ₐ[T] Fin n → T
Tactic: refine ⟨n, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
⊢ ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)
have intro : ∀ (val : Fintype ι), ∃ (n : ℕ), Nonempty ((ι → R) ≃ₐ[R] Fin n → R)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_3
inst_3 : CommRing S'
inst_4 : Algebra R S'
e : S ≃ₐ[R] S'
inst_5 : IsFiniteSplit R S
⊢ IsFiniteSplit R S'
have obtain : ∀ (n : ℕ) (f : S ≃ₐ[R] Fin n → R), IsFiniteSplit R S'
Tactic: obtain ⟨n, ⟨f⟩⟩ := nonempty_algEquiv_fun R S
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Subsingleton R
⊢ IsFiniteSplit R S
have this : Subsingleton S
Tactic: have : Subsingleton S := RingHom.codomain_trivial (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
⊢ Module.Free R S
have obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Module.Free R S
Tactic: obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
⊢ Module.FinitePresentation R S
have obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Module.FinitePresentation R S
Tactic: obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S
-- Lean 4 proof step from Mathlib.RingTheory.TotallySplit (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsFiniteSplit R S
⊢ Etale R S
have obtain : ∀ (n : ℕ) (e : S ≃ₐ[R] Fin n → R), Etale R S
Tactic: obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S