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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup 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 : M), f x = 0 → ∃ n, r ^ n • x = 0
⊢ IsLocalizedModule.Away r f

Tactic:
refine IsLocalizedModule.Away.mk h₁ h₂ fun x y hxy ↦ ?_
  have : f (x - y) = 0 := by simp [hxy]
  obtain ⟨n, hn⟩ := h₃ _ this
  use n
  simpa [smul_sub, sub_eq_zero] using hn

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

Goal state before:
pp: case hs1
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
⊢ l.range.FG

Tactic:
LinearMap.range_eq_top.mpr hl

Goal state after:
case hs1
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
⊢ ⊤.FG
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case mp
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 : ↥s
⊢ f ((fun t ↦ integerMultiple S f s id t) x) ∈ commonDenomOfFinset S f s • ↑s

Tactic:
rw [map_integerMultiple]

Goal state after:
case mp
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 : ↥s
⊢ commonDenom S f s id • id ↑x ∈ commonDenomOfFinset S f s • ↑s
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M✝ : Type ?u.7
N : Type ?u.12
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι✝ : Sort ?u.18
inst✝⁴ : Finite ι✝
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), FinitePresentation R (M i)
inst✝ : Finite ι
⊢ FinitePresentation R ((i : ι) → M i)

Tactic:
refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
  · exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
  · exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
  · infer_instance
  · introv hN hN'
    infer_instance

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ p ∈ supported R s ↔ ↑p.vars ⊆ s

Tactic:
supported_eq_range_rename,

Goal state after:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ p ∈ (rename Subtype.val).range ↔ ↑p.vars ⊆ s
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s : Set σ
inst✝ : Nontrivial R
i : σ
⊢ X i ∈ supported R s ↔ i ∈ s

Tactic:
simp [mem_supported]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : F ∈ supported ℤ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
supported_eq_range_rename,

Goal state after:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : F ∈ (rename Subtype.val).range
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case e'_2.e'_1
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
x : ↥σ →₀ R
hxσ : x ∈ ↑τ
⊢ s' ⟨x, hxσ⟩ • (linearCombination R i) x = 0

Tactic:
exact hs' ⟨x, hxσ⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
⊢ (pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (pderiv i) f

Tactic:
rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝² : CommRing R''
inst✝¹ : CommRing S''
inst✝ : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (r + s) • x = r • x + s • x

Tactic:
by
    have := smul_eq_zero_of_mem (P.σ (r + s) - (P.σ r + P.σ s) : P.Ring) (by simp) x
    simpa only [sub_smul, add_smul, sub_eq_zero]

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

Goal state before:
pp: case refine_2
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ genWeightSpace L (-⇑↑⟨β, ⋯⟩) ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ

pp: case refine_3
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ corootSubmodule ↑⟨β, ⋯⟩ ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ

Tactic:
· have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
        exact le_iSup₂_of_le _ (hne (-β) this) le_rfl

Goal state after:
case refine_3
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ corootSubmodule ↑⟨β, ⋯⟩ ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ
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:
rw [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.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_2.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
r : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker
m : M
⊢ ((LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype (r, m).1, LinearMap.id (r, m).2).1 ∈ ⨅ i, I i

pp: case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤

Tactic:
· simpa only [← (I _).ker_mkQ, ← ker_pi] using! Subtype.mem _

Goal state after:
case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ support R N ⊆ support R M

Tactic:
by
  simp_rw [Set.subset_def, mem_support_iff']
  rintro x ⟨m, hm⟩
  obtain ⟨m, rfl⟩ := hf m
  exact ⟨m, fun r hr e ↦ hm r hr (by simpa using congr(f $e))⟩

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
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ s • r • m = 0

Tactic:
← hm',

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ s • f m' = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)).range = M

Tactic:
rw [Algebra.toSubmodule_bot, mulMap_range, mul_one]

Goal state after:
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✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Tactic:
rw [LinearIndependent] at hm

Goal state after:
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✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))
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)
⊢ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) []).sum = 0

Tactic:
List.map_nil,

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)
⊢ [].sum = 0
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R P
inst✝ : Flat R P
w : Basis (Free.ChooseBasisIndex k (k ⊗[R] P)) k (k ⊗[R] P) := Free.chooseBasis k (k ⊗[R] P)
v : Free.ChooseBasisIndex k (k ⊗[R] P) → P
eq : (fun x ↦ ⇑((TensorProduct.mk R k P) 1) ∘ x) v = ⇑w
⊢ ⊤ ≤ Submodule.span R (Set.range v)

Tactic:
by
    exact (span_eq_top_of_tmul_eq_basis _ w <| congr_fun eq).ge

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

Goal state before:
pp: case refine_2
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 = ⊥.colon {(f ∘ₗ mkQ I) 1}

Tactic:
conv_lhs => rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]

Goal state after:
case refine_2
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
⊢ (f ∘ₗ mkQ I).ker = ⊥.colon {(f ∘ₗ mkQ I) 1}
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
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ False

Tactic:
rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂

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
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_2
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
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ J.asIdeal
⊢ J ∈ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier

Tactic:
J.isPrime.mul_mem_iff_mem_or_mem.not,

Goal state after:
case refine_2
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
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : ¬(a ⊗ₜ[R] 1 ∈ J.asIdeal ∨ 1 ⊗ₜ[R] t ∈ J.asIdeal)
⊢ J ∈ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mp
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f✝ : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f✝ ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).range
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
⊢ f ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f✝).range →
    f ∈
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f✝)).range

Tactic:
intro hf
      obtain ⟨a, ha, c, rfl⟩ := hf
      obtain ⟨g, rfl⟩ := ha
      use IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g c
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
        (LocalizedModule.map I.primeCompl) c).injective
      dsimp
      conv_rhs => rw [← Submonoid.smul_def]
      conv_lhs => rw [← LinearMap.map_smul_of_tower]
      rw [← Submonoid.smul_def, IsLocalizedModule.mk'_cancel', IsLocalizedModule.mk'_cancel']
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)
      · exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)
      ext
      simp only [LocalizedModule.map_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        Function.comp_apply, LocalizedModule.mkLinearMap_apply, LinearMap.llcomp_apply,
        LocalizedModule.map_mk]

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 _ _

Goal state after:
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'
this : FinitePresentation R (I →₀ R)
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h'
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝¹ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
x : R
s : ↥S
hx : IsLocalization.mk' (Localization S) x s ∈ p.asIdeal.primeCompl
H : x ∈ ↑p'
⊢ (algebraMap R (Localization S)) x * IsLocalization.mk' (Localization S) 1 s ∈ ↑p.asIdeal

Tactic:
exact Ideal.mul_mem_right _ _ H

Goal state after: