mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r r' : R₁
x✝ x y : ⨂[R] (i : ι), s i
ihx : (r * r') • x = r • r' • x
ihy : (r * r') • y = r • r' • y
⊢ (r * r') • (x + y) = r • r' • (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ 1 • tprodCoeff R r f = tprodCoeff R r f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : 1 • z = z
ihy : 1 • y = y
⊢ 1 • (z + y) = z + y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ r' • r'' • tprodCoeff R xr xf = r'' • r' • tprodCoeff R xr xf

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ Submodule.span R (Set.range id) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ Free R M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.lTensor (↥M) (inclusion hN)).range
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ (M.mulMap N') x' = (M.mulMap N') y'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (z + y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁵ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁴ : (i : ι) → AddCommMonoid (s i)
inst✝¹³ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
E : Type u_9
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
F : Type u_10
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ (r' • r'') • tprodCoeff R xr xf = r' • r'' • tprodCoeff R xr xf

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁵ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁴ : (i : ι) → AddCommMonoid (s i)
inst✝¹³ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
E : Type u_9
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
F : Type u_10
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (z + y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
r✝ r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ (r✝ + r') • tprodCoeff R r f = r✝ • tprodCoeff R r f + r' • tprodCoeff R r f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n s
l : ℕ
a : ↥(insert n s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
⊢ v n ∉ 𝔪 • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ (mulLeftMap N m).ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
r r' : R₁
x✝ x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ (M.mulRightMap n).ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
⊢ ∃ j, IsUnit (a n j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ 0 • tprodCoeff R r f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i✝ : ι
hi : i✝ ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
i : ↥(insert n✝ s)
⊢ a i j = a' ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
x✝ x y : ⨂[R] (i : ι), s i
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 • (x + y) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
h : Function.Injective ⇑i
⊢ i = Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = r • tprodCoeff R 1 (update f i x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
⊢ z = z • 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
⊢ tprodCoeff R z f = z • (tprod R) f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑p = (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ p ∈ x.lifts ↔ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ x.lifts.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ 0 ∈ lifts 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ p + q ∈ (x + y).lifts

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
h : Function.Injective ⇑i
⊢ i = Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h : p ∈ x.lifts
a : R
⊢ (FreeAddMonoid.map fun y ↦ (a * y.1, y.2)) p ∈ (a • x).lifts

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (tprod R) f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)
⊢ M.LinearDisjoint N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective ⇑i
⊢ i = M'.mulMap N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z x y : ⨂[R] (i : ι), s i
hx : φ₁ x = φ₂ x
hy : φ₁ y = φ₂ y
⊢ φ₁ (x + y) = φ₂ (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
⊢ M'.LinearDisjoint N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective ⇑i
⊢ i = M.mulMap N'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
⊢ M.LinearDisjoint N'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
⊢ φ₁ = φ₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ (M.mulRightMap n) m = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
t : ⨂[R] (i : ι), s i
x✝¹ : R
x✝ : (i : ι) → s i
⊢ (tprod R) x✝ ∈ Set.range ⇑(tprod R)

Tactic:
by

Goal state after: