mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ I * K ≤ I * ⨅ i, J i

Tactic:
le_iInf (a := K) fun i ↦ ?_

Goal state after:
case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ I * iInf ?m.119 ≤ I * ⨅ i, J i

A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ Sort ?u.69

A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ ?m.117 → Ideal A

A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ?m.117
⊢ K ≤ ?m.119 i
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
s : Finset κ
g : κ → R
hs : ∑ i ∈ s, g i • ↑(b i) = 0
⊢ ∀ i ∈ s, g i = 0

Tactic:
← Submodule.coe_smul_of_tower,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
s : Finset κ
g : κ → R
hs : ∑ x ∈ s, ↑(g x • b x) = 0
⊢ ∀ i ∈ s, g i = 0
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
h_minus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_eq : i = j
⊢ Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0

Tactic:
by rw [← hi, ← hj, h_eq, sub_self]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : u ≈ v
⊢ u' ∘ₗ u ≈ u' ∘ₗ v

Tactic:
by
  rw [equiv_iff_hasNoetherianRange] at *
  simpa only [LinearMap.comp_sub] using h.comp_left u'

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ IsNoetherian K ↥(S.projection T hST).range ↔ IsNoetherian K ↥S

Tactic:
range_projection

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ IsNoetherian K ↥S ↔ IsNoetherian K ↥S
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ IsNoetherian K ↥(T.projection S ⋯).range ↔ IsNoetherian K ↥T

Tactic:
range_projection

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ IsNoetherian K ↥T ↔ IsNoetherian K ↥T
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
j : ↑{M | M ∈ normalizedFactors J}
⊢ ↑((idealFactorsEquivOfQuotEquiv f).symm ⟨↑j, ⋯⟩) ∈ {L | L ∈ normalizedFactors I}

Tactic:
rw [idealFactorsEquivOfQuotEquiv_symm]
      exact
        idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI
          j.prop

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (s.inf fun i ↦ f i ^ e i) = ∏ i ∈ s, f i ^ e i

Tactic:
by
  rw [prod_eq_iInf_of_pairwise_isCoprime, Finset.inf_eq_iInf s fun i ↦ (f i) ^ e i]
  intro i hi j hj hij
  exact Ideal.isCoprime_iff_sup_eq.mpr (pow_sup_pow_eq_top (IsMaximal.coprime_of_ne
    (IsPrime.isMaximal (isPrime_of_prime (prime i hi)) (prime i hi).ne_zero)
    (IsPrime.isMaximal (isPrime_of_prime (prime j hj)) (prime j hj).ne_zero)
    (coprime i hi j hj hij)))

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : x * x ∣ a
⊢ IsUnit x

Tactic:
rw [← span_singleton_dvd_span_singleton_iff_dvd, ← span_singleton_mul_span_singleton] at hx
    simpa using h _ hx

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

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
this : p.IsPrime
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Tactic:
exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ (f ∘ₗ (π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm) ∘ₗ π) x =
    (f ∘ₗ (s₁ • linearCombination R i)) x

Tactic:
LinearMap.comp_assoc

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ (f ∘ₗ π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm ∘ₗ π) x =
    (f ∘ₗ (s₁ • linearCombination R i)) x
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ ((↑f ∘ₗ (R ∙ s j).mkQ) ∘ₗ
      DirectSum.toModule R (Fin d) M fun i ↦ liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R M ⋯.choose) ⋯) =
    LinearMap.id

Tactic:
LinearMap.comp_assoc

Goal state after:
case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ (↑f ∘ₗ
      (R ∙ s j).mkQ ∘ₗ
        DirectSum.toModule R (Fin d) M fun i ↦
          liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R M ⋯.choose) ⋯) =
    LinearMap.id
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = m i • (monomial m) r

Tactic:
smul_monomial

Goal state after:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case mul_X
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
p : MvPolynomial ι' S
i : ι'
h : ∃ a, (Q.aux P) a = p
⊢ ∃ a, (Q.aux P) a = p * X i

Tactic:
| mul_X p i h =>

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
⊢ (invtSubmoduleToLieIdeal (↑q) hq).toInvtRootSubmodule = q

Tactic:
simp only [Subtype.ext_iff, LieIdeal.toInvtRootSubmodule, LieIdeal.rootSpan, LieIdeal.rootSet]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
⊢ Submodule.span K
      (⇑(rootSystem H).root '' {α | rootSpace H ⇑↑α ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q) hq) H}) =
    ↑q
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
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
x : ↥P'.ker
y : P.Ring
y_in : y ∈ P.ker
hy : f.toRingHom y = ↑x
⊢ (map f) (mk ⟨y, y_in⟩) = mk x

Tactic:
simp [hy]

Goal state after:
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₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ Submodule.map Extension.Cotangent.mk (Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩)) ≤ φ.range

Tactic:
Submodule.map_span_le

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₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
⊢ ∀ m ∈ Set.range fun r ↦ ⟨pres.relation r, ⋯⟩, Extension.Cotangent.mk m ∈ φ.range
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) = 0

Tactic:
rw [← s.linearCombination_var_relation ⟨i, r⟩]

Goal state after:
A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) =
    (Finsupp.linearCombination A s.var) ((directSum relations).relation ⟨i, r⟩)
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
pres : Presentation A M
left✝ : Finite pres.G
right✝ : Finite pres.R
⊢ FinitePresentation A M

Tactic:
exact pres.finitePresentation

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

Goal state before:
pp: case a.convert_4.monomial
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 : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ ∑ a_1 ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with a_1.1 = i,
      (aeval P.val) ((monomial a_1.2) (coeff (e.symm a_1) ((monomial (e.symm v)) a))) =
    coeff i ((monomial v.1) ((aeval P.val) ((monomial v.2) a)))

Tactic:
simp only [coeff_monomial, ← e.injective.eq_iff,
          map_zero, AddEquiv.apply_symm_apply, apply_ite]

Goal state after:
case a.convert_4.monomial
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 : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ if v.1 = i then
    (∑ x ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with x.1 = i,
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      (aeval P.val) ((monomial v.2) a)
  else
    (∑ x ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with x.1 = i,
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      0
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
⊢ (CotangentSpace.map f) (1 ⊗ₜ[P.Ring] (D R P.Ring) ↑x) = P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))

Tactic:
map_tmul,

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
⊢ (algebraMap S S') 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom ↑x) =
    P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ (mk ⟨f.toAlgHom ↑x, ⋯⟩ - mk ⟨g.toAlgHom ↑x, ⋯⟩).val = P'.ker.toCotangent ((f.subToKer g) ↑x)

Tactic:
apply (Ideal.cotangentEquivIdeal _).injective

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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ P'.ker.cotangentEquivIdeal (mk ⟨f.toAlgHom ↑x, ⋯⟩ - mk ⟨g.toAlgHom ↑x, ⋯⟩).val =
    P'.ker.cotangentEquivIdeal (P'.ker.toCotangent ((f.subToKer g) ↑x))
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'
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''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ P'.cotangentComplex ((Cotangent.map f) x) = 0

Tactic:
rw [hx]

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'
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''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ (CotangentSpace.map f) 0 = 0
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'
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''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
⊢ map (g.comp f) = ↑S (map g) ∘ₗ map f

Tactic:
by
  ext; simp [Cotangent.map_comp]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = (Algebra.linearMap S S') (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ a • x' = ↑⟨(algebraMap R S) a, ⋯⟩ * x'

Tactic:
· exact Algebra.smul_def _ _

Goal state after: