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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Submodule R M
R' : Type u_1
inst✝⁷ : CommSemiring R'
inst✝⁶ : Algebra R R'
M' : Type u_2
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Module R' M'
inst✝² : IsScalarTower R R' M'
S : Submonoid R
inst✝¹ : IsLocalization S R'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
⊢ span R' (⇑f '' s) = span R' (⇑f '' s)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd ↑k

Tactic:
]

Goal state after:
n : ℕ
k : Fin n
inst✝ : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd ↑k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
hn : Even n
⊢ Even ↑k ↔ ↑k % 2 = 0

Tactic:
]

Goal state after:
n : ℕ
k : Fin n
hn : Even n
⊢ Even ↑k ↔ ↑k % 2 = 0
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ Odd ↑k ↔ ↑k % 2 = 1

Tactic:
]

Goal state after:
n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ Odd ↑k ↔ ↑k % 2 = 1
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (ker (IsLocalization.map (Localization.Away (f ↑g)) f ⋯)).FG

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (ker (IsLocalization.map (Localization.Away (f ↑g)) f ⋯)).FG
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ ¬Odd ↑k ↔ Even ↑k

Tactic:
]

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

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ ¬Even ↑k ↔ Odd ↑k

Tactic:
]

Goal state after:
n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ ¬Even ↑k ↔ Odd ↑k
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: 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_2, u_3} (Cardinal.mk ↑s)

Tactic:
]

Goal state after:
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_2, u_3} (Cardinal.mk ↑s)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: 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
fg : N.FG
⊢ Cardinal.toNat N.spanRank ≤ Cardinal.toNat N.spanRank

pp: case hd
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
fg : N.FG
⊢ Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0

Tactic:
]

Goal state after:
case hd
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
fg : N.FG
⊢ Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: 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
⊢ Cardinal.lift.{u_2, u_3} ⊤.spanRank ≤ Cardinal.lift.{u_2, u_3} ⊤.spanRank

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: 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
fg : N.FG
⊢ ⊤.spanFinrank ≤ ⊤.spanFinrank

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
hs₂ : span R t = ⊤
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
hs₂ : span R t = ⊤
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Equiv.Perm.sign p.cycleRange • f (cons x v) = (-1) ^ ↑p • f (cons x v)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Equiv.Perm.sign p.cycleRange • f (cons x v) = (-1) ^ ↑p • f (cons x v)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
ht₂ : span R t = ⊤
⊢ s.ncard ≤ Cardinal.toNat (Cardinal.mk ↑s)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
ht₂ : span R t = ⊤
⊢ s.ncard ≤ Cardinal.toNat (Cardinal.mk ↑s)
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ f (Matrix.vecCons x v) = f (Matrix.vecCons x v)

pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Even (↑p + ↑p)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Even (↑p + ↑p)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N : Submodule R M
fg : N.FG
this✝ : Module 𝓀 (↥N ⧸ maximalIdeal R • ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R 𝓀 (↥N ⧸ maximalIdeal R • ⊤) := spanFinrank_eq_finrank_quotient._proof_1_7 N
⊢ Module.finrank 𝓀 (𝓀 ⊗[R] ↥N) = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N : Submodule R M
fg : N.FG
this✝ : Module 𝓀 (↥N ⧸ maximalIdeal R • ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R 𝓀 (↥N ⧸ maximalIdeal R • ⊤) := spanFinrank_eq_finrank_quotient._proof_1_7 N
⊢ Module.finrank 𝓀 (𝓀 ⊗[R] ↥N) = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ 0 = 0

pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
k : Fin (n + 1)
i : Fin n
hki : k ≠ k.succAbove i
j : Fin n
hkj : k ≠ k.succAbove j
hvij : v (k.succAbove i) = v (k.succAbove j)
hij : k.succAbove i ≠ k.succAbove j
x✝ : k ≠ k.succAbove i ∧ k ≠ k.succAbove j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ 0 = 0

pp: case hvij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ v i = v j

pp: case hij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ i ≠ j

Tactic:
]

Goal state after:
case hvij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ v i = v j

case hij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ i ≠ j
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: case e_a.e_a.e_a.e_6
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth v j = v j.succ
H₂ : j.succ.removeNth v i = v i.castSucc
⊢ (i.predAbove j.succ).removeNth ((j.succ.succAbove i).removeNth v) = j.removeNth (i.castSucc.removeNth v)

Tactic:
]

Goal state after:
case e_a.e_a.e_a.e_6
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth v j = v j.succ
H₂ : j.succ.removeNth v i = v i.castSucc
⊢ (i.predAbove j.succ).removeNth ((j.succ.succAbove i).removeNth v) = j.removeNth (i.castSucc.removeNth v)
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 ι
⊢ (Matrix.of fun i j ↦ (f (a j)) (x (a i))).det = Matrix.det 1

Tactic:
]

Goal state after:
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 ι
⊢ (Matrix.of fun i j ↦ (f (a j)) (x (a i))).det = Matrix.det 1
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
⊢ 0 = 0

Tactic:
]

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 : a i ≤ a j
h'' : ∀ (a_1 : Fin n), a a_1 = b (σ a_1)
⊢ σ i ≤ σ j

Tactic:
]

Goal state after:
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 : a i ≤ a j
h'' : ∀ (a_1 : Fin n), a a_1 = b (σ a_1)
⊢ σ i ≤ σ j
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:
simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge

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
⊢ (Submodule.map (ExteriorAlgebra.ι R) ⊤ ^ n).FG

Tactic:
]

Goal state after:
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
⊢ (Submodule.map (ExteriorAlgebra.ι R) ⊤ ^ n).FG
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
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ N₁ = 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
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ N₁ = N₂
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)
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm s)) i)).det = 1

Tactic:
]

Goal state after:
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)
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm s)) i)).det = 1
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₂
⊢ 𝔪 ≤ 𝔪

pp: case h
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₂
⊢ ⊥ ≠ ⊤

Tactic:
]

Goal state after:
case h
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₂
⊢ ⊥ ≠ ⊤
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
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm t)) i)).det = 0

Tactic:
]

Goal state after:
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
⊢ (Matrix.of fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm t)) i)).det = 0
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 = ⊤ ↔ Submodule.map (𝔪 • ⊤).mkQ N = ⊤

Tactic:
]

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
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ False

Tactic:
apply hit

Goal state after:
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
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ (ofFinEmbEquiv.symm s) k ∈ t
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
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ ((↑t).orderEmbOfFin ⋯) j ∈ ↑t

Tactic:
]

Goal state after:
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
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ ((↑t).orderEmbOfFin ⋯) j ∈ ↑t
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)
⊢ ιMulti_family R n (⇑b) s = ιMulti_family R n (⇑b) s

Tactic:
]

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)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) s = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)

Tactic:
]

Goal state after:
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)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) t)) s = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)