awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
refine_1 :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
        {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x →
      ∀ (a : A) (m : ↥p) (h : a ⊗ₜ[R] m = x),
        x ∈
          (↑(comap (LinearMap.baseChange A p.subtype)
                (span A
                  (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
                    Set (A ⊗[R] M)))) :
            Set (A ⊗[R] ↥p))
⊢ {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} ⊆
    (↑(comap (LinearMap.baseChange A p.subtype)
          (span A
            (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
              Set (A ⊗[R] M)))) :
      Set (A ⊗[R] ↥p))

Tactic:
refine fun _ ⟨a, m, h⟩ ↦ ?_
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
h_1 :
  Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
    {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x
a : A
m : ↥p
h : a ⊗ₜ[R] m = x
refine_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)))
    (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] (p.subtype : (a : ↥p) → M) m : A ⊗[R] M))
⊢ x ∈
    (↑(comap (LinearMap.baseChange A p.subtype)
          (span A
            (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
              Set (A ⊗[R] M)))) :
      Set (A ⊗[R] ↥p))

Tactic:
rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul,
      ← smul_tmul']

Premises used: Submodule.mem_comap, TensorProduct.smul_tmul', SetLike.mem_coe, smul_eq_mul, mul_one, LinearMap.baseChange_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
h_1 :
  Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
    {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x
a : A
m : ↥p
h : a ⊗ₜ[R] m = x
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M))
    (span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)))
    (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] (p.subtype : (a : ↥p) → M) m : A ⊗[R] M))

Tactic:
smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)

Premises used: Set.Mem, And.intro, Exists.intro, Submodule.subset_span, Subtype.val, rfl, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
h_1 :
  Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
    {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x
a : A
m : ↥p
h : a ⊗ₜ[R] m = x
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M))
    (span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)))
    (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] (p.subtype : (a : ↥p) → M) m : A ⊗[R] M))

Tactic:
exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)) ≤
    baseChange A p

Tactic:
span_le.2 fun _ ⟨m, hm, h⟩ ↦ h ▸ ⟨1 ⊗ₜ[R] ⟨m, hm⟩, rfl⟩

Premises used: Iff.mpr, _private.0.Submodule.baseChange_eq_span.match_3, Membership.mem, Eq.rec, Subtype.mk, SetLike.coe, Submodule.baseChange, Exists.intro, TensorProduct.tmul, OfNat.ofNat, Submodule.span_le, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)) ≤
    baseChange A p

Tactic:
refine span_le.2 fun _ ⟨m, hm, h⟩ ↦ h ▸ ⟨1 ⊗ₜ[R] ⟨m, hm⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A ⊥) ⊥

Tactic:
simp [baseChange_eq_span]

Premises used: Submodule.baseChange_eq_span
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
rw : LE.le (α := Submodule A (A ⊗[R] M)) (span A {t : A ⊗[R] M | ∃ (m : A) (n : M), m ⊗ₜ[R] n = t}) (baseChange A ⊤)
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A ⊤) ⊤

Tactic:
rw [eq_top_iff, ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)]

Premises used: TensorProduct.span_tmul_eq_top, eq_top_iff, Submodule.span_eq_top_of_span_eq_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (span A {t : A ⊗[R] M | ∃ (m : A) (n : M), m ⊗ₜ[R] n = t}) (baseChange A ⊤)

Tactic:
span_le.2 fun _ ⟨a, m, h⟩ ↦ h ▸ tmul_mem_baseChange_of_mem _ trivial

Premises used: Iff.mpr, trivial, Membership.mem, Eq.rec, Submodule.tmul_mem_baseChange_of_mem, SetLike.coe, Submodule.baseChange, _private.0.Submodule.baseChange_top.match_1, Top.top, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (span A {t : A ⊗[R] M | ∃ (m : A) (n : M), m ⊗ₜ[R] n = t}) (baseChange A ⊤)

Tactic:
exact span_le.2 fun _ ⟨a, m, h⟩ ↦ h ▸ tmul_mem_baseChange_of_mem _ trivial
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p q : Submodule R M
h : p ≤ q
rw :
  LE.le (α := Submodule A (A ⊗[R] M))
    (LinearMap.range (M := TensorProduct.{u_1, u_3, u_2} R A ↥p)
        ((AlgebraTensorModule.map LinearMap.id q.subtype : TensorProduct.{u_1, u_3, u_2} R A ↥q →ₗ[A] A ⊗[R] M) ∘ₗ
            (AlgebraTensorModule.map LinearMap.id (inclusion h) :
              TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] TensorProduct.{u_1, u_3, u_2} R A ↥q) :
          TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] A ⊗[R] M) :
      Submodule A (A ⊗[R] M))
    (baseChange A q : Submodule A (A ⊗[R] M))
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)

Tactic:
rw [baseChange, LinearMap.baseChange, ← subtype_comp_inclusion p q h,
    ← LinearMap.id_comp LinearMap.id, AlgebraTensorModule.map_comp]

Premises used: Submodule.subtype_comp_inclusion, LinearMap.id, LinearMap.baseChange, TensorProduct.AlgebraTensorModule.map_comp, Submodule.baseChange, LinearMap.id_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p q : Submodule R M
h : p ≤ q
⊢ LE.le (α := Submodule A (A ⊗[R] M))
    (LinearMap.range (M := TensorProduct.{u_1, u_3, u_2} R A ↥p)
        ((AlgebraTensorModule.map LinearMap.id q.subtype : TensorProduct.{u_1, u_3, u_2} R A ↥q →ₗ[A] A ⊗[R] M) ∘ₗ
            (AlgebraTensorModule.map LinearMap.id (inclusion h) :
              TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] TensorProduct.{u_1, u_3, u_2} R A ↥q) :
          TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] A ⊗[R] M) :
      Submodule A (A ⊗[R] M))
    (baseChange A q : Submodule A (A ⊗[R] M))

Tactic:
apply LinearMap.range_comp_le_range

Premises used: LinearMap.range_comp_le_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
s : Set M
rw :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A
      (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (span R s)) :
        Set (A ⊗[R] M)))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
rw₁ :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A
      (↑(span R ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s)) :
        Set (A ⊗[R] M)))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
rw₂ rw₃ :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A (span R s))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))

Tactic:
rw [baseChange_eq_span, map_span, span_span_of_tower]

Premises used: Submodule.span_span_of_tower, Submodule.baseChange_eq_span, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
a : A
x : ↥p
⊢ Eq (α := A ⊗[R] M) (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) (a ⊗ₜ[R] x)) : A ⊗[R] M)
    (a ⊗ₜ[R] (↑x : M))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ Function.Surjective (α := TensorProduct.{u_1, u_3, u_2} R A ↥p) (β := ↥(baseChange A p))
    (⇑(toBaseChange A p) : (a : A ⊗[R] ↥p) → ↥(baseChange A p))

Tactic:
LinearMap.surjective_rangeRestrict _

Premises used: Set.Mem, LinearMap.surjective_rangeRestrict
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) y
obtain :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p)
    (hx :
      (toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x =
        Subtype.mk (p := fun (x : A ⊗[R] M) ↦ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) x) y hy),
    ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
      (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y
⊢ ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y

Tactic:
obtain ⟨x, hx⟩ := toBaseChange_surjective A p ⟨y, hy⟩

Premises used: Submodule.toBaseChange_surjective, Subtype.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) y
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
hx :
  (toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x =
    Subtype.mk (p := fun (x : A ⊗[R] M) ↦ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) x) y hy
⊢ ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y

Tactic:
⟨x, congr($hx)⟩

Premises used: congrArg, id, Exists.intro, Subtype.val
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) y
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
hx :
  (toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x =
    Subtype.mk (p := fun (x : A ⊗[R] M) ↦ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) x) y hy
⊢ ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y

Tactic:
exact ⟨x, congr($hx)⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
rw :
  LinearMap.baseChange A f ∘ₗ
      (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f
⊢ LinearMap.baseChange A f ∘ₗ (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f

Tactic:
rw [cancelBaseChange_self_eq_lid]

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange_self_eq_lid
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
a :
  ∀ (x : M),
    Eq (α := A ⊗[A] N)
      ((((curry
                    (LinearMap.baseChange A f ∘ₗ
                      (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) :
                  A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
                (a : A) → M →ₗ[R] A ⊗[A] N)
              1 :
            (a : M) → A ⊗[A] N)
          x :
        A ⊗[A] N)
      ((((curry ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f) : A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
                (a : A) → M →ₗ[R] A ⊗[A] N)
              1 :
            (a : M) → A ⊗[A] N)
          x :
        A ⊗[A] N)
⊢ LinearMap.baseChange A f ∘ₗ
      (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
x : M
⊢ Eq (α := A ⊗[A] N)
    ((((curry
                  (LinearMap.baseChange A f ∘ₗ
                    (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) :
                A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
              (a : A) → M →ₗ[R] A ⊗[A] N)
            1 :
          (a : M) → A ⊗[A] N)
        x :
      A ⊗[A] N)
    ((((curry ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f) : A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
              (a : A) → M →ₗ[R] A ⊗[A] N)
            1 :
          (a : M) → A ⊗[A] N)
        x :
      A ⊗[A] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
rw : ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f).ker = f.ker
rw₁ : Submodule.comap f (LinearMap.ker (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N)) = f.ker
rw₂ : Submodule.comap f ⊥ = f.ker
rw₃ rw₄ : f.ker = f.ker
⊢ LinearMap.ker
      (LinearMap.baseChange A f ∘ₗ
        (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) =
    f.ker

Tactic:
rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
    LinearEquiv.ker, Submodule.comap_bot]

Premises used: LinearMap.ker_comp, TensorProduct.AlgebraTensorModule.baseChange_comp_cancelBaseChange_symm_self, LinearEquiv.ker, Submodule.comap_bot
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst_6 : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j : κ, a i j • y j
ham : ∀ (j : κ), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (i : ι),
    n i =
      ∑ j : Fin (Fintype.card κ),
        HSMul.hSMul.{u_1, u_3, u_3} (α := R)
          ((fun (x : ι) ↦ (a x ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ) : Fin (Fintype.card κ) → R)) i j)
          ((y ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ)) j)

Tactic:
simpa only [← e.sum_comp] using hay

Premises used: Equiv.sum_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst_6 : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j : κ, a i j • y j
ham : ∀ (j : κ), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
e : Fin (Fintype.card κ) ≃ κ
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (ham :
      ∀ (a_1 : Fin (Fintype.card κ)),
        Eq.{u_2 + 1} (α := M) (∑ i : ι, a i ((e : (a : Fin (Fintype.card κ)) → κ) a_1) • m i) 0)
    (j : Fin (Fintype.card κ)),
    Eq.{u_2 + 1} (α := M)
      (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          ((fun (x : ι) ↦ (a x ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ) : Fin (Fintype.card κ) → R)) i j) (m i))
      0
⊢ ∀ (j : Fin (Fintype.card κ)),
    Eq.{u_2 + 1} (α := M)
      (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          ((fun (x : ι) ↦ (a x ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ) : Fin (Fintype.card κ) → R)) i j) (m i))
      0

Tactic:
rwa [← e.forall_congr_right] at ham

Premises used: Equiv.forall_congr_right
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst_6 : Fintype κ
e : κ ≃ ι
⊢ VanishesTrivially.{u_1, u_2, u_3, u_5} R (ι := κ) (m ∘ (⇑e : (a : κ) → ι)) (n ∘ (⇑e : (a : κ) → ι)) ↔
    VanishesTrivially R m n

Tactic:
simp [VanishesTrivially, ← e.forall_congr_right,
    ← (e.arrowCongr (.refl _)).exists_congr_right, ← e.sum_comp]

Premises used: Equiv.exists_congr_right, Equiv.sum_comp, Equiv.arrowCongr, TensorProduct.VanishesTrivially, Equiv.forall_congr_right, Equiv.refl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hmn : VanishesTrivially R m n
obtain :
  ∀ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N) (h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j)
    (h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0), Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
⊢ Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0

Tactic:
obtain ⟨k, a, y, h₁, h₂⟩ := hmn
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : ι, ∑ x_1 : Fin k, HSMul.hSMul (β := M ⊗[R] N) (a x x_1) (m x ⊗ₜ[R] y x_1)) 0
⊢ Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0

Tactic:
simp_rw [h₁, tmul_sum, tmul_smul]

Premises used: TensorProduct.tmul_smul, TensorProduct.tmul_sum
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
rw : Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
⊢ Eq (α := M ⊗[R] N) (∑ x : ι, ∑ x_1 : Fin k, HSMul.hSMul (β := M ⊗[R] N) (a x x_1) (m x ⊗ₜ[R] y x_1)) 0

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
simp_rw₁ : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, (a x_1 x • m x_1) ⊗ₜ[R] y x) 0
simp_rw₂ : Eq (α := M ⊗[R] N) (∑ x : Fin k, (∑ a_1 : ι, a a_1 x • m a_1) ⊗ₜ[R] y x) 0
simp_rw₃ : Eq (α := M ⊗[R] N) (∑ x : Fin k, 0 ⊗ₜ[R] y x) 0
simp_rw₄ : Eq (α := M ⊗[R] N) (∑ x : Fin k, 0) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0

Tactic:
simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_smul, TensorProduct.zero_tmul, Finset.sum_const_zero, TensorProduct.sum_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
⊢ let G : (ι →₀ R) →ₗ[R] M := linearCombination R m;
  G = linearCombination R m

Tactic:
set G : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R m with hG

Premises used: Finsupp.linearCombination, Finsupp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
i : ι
⊢ (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i

Tactic:
simp [hG]