mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ annihilator R M

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∉ p.asIdeal

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ annihilator R M
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∉ p.asIdeal

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∉ p.asIdeal
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ support R M ∩ zeroLocus ↑I

pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R M ∩ zeroLocus ↑I ⊆ support R (M ⧸ I • ⊤)

Tactic:
·

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ support R M ∩ zeroLocus ↑I
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ support R M

pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ zeroLocus ↑I

Tactic:
·

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ support R M
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ zeroLocus ↑I

Tactic:
·

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ zeroLocus ↑I
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R M ∩ zeroLocus ↑I ⊆ support R (M ⧸ I • ⊤)

Tactic:
·

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R M ∩ zeroLocus ↑I ⊆ support R (M ⧸ I • ⊤)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
hij : i ≤ j.castSucc
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

Tactic:
·

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
hij : i ≤ j.castSucc
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

Tactic:
·

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
hij : i ≤ j.castSucc
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inl
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even ↑k
⊢ Even k

pp: case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k

Tactic:
·

Goal state after:
case inl
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even ↑k
⊢ Even k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Even ↑k
⊢ Odd k

pp: case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k

Tactic:
·

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Even ↑k
⊢ Odd k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k

Tactic:
·

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: case e'_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s) =
    Cardinal.lift.{u_3, max u_2 u_3} (Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s))

pp: case e'_4
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s) =
    Cardinal.lift.{u_3, max u_2 u_3} (Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s))
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: case e'_4
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}

Tactic:
·

Goal state after:
case e'_4
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₁
x✝ y✝ : N (Sum.inl val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inr i₂)

pp: case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₂
x✝ y✝ : N (Sum.inr val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inr i₂)

Tactic:
·

Goal state after:
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₁
x✝ y✝ : N (Sum.inl val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inr i₂)
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₂
x✝ y✝ : N (Sum.inr val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inr i₂)

Tactic:
·

Goal state after:
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₂
x✝ y✝ : N (Sum.inr val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inr val✝) y✝ (Sum.inr i₂)
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₁ : ι₁
p : R
q : N (Sum.inl i₁)
⊢ ((a fun i₁_1 ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inl i₁_1)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inr i₂)) =
    p •
      (a fun i₁_1 ↦ Function.update m (Sum.inl i₁) q (Sum.inl i₁_1)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m (Sum.inl i₁) q (Sum.inr i₂)

pp: case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₂ : ι₂
p : R
q : N (Sum.inr i₂)
⊢ ((a fun i₁ ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂_1 ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inr i₂_1)) =
    p •
      (a fun i₁ ↦ Function.update m (Sum.inr i₂) q (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂_1 ↦ Function.update m (Sum.inr i₂) q (Sum.inr i₂_1)

Tactic:
·

Goal state after:
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₁ : ι₁
p : R
q : N (Sum.inl i₁)
⊢ ((a fun i₁_1 ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inl i₁_1)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inr i₂)) =
    p •
      (a fun i₁_1 ↦ Function.update m (Sum.inl i₁) q (Sum.inl i₁_1)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m (Sum.inl i₁) q (Sum.inr i₂)
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₂ : ι₂
p : R
q : N (Sum.inr i₂)
⊢ ((a fun i₁ ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂_1 ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inr i₂_1)) =
    p •
      (a fun i₁ ↦ Function.update m (Sum.inr i₂) q (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂_1 ↦ Function.update m (Sum.inr i₂) q (Sum.inr i₂_1)

Tactic:
·

Goal state after:
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₂ : ι₂
p : R
q : N (Sum.inr i₂)
⊢ ((a fun i₁ ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂_1 ↦ Function.update m (Sum.inr i₂) (p • q) (Sum.inr i₂_1)) =
    p •
      (a fun i₁ ↦ Function.update m (Sum.inr i₂) q (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂_1 ↦ Function.update m (Sum.inr i₂) q (Sum.inr i₂_1)
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j
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
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ ((alternatingMapToDual R M n) f) ((ιMulti R n) v) = (Matrix.of fun i j ↦ (f j) (v i)).det

Tactic:
simp [alternatingMapToDual, Matrix.det_apply]

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

Goal state before:
pp: case pos
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
⊢ (f (a j)) (x (a i)) = 1 i j

pp: case neg
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
⊢ (f (a j)) (x (a i)) = 1 i j

Tactic:
·

Goal state after:
case pos
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
⊢ (f (a j)) (x (a i)) = 1 i j
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: case neg
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
⊢ (f (a j)) (x (a i)) = 1 i j

Tactic:
·

Goal state after:
case neg
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
⊢ (f (a j)) (x (a i)) = 1 i j
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
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₂

pp: case mpr
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
⊢ N₁ = N₂ → Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂

Tactic:
·

Goal state after:
case mp
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₂
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mpr
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
⊢ N₁ = N₂ → Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂

Tactic:
·

Goal state after:
case mpr
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
⊢ N₁ = N₂ → Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
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 = ⊤

pp: case mpr
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
⊢ N = ⊤ → Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤

Tactic:
·

Goal state after:
case mp
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 = ⊤