mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.span pres.Ring (⇑(Submodule.subtype pres.ker) '' Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = pres.ker

Tactic:
Submodule.coe_subtype,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.span pres.Ring (Subtype.val '' Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = pres.ker
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
hf : Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r (presB.π (Finsupp.single g a)) + Finsupp.single r (presB.π f) ∈
    Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
refine Submodule.add_mem _ ?_ hf

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
hf : Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r (presB.π (Finsupp.single g a)) ∈
    Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: 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) ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) = 0
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0

Tactic:
erw [Finsupp.linearCombination_embDomain] at this

Goal state after:
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
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial.isTrue
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 (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
h✝ : a = 0
⊢ 0 = if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

Tactic:
simp only [*, map_zero, ite_self]

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

Goal state before:
pp: 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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
⊢ VanishesTrivially R (fun i ↦ (↑i).1) fun i ↦ (↑i).2

Tactic:
have e := (Fintype.equivFin s).symm

Goal state after:
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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
e : Fin (Fintype.card ↥s) ≃ ↥s
⊢ VanishesTrivially R (fun i ↦ (↑i).1) fun i ↦ (↑i).2
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal

Tactic:
simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : p ∈ support R M
⊢ q ∈ support R M

Tactic:
Module.mem_support_iff_exists_annihilator

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
⊢ ∃ m, (R ∙ m).annihilator ≤ q.asIdeal
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
x : N
hs' : x ∈ Submodule.span R' ↑(insert a s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(insert a s)

Tactic:
simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]

Goal state after:
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) = localized' R' S f (span R s)

Tactic:
localized'_span

Goal state after:
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)
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:
· let := Classical.decEq ι₁; simp

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 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:
let := Classical.decEq ι₂; 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₁)
⊢ ((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:
· let := Classical.decEq ι₁; simp

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.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:
let := Classical.decEq ι₂; 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
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
⊢ ((toTensorPower R M n).dualMap.compMultilinearMap (TensorPower.multilinearMapToDual R M n)).toFun f = 0

Tactic:
ext v
    suffices Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) = 0 by
      simpa [Matrix.det_apply] using this
    exact Matrix.det_zero_of_column_eq hij (by simp [hf])

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:
rw [injective_iff_map_eq_zero]

Goal state after:
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₁)
⊢ ∀ (a : M₃ ⊗[R] N₁), (LinearMap.lTensor M₃ g₁) a = 0 → a = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: case h
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)
i : I
⊢ v i = (⇑W.subtype ∘ ⇑(Basis.span hv)) i

Tactic:
Submodule.coe_subtype,

Goal state after:
case h
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)
i : I
⊢ v i = (Subtype.val ∘ ⇑(Basis.span hv)) i
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 rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]

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
hi : Surjective ⇑i
this✝ : Module.Finite R ↥i.ker
this : Surjective ⇑(LinearMap.baseChange k i)
⊢ finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0

Tactic:
simp only [Module.finrank_tensorProduct, Module.finrank_self,
        Module.finrank_finsupp_self, one_mul, add_zero]

Goal state after:
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
this : Surjective ⇑(LinearMap.baseChange k i)
⊢ Fintype.card ι = finrank k (k ⊗[R] M)
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
ι : Type u_1
m : Basis ι R ↥M
H : Function.Injective ⇑(mulLeftMap N ⇑m)
⊢ M.LinearDisjoint N

Tactic:
by
  classical simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H
  exact ⟨H⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ a = b

Tactic:
refine gradedMonoid_eq_of_reindex_cast h ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a.snd = b.snd
Module: Mathlib.LinearAlgebra.LinearDisjoint

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

Tactic:
exact (H N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])

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

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

Tactic:
by
    rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]

Goal state after: