awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
refine_3 :
  (∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m) →
    (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
      ∀ (x y : A ⊗[R] B),
        (x * (u + v)) • m = x • (u + v) • m →
          (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m
⊢ (∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m) →
    (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
      ∀ (x y : A ⊗[R] B),
        (x * (u + v)) • m = x • (u + v) • m →
          (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m

Tactic:
_
-- 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
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
h : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
refine_3 :
  (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
    ∀ (x y : A ⊗[R] B),
      (x * (u + v)) • m = x • (u + v) • m →
        (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m
⊢ (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
    ∀ (x y : A ⊗[R] B),
      (x * (u + v)) • m = x • (u + v) • m →
        (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m

Tactic:
_
-- 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
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
h : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
h_1 : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (z * (u + v)) • m = z • (u + v) • m
hw : (w * (u + v)) • m = w • (u + v) • m
refine_3 :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * (u + v)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (u + v) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ ((z + w) * (u + v)) • m = (z + w) • (u + v) • m

Tactic:
simp only [(· • ·)] at hz hw ⊢

Premises used: HSMul.hSMul
-- 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
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
h : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
h_1 : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z * (u + v)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) z : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (u + v) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
hw :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (w * (u + v)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) w : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (u + v) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * (u + v)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (u + v) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)

Tactic:
simp only [add_mul, map_add, LinearMap.add_apply, hz, hw, add_add_add_comm]

Premises used: add_mul, LinearMap.add_apply, map_add, add_add_add_comm
-- 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
inst_11 : SMulCommClass A B M
m : M
simp : (((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (1 ⊗ₜ[R] 1) : M →ₗ[R] M) : (a : M) → M) m = m
⊢ HSMul.hSMul (α := A ⊗[R] B) 1 m = m

Tactic:
simp only [(· • ·), Algebra.TensorProduct.one_def]

Premises used: HSMul.hSMul, Algebra.TensorProduct.one_def
-- 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
inst_11 : SMulCommClass A B M
m : M
⊢ (((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (1 ⊗ₜ[R] 1) : M →ₗ[R] M) : (a : M) → M) m = m

Tactic:
simp only [moduleAux_apply, one_smul]

Premises used: one_smul, TensorProduct.Algebra.moduleAux_apply
-- 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
inst_11 : SMulCommClass A B M
x : A ⊗[R] B
⊢ HSMul.hSMul (β := M) x 0 = 0

Tactic:
simp only [(· • ·), map_zero]

Premises used: map_zero, HSMul.hSMul
-- 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
inst_11 : SMulCommClass A B M
x : A ⊗[R] B
m₁ m₂ : M
⊢ x • (m₁ + m₂) = x • m₁ + x • m₂

Tactic:
simp only [(· • ·), map_add]

Premises used: map_add, HSMul.hSMul
-- 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
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x + y) • m = x • m + y • m

Tactic:
simp only [(· • ·), map_add, LinearMap.add_apply]

Premises used: LinearMap.add_apply, map_add, HSMul.hSMul
-- 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
inst_11 : SMulCommClass A B M
m : M
⊢ HSMul.hSMul (α := A ⊗[R] B) 0 m = 0

Tactic:
simp only [(· • ·), map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, HSMul.hSMul
-- 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
inst_11 : SMulCommClass A B M
a : A
b : B
m : M
⊢ HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m = a • b • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
a :
  Eq (α := A ⊗[R] B)
    ((((AlgebraTensorModule.curry (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
            (a : R) → R →ₗ[R] A ⊗[R] B)
          1 :
        (a : R) → A ⊗[R] B)
      1)
    ((((AlgebraTensorModule.curry (map (Algebra.linearMap R A) (Algebra.linearMap R B)) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
            (a : R) → R →ₗ[R] A ⊗[R] B)
          1 :
        (a : R) → A ⊗[R] B)
      1)
⊢ Eq (α := R ⊗[R] R →ₗ[R] A ⊗[R] B) (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R)
    (map (Algebra.linearMap R A) (Algebra.linearMap R B))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Eq (α := A ⊗[R] B)
    ((((AlgebraTensorModule.curry (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
            (a : R) → R →ₗ[R] A ⊗[R] B)
          1 :
        (a : R) → A ⊗[R] B)
      1)
    ((((AlgebraTensorModule.curry (map (Algebra.linearMap R A) (Algebra.linearMap R B)) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
            (a : R) → R →ₗ[R] A ⊗[R] B)
          1 :
        (a : R) → A ⊗[R] B)
      1)

Tactic:
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, map_tmul,
    Algebra.linearMap_apply, map_one, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.mul'_apply, mul_one, Algebra.TensorProduct.one_def]

Premises used: LinearMap.coe_restrictScalars, LinearMap.mul'_apply, Algebra.linearMap_apply, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.coe_comp, map_one, TensorProduct.curry_apply, TensorProduct.map_tmul, Function.comp_apply, mul_one, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
rw : range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) = HSMul.hSMul (β := Submodule R Q) I ⊤
⊢ map (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (range (rTensor Q I.subtype)) = HSMul.hSMul (β := Submodule R Q) I ⊤

Tactic:
rw [← map_top, ← Submodule.map_comp, map_top]

Premises used: Submodule.map_top, Submodule.map_comp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
q_1 : Q
h : q_1 ∈ HSMul.hSMul (β := Submodule R Q) I ⊤
r : R
hr : r ∈ I
q : Q
h_1 : Membership.mem (γ := Submodule R Q) ⊤ q
⊢ ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ I) r hr ⊗ₜ[R] q) =
    r • q

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
q : Q
h : q ∈ HSMul.hSMul (β := Submodule R Q) I ⊤
⊢ ∀ (x y : Q),
    Membership.mem (γ := Submodule R Q) (range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype))
        x →
      Membership.mem (γ := Submodule R Q) (range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype))
          y →
        Membership.mem (γ := Submodule R Q)
          (range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype)) (x + y)

Tactic:
simp +contextual [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
refine :
  range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) ≤ HSMul.hSMul (β := Submodule R Q) I ⊤
⊢ range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) = HSMul.hSMul (β := Submodule R Q) I ⊤

Tactic:
refine le_antisymm ?_ fun q h ↦ Submodule.smul_induction_on h
    (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
    (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) 0 : Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ ∀ (x : ↥I) (y : Q),
    Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
      (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) (x ⊗ₜ[R] y) : Q)

Tactic:
simp +contextual [Submodule.smul_mem_smul]

Premises used: Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ ∀ (x y : ↥I ⊗[R] Q),
    Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
        (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) x : Q) →
      Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
          (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) y : Q) →
        Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
          (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) (x + y) : Q)

Tactic:
simp +contextual [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ Membership.mem (α := Q) (HSMul.hSMul (β := Submodule R Q) I ⊤)
    (((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype : (a : ↥I ⊗[R] Q) → Q) t : Q)

Tactic:
exact t.induction_on (by simp) (by simp +contextual [Submodule.smul_mem_smul])
    (by simp +contextual [add_mem])
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  {t : S ⊗[R] M | ∃ (m : S) (n : M), m ⊗ₜ[R] n = t} ⊆
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
⊢ Function.Surjective (α := M) (β := S ⊗[R] M) (⇑((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)

Tactic:
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]

Premises used: TensorProduct.span_tmul_eq_top, LinearMap.range_eq_top, top_le_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : S
y : M
obtain :
  ∀ (x : R),
    Membership.mem (α := S ⊗[R] M)
      (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
        Set (S ⊗[R] M))
      ((algebraMap R S : (a : R) → S) x ⊗ₜ[R] y : S ⊗[R] M)
⊢ x ⊗ₜ[R] y ∈
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))

Tactic:
obtain ⟨x, rfl⟩ := h x

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : M
x : R
rw :
  1 ⊗ₜ[R] (x • y) ∈
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
⊢ Membership.mem (α := S ⊗[R] M)
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
    ((algebraMap R S : (a : R) → S) x ⊗ₜ[R] y : S ⊗[R] M)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))

Tactic:
⟨x • y, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, HSMul.hSMul, Set.range, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))

Tactic:
exact ⟨x • y, rfl⟩
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
rw :
  {t : S ⊗[R] T | ∃ (m : S) (n : T), m ⊗ₜ[R] n = t} ⊆
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
⊢ Function.Surjective (α := S) (β := S ⊗[R] T)
    (⇑((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1) : (a : S) → S ⊗[R] T)

Tactic:
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]

Premises used: TensorProduct.span_tmul_eq_top, LinearMap.range_eq_top, top_le_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
t : T
obtain :
  ∀ (r : R),
    Membership.mem (α := S ⊗[R] T)
      (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
            ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
        Set (S ⊗[R] T))
      (s ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
⊢ s ⊗ₜ[R] t ∈
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))

Tactic:
obtain ⟨r, rfl⟩ := h t

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
r : R
rw :
  (r • s) ⊗ₜ[R] 1 ∈
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
⊢ Membership.mem (α := S ⊗[R] T)
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
    (s ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
r : R
⊢ (r • s) ⊗ₜ[R] 1 ∈
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))

Tactic:
⟨r • s, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, HSMul.hSMul, Set.range, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
r : R
⊢ (r • s) ⊗ₜ[R] 1 ∈
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))

Tactic:
exact ⟨r • s, rfl⟩
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Surjective (α := T) (β := S ⊗[R] T) (⇑includeRight : (a : T) → S ⊗[R] T)

Tactic:
TensorProduct.mk_surjective _ _ _ h

Premises used: TensorProduct.mk_surjective, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
T : Type u_4
inst : CommSemiring R
inst_1 : Ring T
inst_2 : Algebra R T
S : Type u_5
A : Type u_6
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Algebra S A
inst_6 : Algebra R A
inst_7 : SMulCommClass R S A
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ Function.Surjective (α := A) (β := A ⊗[R] T) (⇑includeLeft : (a : A) → A ⊗[R] T)

Tactic:
TensorProduct.flip_mk_surjective _ h

Premises used: TensorProduct.flip_mk_surjective, TensorProduct.tmul, AddCon.toQuotient