mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ x = 1 * x

Tactic:
one_mul

Goal state after:
case refine_1.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ x = x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ 1 * y' ∈ I

Tactic:
one_mul

Goal state after:
case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ y' ∈ I
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom (x • y) = (RingHom.id A) x • (decomposeAddEquiv 𝓜).toAddHom y

Tactic:
← DirectSum.sum_support_decompose 𝓐 x,

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom ((∑ i ∈ DFinsupp.support ((decompose 𝓐) x), ↑(((decompose 𝓐) x) i)) • y) =
    (RingHom.id A) (∑ i ∈ DFinsupp.support ((decompose 𝓐) x), ↑(((decompose 𝓐) x) i)) • (decomposeAddEquiv 𝓜).toAddHom y
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_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
γ : Weight K (↥H) L :=
  { toFun := ⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α), genWeightSpace_ne_bot' := h_minus_ne_bot }
hγ_nonzero : γ.IsNonZero
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_sum_in_range : S.root i + S.root j ∈ Set.range ⇑S.root
h_equiv : Weight.toLinear K (↥H) L χ ∈ ↑⟨q, ⋯⟩ ↔ S.root j ∈ ↑⟨q, ⋯⟩
⊢ False

Tactic:
exact h_chi_not_in_q (h_equiv.mpr (by
      rw [hj, Weight.toLinear_neg]
      convert q.smul_mem (-1) hαq
      rw [neg_smul, one_smul]))

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ comap (Ideal.Quotient.mk L)
      (map g (map (Ideal.Quotient.mk J) (comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑x))))) =
    comap (Ideal.Quotient.mk L) (map (g.comp f) (map (Ideal.Quotient.mk I) ↑x))

Tactic:
map_comap_of_surjective (Ideal.Quotient.mk J)
    Ideal.Quotient.mk_surjective,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ comap (Ideal.Quotient.mk L) (map g (map f (map (Ideal.Quotient.mk I) ↑x))) =
    comap (Ideal.Quotient.mk L) (map (g.comp f) (map (Ideal.Quotient.mk I) ↑x))
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
r : R
h₁ : IsUnit ((algebraMap R (Module.End R N)) r)
h₂ : ∀ (x : N), ∃ n y, r ^ n • x = f y
h₃ : ∀ (x y : M), f x = f y → ∃ n, r ^ n • x = r ^ n • y
x y : M
hxy : f x = f y
⊢ ∃ c, c • x = c • y

Tactic:
obtain ⟨n, hn⟩ := h₃ _ _ hxy
    use ⟨_, n, rfl⟩, hn

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 ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (s.inf fun i ↦ (f i).asIdeal ^ e i) = ∏ i ∈ s, (f i).asIdeal ^ e i

Tactic:
prod_eq_iInf_of_pairwise_isCoprime

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (s.inf fun i ↦ (f i).asIdeal ^ e i) = ⨅ i ∈ s, (f i).asIdeal ^ e i

R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (↑s).Pairwise (Function.onFun IsCoprime fun i ↦ (f i).asIdeal ^ e i)
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : M'
hx : x ∈ ↑s
⊢ (fun x ↦ ↑(commonDenomOfFinset S f s) • x) x ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach

Tactic:
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s id _⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ↑(finsetIntegerMultiple S f s) = commonDenomOfFinset S f s • ↑s

Tactic:
by
  delta finsetIntegerMultiple commonDenom
  rw [Finset.coe_image]
  ext
  constructor
  · rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
    rw [map_integerMultiple]
    exact Set.mem_image_of_mem _ x.prop
  · rintro ⟨x, hx, rfl⟩
    exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s id _⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ p ^ k • (f1.choose - a • z) = 0

Tactic:
smul_sub,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ p ^ k • f1.choose - p ^ k • a • z = 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_bijective_map_powers S f g _ this

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case add
R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p q : MvPolynomial (σ ⊕ ι) R
a✝¹ : (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)
a✝ : (pderiv i) ((sumRingEquiv R σ ι) q) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) q)
⊢ (pderiv i) ((sumRingEquiv R σ ι) (p + q)) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) (p + q))

Tactic:
| add p q _ _ =>

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective ⇑(algebraMap R S)
⊢ (Generators.ofSurjectiveAlgebraMap ⋯).ker = ⊥

Tactic:
rw [← RingHom.injective_iff_ker_eq_bot]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective ⇑(algebraMap R S)
⊢ Function.Injective ⇑(algebraMap (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring S)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Presentation R S ι σ
r : R
inst✝ : IsLocalization.Away r S
⊢ Ideal.span (Set.range fun x ↦ C r * X () - 1) = (Generators.localizationAway S r).ker

Tactic:
simp only [Set.range_const]
    exact (Generators.ker_localizationAway r).symm

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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
α : ↥LieSubalgebra.root
⊢ α ∈ J.rootSet ↔ α ∈ I.rootSet

Tactic:
rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
    exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, rfl⟩⟩

Goal state after:
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:
obtain ⟨a, rfl⟩ := h

Goal state after:
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 ι σ
i : ι'
a : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ a_1, (Q.aux P) a_1 = (Q.aux P) a * X i
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: 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 ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ aeval (Q.comp P.toGenerators).val = (aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Q.aux P)

Tactic:
by
  ext i
  simp only [AlgHom.coe_comp, Function.comp_apply]
  cases i <;> simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: 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✝ f'✝ : M →ₗ[A] N✝
h : (tautologicalSolution A M).postcomp f✝ = (tautologicalSolution A M).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
by
    ext m
    exact Relations.Solution.congr_var h m

Goal state after:
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
i : ι' →₀ ℕ
j : ι →₀ ℕ
this :
  (Q.toComp P).toAlgHom ((monomial j) (coeff (e.symm (i, j)) x)) = (monomial (e.symm (0, j))) (coeff (e.symm (i, j)) x)
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) = (monomial (e.symm (i, j))) (1 * coeff (e.symm (i, j)) x)

Tactic:
one_mul

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 : ι →₀ ℕ
this :
  (Q.toComp P).toAlgHom ((monomial j) (coeff (e.symm (i, j)) x)) = (monomial (e.symm (0, j))) (coeff (e.symm (i, j)) x)
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) = (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case refine_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
ι : 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
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj

Tactic:
simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]

Goal state after:
case refine_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
ι : 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
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i = ∑ x ∈ ma, ↑x.1 i • x.2
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: 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
h₄ : ∀ {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
hfx : x f = 0
⊢ ∃ k a y, x = y ∘ₗ a ∧ a f = 0

Tactic:
let f' : Fin l → R := f
    let x' : Fin l → M := fun i ↦ x (single i 1)
    have := calc
      ∑ i, f' i • x' i
      _ = ∑ i, f i • x (single i 1) := rfl
      _ = x (∑ i, f i • Finsupp.single i 1) := by simp_rw [map_sum, map_smul]
      _ = x f := by simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
      _ = 0 := hfx
    obtain ⟨k, a', y', ⟨ha'y', ha'⟩⟩ := h₄ this
    use k
    use Finsupp.linearCombination R (fun i ↦ equivFunOnFinite.symm (a' i))
    use Finsupp.linearCombination R y'
    constructor
    · apply Finsupp.basisSingleOne.ext
      intro i
      simpa [linearCombination_apply, sum_fintype, Finsupp.single_apply] using ha'y' i
    · ext j
      simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finsetSum_apply]
      exact ha' j

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 ι
σ : Type u_1
u : σ → ι
hu : Function.Injective u
x : ↥P.ker
⊢ ⇑((P.cotangentRestrict hu) (Extension.Cotangent.mk x)) = fun j ↦ (aeval P.val) ((pderiv (u j)) ↑x)

Tactic:
by
  ext j
  simp only [cotangentRestrict, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Extension.cotangentComplex_mk]
  simp only [toExtension_Ring, P.cotangentSpaceBasis_repr_tmul, one_mul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ⊤.spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
by
  grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le]

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

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

Tactic:
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₂

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