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

Goal state before:
pp: case refine_2
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ baseChangeHom R S (Fin m → R) N ∘ₗ lcomp R N g =
    ↑R (lcomp S (S ⊗[R] N) (baseChange S g)) ∘ₗ baseChangeHom R S (Fin n → R) N

pp: case refine_3
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(lcomp S (S ⊗[R] N) (baseChange S f)) ⇑(lcomp S (S ⊗[R] N) (baseChange S g))

pp: case refine_4
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Injective ⇑(lcomp S (S ⊗[R] N) (baseChange S f))

Tactic:
· exact LinearMap.ext fun φ ↦ TensorProduct.AlgebraTensorModule.curry_injective
      (LinearMap.ext fun s ↦ (LinearMap.ext fun m ↦ (by simp)))

Goal state after:
case refine_3
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(lcomp S (S ⊗[R] N) (baseChange S f)) ⇑(lcomp S (S ⊗[R] N) (baseChange S g))

case refine_4
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Injective ⇑(lcomp S (S ⊗[R] N) (baseChange S f))
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
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
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
y : P.Ring
y_in : y ∈ P.ker ^ 2
z : P.Ring
z_in : z ∈ RingHom.ker f.toRingHom
hyz : y + z = ↑x
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
suffices ∃ a, a ∈ RingHom.ker f.toRingHom ∧ a ∈ P.ker ∧ a - x ∈ P.ker ^ 2 by
      simpa [mk_eq_mk_iff_sub_mem]

Goal state after:
case refine_1
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
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
y : P.Ring
y_in : y ∈ P.ker ^ 2
z : P.Ring
z_in : z ∈ RingHom.ker f.toRingHom
hyz : y + z = ↑x
⊢ ∃ a ∈ RingHom.ker f.toRingHom, a ∈ P.ker ∧ a - ↑x ∈ P.ker ^ 2
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 ι σ
r : pres.differentialsRelations.R
⊢ pres.toExtension.toKaehler (pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1))) = 0

Tactic:
apply DFunLike.congr_fun (Function.Exact.linearMap_comp_eq_zero
      (pres.toExtension.exact_cotangentComplex_toKaehler))

Goal state after:
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:
rw [← 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.Free

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type w₀
⊢ PEmpty.{w₁ + 1} → G →₀ A

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: case refine_1.refine_2
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
a : P.Ring
⊢ ∀ (hx : a ∈ P.ker • P.ker) (y : P.Ring) (hy : y ∈ P.ker • P.ker),
    1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨y, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + y, ⋯⟩ = 0

Tactic:
ha

Goal state after:
case refine_1.refine_2
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
a : P.Ring
ha : a ∈ P.ker • P.ker
⊢ ∀ (y : P.Ring) (hy : y ∈ P.ker • P.ker),
    1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨y, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + y, ⋯⟩ = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ RingHom.ker (aeval P.val) = P.ker

Tactic:
← ker_eq_ker_aeval_val

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ P.ker = P.ker
Module: Mathlib.Algebra.Module.Presentation.Tensor

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

Tactic:
ext g₁

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
⊢ Odd k

Tactic:
rcases k.val.even_or_odd with hk | hk
  · simpa using (Even.add_odd hk hn).natCast (R := Fin n)
  · exact odd_of_val hk

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
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a

Tactic:
rw [gMul_def, gOne_def]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (mulEquiv ((tprod R) Fin.elim0 ⊗ₜ[R] a)) = a
Module: Mathlib.LinearAlgebra.TensorPower.Basic

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

Tactic:
refine congr_arg a (Fin.ext ?_)

Goal state after:
case smul_tprod.e_a.e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ i)) = ↑i
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
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a

Tactic:
rw [gMul_def, gOne_def]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (mulEquiv (a ⊗ₜ[R] (tprod R) Fin.elim0)) = a
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝¹ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI✝ : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
x✝ : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hyp : y ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
· exact Or.inr ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hyp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hy.le.trans hq.2⟩ hqp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes

Tactic:
← Ideal.radical_minimalPrimes,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I

Tactic:
rw [← mul_assoc, hI.isPrime.mul_le, not_or, Ideal.span_singleton_le_iff_mem]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ I ^ (n - 1) * J * Ideal.span {z} ≤ ann ∧ ¬J ≤ I ∧ z ∉ I
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l = LinearMap.id

Tactic:
rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
⊢ x ∈ J * K

Tactic:
simp [hJK]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case quotient
A : Type u
inst✝⁶ : CommRing A
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : IsNoetherianRing A
N : Type v
inst✝² : AddCommGroup N
inst✝¹ : Module A N
inst✝ : Module.Finite A N
p : PrimeSpectrum A
f : N ≃ₗ[A] A ⧸ p.asIdeal
⊢ (associatedPrimes A N).Finite

Tactic:
have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary

Goal state after:
case quotient
A : Type u
inst✝⁶ : CommRing A
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : IsNoetherianRing A
N : Type v
inst✝² : AddCommGroup N
inst✝¹ : Module A N
inst✝ : Module.Finite A N
p : PrimeSpectrum A
f : N ≃ₗ[A] A ⧸ p.asIdeal
this : associatedPrimes A (A ⧸ p.asIdeal) = {p.asIdeal.radical}
⊢ (associatedPrimes A N).Finite
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x} * Ideal.span {i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
Ideal.span_singleton_mul_right_inj hx

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : β
hx : ¬x ∈ Set.range ⇑ι
⊢ (e.viaEmbedding ι) x = x

Tactic:
exact extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
let := Localization.AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal

Goal state after:
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
this : Algebra (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal) :=
  AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f

Tactic:
by
  rw [← LinearMap.lTensor_inj_iff_rTensor_inj, lTensor_injective_iff]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this✝ : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional F ↥↑K
hfin : FiniteDimensional F ↥⊤
htop : ⨆ K, ↑K = ⊤
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥⊤
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.Indep B ∧ B ⊆ X ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
and_iff_right hB.indep,

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ B ⊆ X ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ (f '' {M | M.E ⊆ E}).Finite

Tactic:
refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_

Goal state after:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ f '' {M | M.E ⊆ E} ⊆ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ IsRightRegular ↑(e 1)

Tactic:
rw [IsRightRegular]
    convert! Subtype.val_injective.comp e.injective using 2
    rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

Tactic:
simpa using hI.1.subset_ground

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
J' : Set α
hfin : (f '' J').Finite
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
⊢ N.Indep (f '' J')

Tactic:
exact (hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
rintro ⟨hI, I, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I)
⊢ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ ⇑f '' I = ⇑f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ (M.map f hf).Indep I

Tactic:
simp only [map_indep_iff]

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ((M ↾ M.E).comap Subtype.val)✶ = M✶.restrictSubtype M.E

Tactic:
← comapOn_preimage_eq,

Goal state after:
α : Type u_1
M : Matroid α
⊢ ((M ↾ M.E).comapOn (M.E ↓∩ (M ↾ M.E).E) Subtype.val)✶ = M✶.restrictSubtype M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
    ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
  exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn]⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
hC' : C.Nontrivial
he : e ∈ C
hL : M.IsLoop e
⊢ False

Tactic:
by simp [hL.eq_of_isCircuit_mem hC he] at hC'

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard

Tactic:
exact encard_mono hI.subset

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.E
heB : e ∉ B
⊢ False

Tactic:
rw [← hB.closure_eq] at heE

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.closure B
heB : e ∉ B
⊢ False