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

Goal state before:
pp: case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
← Module.Relations.range_map

Goal state after:
case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = pres.differentialsRelations.map.range
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 ι σ
⊢ pres.differentialsSolution.IsPresentation

Tactic:
by
  rw [Module.Relations.Solution.isPresentation_iff]
  constructor
  · rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]
    exact Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective
  · rw [← Module.Relations.range_map]
    exact Function.Exact.linearMap_ker_eq
      ((LinearMap.exact_iff_of_surjective_of_bijective_of_injective
      _ _ _ _ (hom₁ pres)
      pres.cotangentSpaceBasis.repr.symm.toLinearMap .id
      (comm₁₂ pres) (by simpa using comm₂₃ pres) (surjective_hom₁ pres)
        (LinearEquiv.bijective _) (Equiv.refl _).injective).2
        pres.toExtension.exact_cotangentComplex_toKaehler)

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

Goal state before:
pp: case hC
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : R
⊢ ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)).comp C) x =
    ((↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i))).comp C) x

pp: case hX
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : σ
⊢ (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) (X x) = ↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i)) (X x)

Tactic:
<;>

Goal state after:
case hC
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : R
⊢ ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)).comp C) x =
    ((↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i))).comp C) x

case hX
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : σ
⊢ (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) (X x) = ↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i)) (X x)
Module: Mathlib.RingTheory.Extension.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
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨r • s, ⋯⟩ = (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩

Tactic:
rw [smul_tmul]; rfl

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

Goal state before:
pp: case e'_3.inl
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₁ : ι'
⊢ (Finsupp.sumElim 0 f) (Sum.inl i₁) = (Finsupp.mapDomain Sum.inr f) (Sum.inl i₁)

pp: case e'_3.inr
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₂ : ι
⊢ (Finsupp.sumElim 0 f) (Sum.inr i₂) = (Finsupp.mapDomain Sum.inr f) (Sum.inr i₂)

Tactic:
<;>

Goal state after:
case e'_3.inl
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₁ : ι'
⊢ (Finsupp.sumElim 0 f) (Sum.inl i₁) = (Finsupp.mapDomain Sum.inr f) (Sum.inl i₁)

case e'_3.inr
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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₂ : ι
⊢ (Finsupp.sumElim 0 f) (Sum.inr i₂) = (Finsupp.mapDomain Sum.inr f) (Sum.inr i₂)
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: case add
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
m₁✝ m₂✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.add m₁✝ m₂✝)) = 0

pp: case smul
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
a✝ : A
m✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.smul a✝ m✝)) = 0

Tactic:
<;>

Goal state after:
case add
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
m₁✝ m₂✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.add m₁✝ m₂✝)) = 0

case smul
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
a✝ : A
m✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.smul a✝ m✝)) = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e'_5
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
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
j : (ι' →₀ ℕ) × (ι →₀ ℕ)
hi : j.1 ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
hj : j ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = j.1}
⊢ (monomial (e.symm j)) (coeff (e.symm j) x) =
    (monomial (e.symm (j.1, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial j.2) (coeff (e.symm j) x))

Tactic:
obtain ⟨i, j⟩ := j

Goal state after:
case e'_5
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
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
hi : (i, j).1 ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
hj : (i, j) ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = (i, j).1}
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) =
    (monomial (e.symm ((i, j).1, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom ((monomial (i, j).2) (coeff (e.symm (i, j)) x))
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
set G : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R m with hG

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
⊢ VanishesTrivially R m n
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
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
⊢ 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom ↑x) = P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))

Tactic:
Cotangent.map_mk,

Goal state after:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
⊢ 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom ↑x) = P'.cotangentComplex (Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case refine_2
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
⊢ ((↑x).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) ∈ (Q.comp P).ker

Tactic:
simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]
    conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
    simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val,
      Sum.elim_inr, aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Sum.elim_inl, one_mul]
    congr! with v i
    simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

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
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (∑ i, a' (f i • Finsupp.single i 1)) j = 0

Tactic:
← map_sum,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (a' (∑ x, f x • Finsupp.single x 1)) j = 0
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
⊢ IsLocalizedModule.mk' (f r) x 1 ∈ Submodule.span (Rₚ r) ↑(s₁ r)

Tactic:
rw [s₂ r]

Goal state after:
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
⊢ IsLocalizedModule.mk' (f r) x 1 ∈ ⊤
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ (-1) ^ (↑(i.succAbove j) + ↑(j.predAbove i)) = (-1) ^ (↑i + ↑j + 1)

Tactic:
neg_one_pow_congr

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ (-1) ^ ?m.59 = (-1) ^ (↑i + ↑j + 1)

n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Even ?m.59

n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ ℕ
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case pos
n : ℕ
l : Fin (n + n)
h : n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l - (n + n))

pp: case neg
n : ℕ
l : Fin (n + n)
h : ¬n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l)

Tactic:
<;>

Goal state after:
case pos
n : ℕ
l : Fin (n + n)
h : n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l - (n + n))

case neg
n : ℕ
l : Fin (n + n)
h : ¬n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l)
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: 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 : ι₁ ⊕ ι₂) (c : R) (x : N i),
    ((a fun i₁ ↦ Function.update m i (c • x) (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i (c • x) (Sum.inr i₂)) =
      c • (a fun i₁ ↦ Function.update m i x (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i x (Sum.inr i₂)

Tactic:
rintro _ m (i₁ | i₂) p q

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₂)

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.Alternating.Uncurry.Fin

Goal state before:
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.ExteriorPower.Basis

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

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

Tactic:
<;>

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

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