mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
⊢ a j ≠ a i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
⊢ ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑a)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
i : Fin n
hi : ¬a i = (⇑b ∘ ⇑σ) i
⊢ i ∈ Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
⊢ ⇑a = ⇑b ∘ ⇑σ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : i ≤ j
⊢ σ i ≤ σ j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i j : Fin n
hij : i ≤ j
⊢ (Equiv.symm σ) i ≤ (Equiv.symm σ) j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
hσ' : Monotone ⇑(Equiv.symm σ)
⊢ σ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
⊢ ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑b)) = 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
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
⊢ N₂ ≤ 𝔪 • N₂ ⊔ N₁

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup E
inst✝¹ : Module K E
inst✝ : Module.Finite R M
⊢ Module.Finite R ↥(⋀[R]^n M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
v : Fin n → M
⊢ (ιMultiDual R n b s) ((ιMulti R n) v) = (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (v i)).det

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
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ 𝔪 ≤ ⊥.jacobson

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
this : (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) (b ((ofFinEmbEquiv.symm s) i))) = 1
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm s)) i)).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (ιMultiDual R n b s) (ιMulti_family R n (⇑b) s) = 1

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
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
⊢ Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂ ↔ N₁ = N₂

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
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map (𝔪 • ⊤).mkQ N = ⊤ ↔ N = ⊤

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
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
⊢ f ∘ₗ (TensorProduct.mk R k M) 1 = (𝔪 • ⊤).mkQ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
hst : s ≠ t
⊢ (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Basis.exteriorPower n b) s = ιMulti_family R n (⇑b) s

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
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (TensorProduct.mk R k M) 1 = (𝔪 • ⊤).mkQ
⊢ Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Basis.exteriorPower n b).coord s = ιMultiDual R n b s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
x : ↥(⋀[R]^n M)
s : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr x) s = (ιMultiDual R n b s) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) s = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
hst : s ≠ t
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) t = 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
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤ ↔ N = ⊤

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✝ : Module.Finite R M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s) = Finsupp.single s 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup E
inst✝¹ : Module K E
inst✝ : Free R M
⊢ Free R ↥(⋀[R]^n M)

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✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span R (Set.range f) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n

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✝ : Module.Finite R M
p : PrimeSpectrum R
⊢ p ∈ support R M ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
this : ∃ b, v = ⇑W.subtype ∘ ⇑b
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
⊢ (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Skeleton

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
e : C ≌ D
inst✝ : F.Monoidal
hC : Skeletal C
hD : Skeletal D
⊢ let x := monoidOfSkeletalMonoidal hC;
  let x_1 := monoidOfSkeletalMonoidal hD;
  C →* D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Skeleton

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
e : C ≌ D
inst✝ : F.Monoidal
hC : Skeletal C
hD : Skeletal D
⊢ let x := monoidOfSkeletalMonoidal hC;
  let x_1 := monoidOfSkeletalMonoidal hD;
  C →* D

Tactic:
by
  intros; exact
  { toFun := F.obj
    map_one' := hD ⟨(Monoidal.εIso F).symm⟩
    map_mul' X Y := hD ⟨(Monoidal.μIso F X Y).symm⟩ }

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Skeleton

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
e : C ≌ D
inst✝ : e.functor.Monoidal
hC : Skeletal C
hD : Skeletal D
⊢ let x := monoidOfSkeletalMonoidal hC;
  let x_1 := monoidOfSkeletalMonoidal hD;
  C ≃* D

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.lTensor M₁ g₂) y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this✝ : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
z : M₁ ⊗[R] N₁
hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) x
this : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0
⊢ (LinearMap.rTensor N₁ f₁) z = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
⊢ Function.Injective ⇑(LinearMap.lTensor M₃ g₁)

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
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
⊢ (map (↑f) M).mulMap (map (↑f) N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N) = ↑f ∘ₗ M.mulMap N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
⊢ N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ (M.mulMap N).range = M * N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ Function.Surjective ⇑(M.mulMap' N)

Tactic:
mulMap',

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ Function.Surjective ⇑(↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) ⋯) ∘ₗ (M.mulMap N).rangeRestrict)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ Function.Surjective ⇑(M.mulMap' N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N).range = N

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
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
x✝ : ι
⊢ 1 ⊗ₜ[R] v x✝ = bk x✝

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
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Surjective ⇑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ↑(N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n)) = ↑(y • n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
n : ↥N
⊢ N.lTensorOne' (1 ⊗ₜ[R] n) = n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N) 1 = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
r : ↥⊥
n : ↥N
⊢ ((TensorProduct.mk R ↥⊥ ↥N) 1 ∘ₗ N.lTensorOne') (r ⊗ₜ[R] n) = LinearMap.id (r ⊗ₜ[R] n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)).range = M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ ↑(M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) = ↑(y • m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
⊢ M.rTensorOne' (m ⊗ₜ[R] 1) = m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

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
⊢ M.rTensorOne' ∘ₗ ↑(TensorProduct.comm R ↥⊥ ↥M) ∘ₗ (TensorProduct.mk R ↥⊥ ↥M) 1 = LinearMap.id

Tactic:
by

Goal state after: