awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
b : B
x : A ⊗[R] B
a :
  ∀ (xa : A) (xb : B),
    Eq (α := A ⊗[R] B)
      (((((AlgebraTensorModule.curry (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                    A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                xa :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          xb :
        A ⊗[R] B)
      (((((AlgebraTensorModule.curry (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                    A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                  (a : A) → B →ₗ[R] A ⊗[R] B)
                xa :
              B →ₗ[R] A ⊗[R] B) :
            (a : B) → A ⊗[R] B)
          xb :
        A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)

Tactic:
ext xa xb
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
b : B
x : A ⊗[R] B
xa : A
xb : B
⊢ Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              xa :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        xb :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              xa :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        xb :
      A ⊗[R] B)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
⊢ Eq (α := B →+* A ⊗[R] B) (algebraMap B (A ⊗[R] B)) (↑includeRight : B →+* A ⊗[R] B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
⊢ IsScalarTower R B (A ⊗[R] B)

Tactic:
IsScalarTower.of_algebraMap_eq fun r => (Algebra.TensorProduct.includeRight.commutes r).symm

Premises used: IsScalarTower.of_algebraMap_eq, AlgHom.commutes, Eq.symm, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
b : B
⊢ Eq (α := A ⊗[R] B) ((algebraMap B (A ⊗[R] B) : (a : B) → A ⊗[R] B) b : A ⊗[R] B) (1 ⊗ₜ[R] b : A ⊗[R] B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
a : A
b : B
x : A ⊗[R] B
⊢ a • HSMul.hSMul (β := A ⊗[R] B) b 0 = b • HSMul.hSMul (β := A ⊗[R] B) a 0

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
a : A
b : B
x : A ⊗[R] B
x_1 : A
x_2 : B
⊢ a • HSMul.hSMul (β := A ⊗[R] B) b (x_1 ⊗ₜ[R] x_2) = b • HSMul.hSMul (β := A ⊗[R] B) a (x_1 ⊗ₜ[R] x_2)

Tactic:
simp [Algebra.smul_def, right_algebraMap_apply, smul_tmul']

Premises used: Algebra.TensorProduct.right_algebraMap_apply, TensorProduct.smul_tmul', Algebra.smul_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
a : A
b : B
x x_1 x_2 : A ⊗[R] B
h₁ : a • b • x_1 = b • a • x_1
h₂ : a • b • x_2 = b • a • x_2
⊢ a • b • (x_1 + x_2) = b • a • (x_1 + x_2)

Tactic:
simpa using congr($h₁ + $h₂)
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
⊢ SMulCommClass B A (A ⊗[R] B)

Tactic:
.symm ..

Premises used: SMulCommClass.symm
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : Ring A
inst_1 : Ring B
⊢ Ring (A ⊗[ℤ] B)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommRing A
inst_1 : CommRing B
⊢ CommRing (A ⊗[ℤ] B)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
rw :
  LE.le (α := Subring (A ⊗[R] B)) ⊤
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
⊢ Eq (α := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
h :
  x ⊗ₜ[R] y =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B)
tmul :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B))
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x ⊗ₜ[R] y)

Tactic:
convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _

Premises used: Algebra.TensorProduct.includeLeftRingHom, DFunLike.coe, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
⊢ x ⊗ₜ[R] y =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B))

Tactic:
mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))

Premises used: Set.Mem, Subring.subset_closure, Exists.intro, Or.inl, Or.inr, rfl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B))

Tactic:
exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))

Premises used: Subring.subset_closure, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x y : A ⊗[R] B
h :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x
h_1 :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    y
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x + y)

Tactic:
add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x y : A ⊗[R] B
h :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x
h_1 :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    y
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x + y)

Tactic:
exact add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
zero :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    0
tmul :
  ∀ (x : A) (y : B),
    Membership.mem (γ := Subring (A ⊗[R] B))
      (Subring.closure
        (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
          Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
      (x ⊗ₜ[R] y)
add :
  ∀ (x y : A ⊗[R] B),
    Membership.mem (γ := Subring (A ⊗[R] B))
        (Subring.closure
          (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
            Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
        x →
      Membership.mem (γ := Subring (A ⊗[R] B))
          (Subring.closure
            (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
              Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
          y →
        Membership.mem (γ := Subring (A ⊗[R] B))
          (Subring.closure
            (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
              Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
          (x + y)
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x

Tactic:
induction x with
  | zero => exact zero_mem _
  | tmul x y =>
    convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
    · simp
    · exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))
  | add x y _ _ => exact add_mem ‹_› ‹_›

Premises used: Algebra.TensorProduct.includeLeftRingHom, Subring.subset_closure, AddMemClass.add_mem, ZeroMemClass.zero_mem, TensorProduct.tmul, DFunLike.coe, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
h : Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A (↑(Subalgebra.map includeRight ⊤) : Set (A ⊗[R] B))) ⊤
⊢ Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A ((fun (x : B) ↦ 1 ⊗ₜ[R] x) '' s)) ⊤

Tactic:
simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]

Premises used: Algebra.adjoin_adjoin_of_tower, AlgHom.map_adjoin
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
suffices : Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A (↑(Subalgebra.map includeRight ⊤) : Set (A ⊗[R] B))) ⊤
⊢ Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A ((fun (x : B) ↦ 1 ⊗ₜ[R] x) '' s)) ⊤

Tactic:
suffices h : adjoin A ((⊤ : Subalgebra R B).map (includeRight (A := A)) : Set (A ⊗[R] B)) = ⊤ by
    simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
rw :
  LE.le (α := Submodule A (A ⊗[R] B))
    (Submodule.span A
      (↑(LinearMap.range (R := R) (M := B) (τ₁₂ := RingHom.id R)
            ((TensorProduct.mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
        Set (A ⊗[R] B)))
    ((Subalgebra.toSubmodule : (a : Subalgebra A (A ⊗[R] B)) → Submodule A (A ⊗[R] B))
      (adjoin A (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))))
⊢ Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A (↑(Subalgebra.map includeRight ⊤) : Set (A ⊗[R] B))) ⊤

Tactic:
rw [← Algebra.toSubmodule_eq_top, ← top_le_iff, Algebra.map_top, ← Submodule.baseChange_top,
    Submodule.baseChange_eq_span, Submodule.map_top]

Premises used: Submodule.map_top, Submodule.baseChange_eq_span, Algebra.toSubmodule_eq_top, top_le_iff, Algebra.map_top, Submodule.baseChange_top
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
⊢ LE.le (α := Submodule A (A ⊗[R] B))
    (Submodule.span A
      (↑(LinearMap.range (R := R) (M := B) (τ₁₂ := RingHom.id R)
            ((TensorProduct.mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
        Set (A ⊗[R] B)))
    ((Subalgebra.toSubmodule : (a : Subalgebra A (A ⊗[R] B)) → Submodule A (A ⊗[R] B))
      (adjoin A (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))))

Tactic:
span_le_adjoin _ _

Premises used: Set.Mem, Algebra.span_le_adjoin, setOf, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
⊢ LE.le (α := Submodule A (A ⊗[R] B))
    (Submodule.span A
      (↑(LinearMap.range (R := R) (M := B) (τ₁₂ := RingHom.id R)
            ((TensorProduct.mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
        Set (A ⊗[R] B)))
    ((Subalgebra.toSubmodule : (a : Subalgebra A (A ⊗[R] B)) → Submodule A (A ⊗[R] B))
      (adjoin A (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))))

Tactic:
exact span_le_adjoin _ _

Premises used: Algebra.span_le_adjoin
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
apply :
  Function.RightInverse (α := S ⊗[R] M) (β := M)
    (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (⇑(LinearMap.liftBaseChange S LinearMap.id) : (a : S ⊗[R] M) → M)
⊢ Function.Injective (α := M) (β := S ⊗[R] M)
    (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)

Tactic:
apply Function.RightInverse.injective (g := LinearMap.liftBaseChange S LinearMap.id)

Premises used: Function.RightInverse.injective
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
m : M
⊢ (LinearMap.liftBaseChange S LinearMap.id : (a : S ⊗[R] M) → M)
      (((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) m : S ⊗[R] M) =
    m

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : B
a :
  ∀ (i : B),
    Eq (α := A ⊗[R] B)
      ((((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B : (a : B) → Module.End R B) f)) :
                  A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              1 :
            (a : B) → A ⊗[R] B)
          i :
        A ⊗[R] B)
      ((((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B) : (a : A ⊗[R] B) → Module.End A (A ⊗[R] B)) (1 ⊗ₜ[R] f)) :
                  A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              1 :
            (a : B) → A ⊗[R] B)
          i :
        A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B →ₗ[A] A ⊗[R] B) (LinearMap.baseChange A ((lmul R B : (a : B) → Module.End R B) f))
    ((lmul A (A ⊗[R] B) : (a : A ⊗[R] B) → Module.End A (A ⊗[R] B)) (1 ⊗ₜ[R] f))

Tactic:
ext i
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f i : B
⊢ Eq (α := A ⊗[R] B)
    ((((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B : (a : B) → Module.End R B) f)) :
                A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
              (a : A) → B →ₗ[R] A ⊗[R] B)
            1 :
          (a : B) → A ⊗[R] B)
        i :
      A ⊗[R] B)
    ((((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B) : (a : A ⊗[R] B) → Module.End A (A ⊗[R] B)) (1 ⊗ₜ[R] f)) :
                A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
              (a : A) → B →ₗ[R] A ⊗[R] B)
            1 :
          (a : B) → A ⊗[R] B)
        i :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
r t : A
h :
  ∀ (x : B) (x_1 : M),
    Eq (α := M)
      ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (r + t)
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                  (a : B) → Module.End R M)
                x :
              Module.End R M) :
            (a : M) → M)
          x_1 :
        M)
      ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                      (AlgHom.toLinearMap (Algebra.lsmul R R M)) +
                    HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) t
                      (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                  (a : B) → Module.End R M)
                x :
              Module.End R M) :
            (a : M) → M)
          x_1 :
        M)
⊢ HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (r + t)
      (AlgHom.toLinearMap (Algebra.lsmul R R M)) =
    HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
        (AlgHom.toLinearMap (Algebra.lsmul R R M)) +
      HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) t
        (AlgHom.toLinearMap (Algebra.lsmul R R M))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
r t : A
x : B
x_1 : M
⊢ Eq (α := M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (r + t)
                  (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) +
                  HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) t
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)

Tactic:
simp only [add_smul, LinearMap.add_apply]

Premises used: LinearMap.add_apply, add_smul