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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x✝ : (Q.comp P).Ring
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : (Q.comp P).Ring
⊢ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ ⊆
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

Tactic:
intro j

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x✝ : (Q.comp P).Ring
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : (Q.comp P).Ring
j : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    j ∈ (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: case e'_7
A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
this : (Finsupp.linearCombination A (s.var ∘ ⇑(Function.Embedding.sectL relations₁.G g₂))) (relations₁.relation r₁) = 0
g₁ : relations₁.G
⊢ (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
        h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
      g₁ =
    (s.var ∘ ⇑(Function.Embedding.sectL relations₁.G g₂)) g₁

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ cotangentComplexBaseChange R S P.Ring A =
    ↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
            LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv)

Tactic:
by
  ext x
  simp [LinearEquiv.baseChange, cotangentComplexBaseChange_tmul]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
a✝ : P.Ring
⊢ (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P))) 1).compDer (D R P.Ring)) a✝ =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R P.Ring)) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.H1Cotangent
⊢ (↑((map (Hom.id P)) x✝)).val = (↑(LinearMap.id x✝)).val

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
i✝ : S
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ)) (X i✝) =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).Ring S)) (X i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
x : P.toExtension.Ring
i : ι
⊢ (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (D R P.toExtension.Ring) x)) i = (aeval P.val) ((pderiv i) x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
⊢ Surjective ⇑(LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1)

Tactic:
have := rTensor_surjective M (pi_mkQ_surjective hI)
  classical rw [pi_mkQ_rTensor] at this
  simpa using this

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

Goal state before:
pp: case e'_1
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card ↥s)), (fun i ↦ (↑(e i)).2) i = ∑ j, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i, a i j • (fun i ↦ ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card ↥s) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i, x✝¹ i a✝ • (fun i ↦ ↑(↑(e i)).1) i = M'.subtype (∑ i, x✝¹ i a✝ • ((fun i ↦ (↑i).1) ∘ ⇑e) i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
i : ι
⊢ 1 • (KaehlerDifferential.map R R P.toExtension.Ring S) ((D R P.Ring) (X i)) = (D R S) (P.val i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
r : R
hr : r ∈ ⨅ i, I i
m : M
x✝ : m ∈ ⊤
⊢ r ∈ (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker

pp: case e'_3.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range ≤ (⨅ i, I i) • ⊤

Tactic:
· simpa only [ker_pi, Submodule.ker_mkQ]

Goal state after:
case e'_3.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range ≤ (⨅ i, I i) • ⊤
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) 0 ∈ (⨅ i, I i) • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.QuotSMulTop

Goal state before:
pp: R : Type ?u.3
inst✝⁶ : CommRing R
r : R
M : Type u_1
M' : Type ?u.14
M'' : Type ?u.19
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
e : M' ≃ₗ[R] M''
⊢ r • Submodule.map ↑e ⊤ = r • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
      exact ⟨1, one_mem _, by simpa using h⟩

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Even (2 * ↑l)

Tactic:
simp

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
⊢ ⊤.spanFinrank = N.spanFinrank

Tactic:
by
  let : Module.Finite R N := Module.Finite.iff_fg.mpr fg
  apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm
  obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank
  have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top)
  let t := Function.surjInv (mk_surjective R N 𝓀 residue_surjective) '' s
  have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id]
  have ht₂ : span R t = ⊤ := by
    rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
  grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank,
    ← hs₁, Set.ncard_image_le hs₃]
  rfl

Goal state after:
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✝)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ ((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₂)

Tactic:
simp

Goal state after:
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✝)
this : DecidableEq ι₂ := Classical.decEq ι₂
⊢ ((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:
simp

Goal state after:
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₁)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ ((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₂)

Tactic:
simp

Goal state after:
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₂)
this : DecidableEq ι₂ := Classical.decEq ι₂
⊢ ((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:
simp

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:
simp

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

Tactic:
simp

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
⊢ ∀ (i : Fin n), (Finsupp.single ((ofFinEmbEquiv.symm t) i) 1) ((ofFinEmbEquiv.symm s) k) = 0

Tactic:
intro j

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
⊢ (Finsupp.single ((ofFinEmbEquiv.symm t) j) 1) ((ofFinEmbEquiv.symm s) k) = 0
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₂ 0) x = (LinearMap.rTensor N₃ f₁) 0

Tactic:
simp

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₁)
z : M₁ ⊗[R] N₁
this✝ : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) ((LinearMap.rTensor N₁ f₁) z)) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)) = 0
hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)
⊢ (LinearMap.rTensor N₁ 0) z = 0

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] (algebraMap R ↥⊥) x) =
    ↑M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) x)

Tactic:
simp

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
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) ((algebraMap R ↥⊥) x ⊗ₜ[R] m) =
    ↑M.lTensorOne ((algebraMap R ↥⊥) x ⊗ₜ[R] m)

Tactic:
simp

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
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
a✝ : ι
x✝ : ↥N
⊢ (mulLeftMap N m ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝

Tactic:
simp

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
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
a✝ : ι
x✝ : ↥M
⊢ (M.mulRightMap n ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
            ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝

Tactic:
simp

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

Goal state before:
pp: case e_6.left
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin na), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.castAdd nb i)) = Fin.addCases a b (Fin.castAdd nb i)

Tactic:
simp

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

Goal state before:
pp: case e_6.right
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin nb), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.natAdd na i)) = Fin.addCases a b (Fin.natAdd na i)

Tactic:
simp

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

Goal state before:
pp: case smul_tprod.e_a.e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ i)) = ↑i

Tactic:
simp

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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
⊢ x ∈ {x, y}

Tactic:
simp

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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ y ∈ {x, y}

Tactic:
simp

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

Goal state before:
pp: case h
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) := ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := ⋯
i : (ι →₀ R) →ₗ[R] M := ⋯
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := ⋯
⊢ ∀ (i : ι), { repr := iequiv.symm } i = v i

Tactic:
intro j

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
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
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
j : ι
⊢ { repr := iequiv.symm } j = v j