mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case h
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 := ⋯
⊢ Submodule.span R ↑(t.attach.biUnion sf) = ⊤

Tactic:
rw [Submodule.span_attach_biUnion, eq_top_iff]

Goal state after:
case h
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, Submodule.span R ↑(sf x)
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
inst✝⁷ : Flat R M
K : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ x = y ∘ₗ a ∘ₗ ↑e.symm

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Finite R M
M' : Type u_5
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalizedModule p.primeCompl l
inst✝ : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
have : Subsingleton (LocalizedModule p.primeCompl M) := e.subsingleton

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Finite R M
M' : Type u_5
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalizedModule p.primeCompl l
inst✝ : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
this : Subsingleton (LocalizedModule p.primeCompl M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
hσ' : Monotone ⇑(Equiv.symm σ)
i : Fin n
⊢ σ i = 1 i

Tactic:
exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n

Tactic:
Module.finrank_eq_card_basis (Module.Free.chooseBasis R M),

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ finrank R ↥(⋀[R]^n M) = (Fintype.card (Free.ChooseBasisIndex R M)).choose n
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n s
⊢ f i = 0

Tactic:
have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv

Goal state after:
case insert
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n s
l : ℕ
a : ↥(insert n s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
⊢ f i = 0
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹

Tactic:
rw [← hj.mul_left_inj, mul_assoc, hj.val_inv_mul, mul_one, eq_neg_iff_add_eq_zero]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a n j + ∑ i ∈ s, f i * a' i = 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ x.lifts.Nonempty

Tactic:
by
  existsi Quot.out x
  simp [lifts, ← AddCon.quot_mk_eq_coe]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • φ₁ ((tprod R) f) = φ₂ (r • (tprod R) f)

Tactic:
φ₂.map_smul

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • φ₁ ((tprod R) f) = r • φ₂ ((tprod R) f)
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ a = 0
⊢ False

Tactic:
exact h.ne_zero 0 hn.2

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi✝ : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
hi : i = n✝
⊢ (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹ = 0

Tactic:
Finset.sum_eq_zero,

Goal state after:
case insert.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi✝ : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
hi : i = n✝
⊢ -0 * ↑hj.unit⁻¹ = 0

case insert.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi✝ : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
hi : i = n✝
⊢ ∀ x ∈ s, f x * a' x = 0
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝⁶ : CommSemiring 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'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {y}).radical
n : ℕ
hb : b ^ n ∈ ⊥.colon {y}
⊢ b ∈ p

Tactic:
rw [mem_colon_singleton, mem_bot] at hb

Goal state after:
case pos.refine_2
R : Type u_1
inst✝⁶ : CommSemiring 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'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {y}).radical
n : ℕ
hb : b ^ n • y = 0
⊢ b ∈ p
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ f, Function.Injective ⇑f
f : R ⧸ I →ₗ[R] M
h : Function.Injective ⇑f
| I

Tactic:
← I.ker_mkQ,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ f, Function.Injective ⇑f
f : R ⧸ I →ₗ[R] M
h : Function.Injective ⇑f
| (mkQ I).ker
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = I.radical

Tactic:
obtain ⟨hJ, x, e⟩ := h
  have : x ≠ 0 := by
    rintro rfl
    apply hJ.1
    rwa [colon_singleton_zero, Ideal.radical_top] at e
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
  have h {y} : y ∈ colon ⊥ {(Ideal.Quotient.mk I) x} ↔ Ideal.Quotient.mk I (y * x) = 0 := by
    rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
  simp only [e, Ideal.Quotient.mkₐ_eq_mk, ne_eq, Ideal.Quotient.eq_zero_iff_mem] at this h ⊢
  refine le_antisymm (Ideal.radical_le_radical_iff.mpr fun y hy ↦ ?_)
    (Ideal.radical_mono fun y ↦ h.mpr ∘ I.mul_mem_right x)
  rw [← I.colon_univ, ← Set.top_eq_univ]
  exact (hI.mem_or_mem (h.mp hy)).resolve_left this

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ ∀ U ∈ Set.range basicOpen, IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] ↑U

Tactic:
rintro _ ⟨f, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
⊢ IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] ↑(basicOpen f)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}
⊢ f = g

Tactic:
by
  simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h
  ext1 x
  exact Fin.fin_two_eq_of_eq_zero_iff (h x)

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i

Tactic:
have : Module.FinitePresentation R (I →₀ R) := Module.finitePresentation_of_projective _ _
  obtain ⟨r, hr, e, he⟩ := Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule S f
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (b.repr.restrictScalars R)
  let e' := IsLocalizedModule.iso (.powers r) (Finsupp.mapRange.linearMap (α := I)
    (Algebra.linearMap R (Localization (.powers r))))
  refine ⟨r, hr, .ofRepr (e ≪≫ₗ ?_), ?_⟩
  · exact
    { __ := e',
      toLinearMap := e'.extendScalarsOfIsLocalization (.powers r) (Localization (.powers r)) }
  · intro i
    have : e'.symm _ = _ := LinearMap.congr_fun (IsLocalizedModule.iso_symm_comp (.powers r)
      (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (.powers r)))))
      (Finsupp.single i 1)
    simp only [Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply,
      map_one, LocalizedModule.mkLinearMap_apply] at this
    change LocalizedModule.lift _ _ _ (e.symm (e'.symm _)) = _
    replace he := LinearMap.congr_fun he (e.symm (e'.symm (Finsupp.single i 1)))
    simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe,
      Function.comp_apply, LinearEquiv.apply_symm_apply, LinearEquiv.restrictScalars_apply] at he
    apply b.repr.injective
    rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]
    simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization p.primeCompl)) =
    map (↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv)
      (map includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p)))

Tactic:
by
        rw [← Ideal.map_coe includeRight, Ideal.map_map]
        congr
        ext
        simp [Localization.tensorLeftAlgEquiv_apply_one_tmul p.primeCompl]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ F⟮↑α⟯ = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ⊤ ≤ F⟮↑α⟯
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ Nonempty (M.AsModule ≃ₗ[R] N.AsModule)

Tactic:
rw [← mk_eq_iff, mk_eq_self]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hf
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) = 0

Tactic:
rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]

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✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
⊢ ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)

Tactic:
intro K

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
⊢ ∀ (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ ↑E.ncard

Tactic:
by
      rw [hE.cast_ncard_eq]
      exact encard_le_encard <| subset_ground hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
x : α
B : Set α
hB : M.IsBase B
hxE : x ∈ M.E
hxB : x ∉ B
⊢ x ∈ M.closure B

Tactic:
rwa [hB.closure_eq]

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

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk (M.E \ X ∪ Y ∩ M.E) = M.eRk (M.E \ X)

Tactic:
union_eq_self_of_subset_right
      (subset_sdiff.2 ⟨inter_subset_right, hXY.symm.mono_left inter_subset_left⟩)

Goal state after:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk (M.E \ X) = M.eRk (M.E \ X)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Tactic:
by
  rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]

Goal state after: