awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
m : M
a : A
n : N
⊢ HSMul.hSMul (β := M ⊗[R] N) a (m ⊗ₜ[R] n) - m ⊗ₜ[R] (a • n) ∈ S

Tactic:
exact Submodule.subset_span ⟨a, m, n, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x x_1 : M
h :
  ∀ (x_2 : N),
    Eq (α := M ⊗[R] N ⧸ S)
      (({ toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x + x_1) ⊗ₜ[R] n), map_add' := ⋯,
              map_smul' := ⋯ } :
            (a : N) → M ⊗[R] N ⧸ S)
          x_2 :
        M ⊗[R] N ⧸ S)
      ((HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N ⧸ S)
              { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x ⊗ₜ[R] n), map_add' := ⋯,
                map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N ⧸ S }
              { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯,
                map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N ⧸ S } :
            (a : N) → M ⊗[R] N ⧸ S)
          x_2 :
        M ⊗[R] N ⧸ S)
⊢ { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x + x_1) ⊗ₜ[R] n), map_add' := ⋯,
      map_smul' := ⋯ } =
    HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N ⧸ S)
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }

Tactic:
ext _
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x x_1 : M
x_2 : N
⊢ Eq (α := M ⊗[R] N ⧸ S)
    (({ toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x + x_1) ⊗ₜ[R] n), map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : N) → M ⊗[R] N ⧸ S)
        x_2 :
      M ⊗[R] N ⧸ S)
    ((HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N ⧸ S)
            { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x ⊗ₜ[R] n), map_add' := ⋯,
              map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N ⧸ S }
            { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯,
              map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N ⧸ S } :
          (a : N) → M ⊗[R] N ⧸ S)
        x_2 :
      M ⊗[R] N ⧸ S)

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x : A
x_1 : M
simp :
  { toFun := fun (n : N) ↦ Submodule.Quotient.mk ((x • x_1) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (β := N →ₗ[A] M ⊗[R] N ⧸ S) x
      { toFun := fun (n : N) ↦ Submodule.Quotient.mk (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }
⊢ { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x • x_1) ⊗ₜ[R] n), map_add' := ⋯,
      map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := N →ₗ[A] M ⊗[R] N ⧸ S) ((RingHom.id A : (a : A) → A) x : A)
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x : A
x_1 : M
⊢ { toFun := fun (n : N) ↦ Submodule.Quotient.mk ((x • x_1) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (β := N →ₗ[A] M ⊗[R] N ⧸ S) x
      { toFun := fun (n : N) ↦ Submodule.Quotient.mk (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := M ⊗[R] N ⧸ S)
      (((((curry (F ∘ₗ mapOfCompatibleSMul A R A M N) : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S)
                x :
              N →ₗ[R] M ⊗[R] N ⧸ S) :
            (a : N) → M ⊗[R] N ⧸ S)
          x_1 :
        M ⊗[R] N ⧸ S)
      (((((curry S.mkQ : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S) x : N →ₗ[R] M ⊗[R] N ⧸ S) :
            (a : N) → M ⊗[R] N ⧸ S)
          x_1 :
        M ⊗[R] N ⧸ S)
⊢ F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
x : M
x_1 : N
⊢ Eq (α := M ⊗[R] N ⧸ S)
    (((((curry (F ∘ₗ mapOfCompatibleSMul A R A M N) : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S)
              x :
            N →ₗ[R] M ⊗[R] N ⧸ S) :
          (a : N) → M ⊗[R] N ⧸ S)
        x_1 :
      M ⊗[R] N ⧸ S)
    (((((curry S.mkQ : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S) x : N →ₗ[R] M ⊗[R] N ⧸ S) :
          (a : N) → M ⊗[R] N ⧸ S)
        x_1 :
      M ⊗[R] N ⧸ S)

Tactic:
simp [S, F]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
⊢ F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ

Tactic:
have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ := by ext; simp [S, F]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
refine_2 : LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N) ≤ S
⊢ LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})

Tactic:
change (mapOfCompatibleSMul A R A M N).ker ≤ S

Premises used: TensorProduct.mapOfCompatibleSMul, LinearMap.ker
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
refine_2 :
  LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (LinearMap.ker (F ∘ₗ mapOfCompatibleSMul A R A M N))
⊢ LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N) ≤ S

Tactic:
rw [← Submodule.ker_mkQ S, ← h]

Premises used: Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (LinearMap.ker (F ∘ₗ mapOfCompatibleSMul A R A M N))

Tactic:
(mapOfCompatibleSMul A R A M N).ker_le_ker_comp F

Premises used: TensorProduct.mapOfCompatibleSMul, Set.Mem, LinearMap.ker_le_ker_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (LinearMap.ker (F ∘ₗ mapOfCompatibleSMul A R A M N))

Tactic:
exact (mapOfCompatibleSMul A R A M N).ker_le_ker_comp F

Premises used: TensorProduct.mapOfCompatibleSMul, LinearMap.ker_le_ker_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.comap (M₂ := Q ⊗[R] P) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R Q P : (a : Q) → P →ₗ[R] Q ⊗[R] P) q)
      (range (lTensor Q g)))
    ((g : (a : N) → P) n : P)

Tactic:
⟨q ⊗ₜ[R] n, rfl⟩

Premises used: Set.Mem, setOf, Set.preimage, Exists.intro, TensorProduct.tmul, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.comap (M₂ := Q ⊗[R] P) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R Q P : (a : Q) → P →ₗ[R] Q ⊗[R] P) q)
      (range (lTensor Q g)))
    ((g : (a : N) → P) n : P)

Tactic:
exact ⟨q ⊗ₜ[R] n, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.comap (M₂ := P ⊗[R] Q) (σ₁₂ := RingHom.id R)
      ((LinearMap.flip (TensorProduct.mk R P Q) : (a : Q) → P →ₗ[R] P ⊗[R] Q) q) (range (rTensor Q g)))
    ((g : (a : N) → P) n : P)

Tactic:
⟨n ⊗ₜ[R] q, rfl⟩

Premises used: Set.Mem, setOf, Set.preimage, Exists.intro, TensorProduct.tmul, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.comap (M₂ := P ⊗[R] Q) (σ₁₂ := RingHom.id R)
      ((LinearMap.flip (TensorProduct.mk R P Q) : (a : Q) → P →ₗ[R] P ⊗[R] Q) q) (range (rTensor Q g)))
    ((g : (a : N) → P) n : P)

Tactic:
exact ⟨n ⊗ₜ[R] q, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
⊢ g = g.range.subtype ∘ₗ g.rangeRestrict

Tactic:
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
nth_rewrite :
  Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (lTensor Q g.range.subtype))
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g)) (range (lTensor Q g.range.subtype))

Tactic:
nth_rewrite 1 [this]
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
rw :
  Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict))
    (range (lTensor Q g.range.subtype))
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (lTensor Q g.range.subtype))

Tactic:
rw [lTensor_comp]

Premises used: LinearMap.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Eq (α := Submodule R (TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)) (range (lTensor Q g.rangeRestrict)) ⊤
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict))
    (range (lTensor Q g.range.subtype))

Tactic:
apply range_comp_of_range_eq_top

Premises used: LinearMap.range_comp_of_range_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf :
  Function.Surjective (α := Q ⊗[R] N) (β := TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)
    (⇑(lTensor Q g.rangeRestrict) : (a : Q ⊗[R] N) → Q ⊗[R] ↥g.range)
⊢ Eq (α := Submodule R (TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)) (range (lTensor Q g.rangeRestrict)) ⊤

Tactic:
rw [range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
⊢ Function.Surjective (α := Q ⊗[R] N) (β := TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)
    (⇑(lTensor Q g.rangeRestrict) : (a : Q ⊗[R] N) → Q ⊗[R] ↥g.range)

Tactic:
apply lTensor_surjective

Premises used: LinearMap.lTensor_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Eq (α := Submodule R ↥g.range) (range g.rangeRestrict) ⊤
hf₁ hf₂ : Eq.{u_4 + 1} (α := Submodule R ↥g.range) ⊤ ⊤
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)

Tactic:
rw [← range_eq_top, range_rangeRestrict]

Premises used: LinearMap.range_rangeRestrict, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
A : Type u_6
inst_5 : Semiring A
inst_6 : Algebra R A
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
rw : Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(lTensor A g) : (a : A ⊗[R] N) → A ⊗[R] P)
⊢ Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(baseChange A g) : (a : A ⊗[R] N) → A ⊗[R] P)

Tactic:
rw [LinearMap.baseChange_eq_ltensor]

Premises used: LinearMap.baseChange_eq_ltensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
A : Type u_6
inst_5 : Semiring A
inst_6 : Algebra R A
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(lTensor A g) : (a : A ⊗[R] N) → A ⊗[R] P)

Tactic:
lTensor_surjective _ hg

Premises used: LinearMap.lTensor_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
A : Type u_6
inst_5 : Semiring A
inst_6 : Algebra R A
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(lTensor A g) : (a : A ⊗[R] N) → A ⊗[R] P)

Tactic:
exact lTensor_surjective _ hg

Premises used: LinearMap.lTensor_surjective
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)

Tactic:
⟨0, map_zero _⟩

Premises used: map_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)

Tactic:
exact ⟨0, map_zero _⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
p : P
q : Q
tmul :
  ∀ (n : N),
    ∃ (a : N ⊗[R] Q),
      Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q)
        ((g : (a : N) → P) n ⊗ₜ[R] q : P ⊗[R] Q)
⊢ ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (p ⊗ₜ[R] q : P ⊗[R] Q)

Tactic:
obtain ⟨n, rfl⟩ := hg p

Premises used: rfl