awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
      (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
      Ideal.map (F := C →ₐ[R] A ⊗[R] C) includeRight (RingHom.ker g))
have rw : Eq (α := Ideal (A ⊗[R] C))
  (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D) (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
    (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
  (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
    Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) ⊥)
Tactic: rw [← Algebra.TensorProduct.lTensor_ker _ hg, RingHom.ker_eq_comap_bot (map (AlgHom.id R A) g)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
      (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f) ⊔
      Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) ⊥)
have rw : Eq (α := Ideal (A ⊗[R] C))
  (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D) (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
    (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
  (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
    (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
Tactic: rw [← Ideal.comap_map_of_surjective (map (AlgHom.id R A) g) (LinearMap.lTensor_surjective A hg)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
      (RingHom.ker (F := A ⊗[R] D →ₐ[S] B ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)))
    (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
have rw : Eq (α := Ideal (A ⊗[R] C))
  (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D) (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
    (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f)))
  (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
    (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
Tactic: rw [Algebra.TensorProduct.rTensor_ker _ hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] C))
    (Ideal.comap (F := A ⊗[R] C →+* A ⊗[R] D)
      (↑(map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f)))
    (Ideal.comap (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
        (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f))))
have apply : Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f))
  (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
    (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))
Tactic: apply congr_arg₂ _ rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →ₐ[R] A ⊗[R] D) includeLeft (RingHom.ker f))
    (Ideal.map (R := A ⊗[R] C) (F := A ⊗[R] C →ₐ[R] A ⊗[R] D) (map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D)
      (Ideal.map (F := A →ₐ[R] A ⊗[R] C) includeLeft (RingHom.ker f)))
have simp : Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
  (Ideal.map (F := A →+* A ⊗[R] D)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] C))
    (RingHom.ker f))
Tactic: simp only [AlgHom.coe_ideal_map, Ideal.map_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Ring C
inst_6 : Ring D
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
inst_10 : Algebra R D
inst_11 : Algebra S A
inst_12 : Algebra S B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hg : Function.Surjective.{u_8 + 1, u_9 + 1} (α := C) (β := D) (⇑g : (a : C) → D)
this :
  Eq (α := A ⊗[R] C →ₐ[S] B ⊗[R] D) (map f g : A ⊗[R] C →ₐ[S] B ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] B ⊗[R] D)
        (map (AlgHom.id S A) g : A ⊗[R] C →ₐ[S] A ⊗[R] D) :
      A ⊗[R] C →ₐ[S] B ⊗[R] D)
⊢ Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
    (Ideal.map (F := A →+* A ⊗[R] D)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(map (AlgHom.id R A) g : A ⊗[R] C →ₐ[R] A ⊗[R] D) : A ⊗[R] C →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] C))
      (RingHom.ker f))
have rw : Eq (α := Ideal (A ⊗[R] D)) (Ideal.map (F := A →+* A ⊗[R] D) (↑includeLeft : A →+* A ⊗[R] D) (RingHom.ker f))
  (Ideal.map (F := A →+* A ⊗[R] D) (↑(AlgHom.comp includeLeft (AlgHom.id R A)) : A →+* A ⊗[R] D) (RingHom.ker f))
Tactic: rw [← AlgHom.comp_toRingHom, Algebra.TensorProduct.map_comp_includeLeft]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
⊢ ↥⊥ ⊗[R] ↥A ≃ₐ[R] ↥A
have refine_1 : ∀ (a₁ a₂ : ↥⊥) (b₁ b₂ : ↥A),
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (a₁ ⊗ₜ[R] b₁) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (a₂ ⊗ₜ[R] b₂) :
        ↥A)
Tactic: refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).lTensorOne ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
refine_1 :
  ∀ (a₁ a₂ : ↥⊥) (b₁ b₂ : ↥A),
    ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
            ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
          (a : ↥⊥ ⊗[R] ↥A) → ↥A)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := ↥A) (β := ↥A)
        (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥⊥ ⊗[R] ↥A) → ↥A)
            (a₁ ⊗ₜ[R] b₁) :
          ↥A)
        (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
                ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
              (a : ↥⊥ ⊗[R] ↥A) → ↥A)
            (a₂ ⊗ₜ[R] b₂) :
          ↥A)
⊢ ↥⊥ ⊗[R] ↥A ≃ₐ[R] ↥A
have refine_2 : Eq.{u_2 + 1} (α := ↥A)
  (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      (1 ⊗ₜ[R] 1) :
    ↥A)
  (1 : ↥A)
Tactic: refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).lTensorOne ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have refine_1 : ∀ (x' : R) (hx : (algebraMap R S : (a : R) → S) x' = (↑x : S)),
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
Tactic: obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R S : (a : R) → S) x' = (↑x : S)
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have hx₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
Tactic: replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have refine_1 : ∀ (y' : R) (hy : (algebraMap R S : (a : R) → S) y' = (↑y : S)),
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
Tactic: obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R S : (a : R) → S) y' = (↑y : S)
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have hy₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
Tactic: replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
Cleared hypotheses: hy