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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u (n - E.order + E.order) = ∑ k, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
h (n - E.order)

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i, E.coeffs i * u (n - E.order + ↑i) = ∑ k, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : u ∈ {u | E.IsSolution u}
n : ℕ
⊢ (a • u) (n + E.order) = ∑ i, E.coeffs i * (a • u) (n + ↑i)

Tactic:
simp [hu n, mul_sum]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : u ∈ {u | E.IsSolution u}
n : ℕ
⊢ ∑ i, a * (E.coeffs i * u (n + ↑i)) = ∑ x, E.coeffs x * (a * u (n + ↑x))
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (DistribSMul.toLinearMap R P I.den) ↑x = I.den • ↑x

Tactic:
DistribSMul.toLinearMap_apply

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ I.den • ↑x = I.den • ↑x
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
x✝ : x ∈ 0
x' : R
x'_mem_zero : x' ∈ ↑0
x'_eq_x : (Algebra.linearMap R P) x' = x
⊢ x = 0

Tactic:
have x'_eq_zero : x' = 0 := x'_mem_zero

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
x✝ : x ∈ 0
x' : R
x'_mem_zero : x' ∈ ↑0
x'_eq_x : (Algebra.linearMap R P) x' = x
x'_eq_zero : x' = 0
⊢ x = 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
⊢ ↑(Ideal.span {x}) = spanSingleton S ((algebraMap R P) x)

Tactic:
ext y

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S ((algebraMap R P) x)
Module: Mathlib.RingTheory.Flat.IsBaseChange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
isb₃ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)))
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
s : S
m : M₁
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁))))
        s)
      m =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
            ↑R (LinearMap.baseChange S f)))
        s)
      m

Tactic:
simpa using congr(s • ($comm₁ m)).symm

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
⊢ ¬f r = 0

Tactic:
simp [hr0]

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

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

Tactic:
by grw [h'.1.equiv]

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

Goal state before:
pp: 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'
a : R
x : M'
x' : M
hx : f x' = x
⊢ IsInteger f (a • x)

Tactic:
use a • x'

Goal state after:
case h
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'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • x
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
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
replace hx : _ ∈ y • Submodule.span R (s : Set M') := Set.smul_mem_smul_set hx

Goal state after:
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
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
hx : ↑y • f x ∈ y • Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : IsLocalRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Module.Finite R A
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
⊢ IsDedekindDomain.primesOverFinset p A = {maximalIdeal A}

Tactic:
have : IsDomain R := .of_faithfulSMul R A

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : IsLocalRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Module.Finite R A
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
⊢ IsDedekindDomain.primesOverFinset p A = {maximalIdeal A}
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M₂ ⧸ f.range →ₗ[A] N✝
h : (pres₂.cokernelSolution data).postcomp f✝ = (pres₂.cokernelSolution data).postcomp f'✝
g : pres₂.G
⊢ (pres₂.postcomp (f✝ ∘ₗ f.range.mkQ)).var g = (pres₂.postcomp (f'✝ ∘ₗ f.range.mkQ)).var g

Tactic:
exact Relations.Solution.congr_var h g

Goal state after:
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
inst✝⁶ : FinitePresentation R M
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
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)

Tactic:
by
  obtain ⟨φ, s, hφ⟩ := FinitePresentation.exists_lift_of_isLocalizedModule S g (ϕ ∘ₗ f)
  have hmap : IsLocalizedModule.map S f g φ = s • ϕ := by
    apply IsLocalizedModule.linearMap_ext S f g
    simp [IsLocalizedModule.map_comp, hφ, LinearMap.smul_comp]
  refine ⟨φ, s, hmap, ?_⟩
  simpa only [hmap] using! ((End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).2.comp hϕ

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

Goal state before:
pp: case add
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)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
x₁ x₂ : L
hx✝ : x₁ ∈ ⨆ i, genWeightSpace L ⇑i
hy✝ : x₂ ∈ ⨆ i, genWeightSpace L ⇑i
ih₁ : ⁅x₁, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
ih₂ : ⁅x₂, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
⊢ ⁅x₁ + x₂, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢

Goal state after:
case add
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)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
x₁ x₂ : L
hx✝ : x₁ ∈ ⨆ i, genWeightSpace L ⇑i
hy✝ : x₂ ∈ ⨆ i, genWeightSpace L ⇑i
ih₁ : ⁅x₁, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
ih₂ : ⁅x₂, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
⊢ ⁅x₁, m⁆ + ⁅x₂, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
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''
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra R R''
inst✝⁴ : Algebra S S'
inst✝³ : Algebra S' S''
inst✝² : Algebra S S''
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : R
⊢ TensorProduct.includeRight.toRingHom ((algebraMap R P.Ring) x) = (algebraMap T P.baseChange.Ring) ((algebraMap R T) x)

Tactic:
by simp [baseChange]

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
hP : P.ker.FG
⊢ (Submodule.map mk ⊤).FG

Tactic:
exact ((Submodule.fg_top P.ker).mpr hP).map _

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M → ∃ pres, Finite pres.G ∧ Finite pres.R

pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M

Tactic:
· intro
    obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (finite_def.1 (inferInstance : Module.Finite A M))
    obtain ⟨R : Type w₁, _, relation, hR⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var) (by
          rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))
    exact
     ⟨{ G := G
        R := R
        relation := relation
        var := var
        linearCombination_var_relation := fun r ↦ by
          rw [Submodule.ext_iff] at hR
          exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
        toIsPresentation := by
          rw [Relations.Solution.isPresentation_iff]
          exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
exact ⟨1, one_mem _, by simpa using h⟩

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
m : ↑↑s
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
⊢ s.attach.prod x • ↑m = 0

Tactic:
rw [hk, mul_comm, mul_smul, hx, smul_zero]

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
⊢ N.spanFinrank ≤ ⊤.spanFinrank

Tactic:
have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id]

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
⊢ N.spanFinrank ≤ ⊤.spanFinrank
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
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ i.range = ⊤

Tactic:
Finsupp.range_linearCombination

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
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Submodule.span R (Set.range v) = ⊤
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: 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
⊢ False

Tactic:
have h2 : I ≠ ⊤ := by contrapose hI; simp [hI, minimalPrimes_top]

Goal state after:
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 ≠ ⊤
⊢ False
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)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
c : R
u : s i →ₗ[R] t i
⊢ map (update f i (c • u)) = c • map (update f i u)

Tactic:
by
  ext x
  simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.smul_apply,
    MultilinearMap.map_update_smul]

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

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ ↑(reindex R s e ≪≫ₗ reindex R (fun i ↦ s (e.symm i)) e') = ↑(reindex R s (e.trans e'))

Tactic:
ext f

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ ((↑(reindex R s e ≪≫ₗ reindex R (fun i ↦ s (e.symm i)) e')).compMultilinearMap (tprod R)) f =
    ((↑(reindex R s (e.trans e'))).compMultilinearMap (tprod R)) f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : Subsingleton ι
i₀ : ι
⊢ { toFun := fun x ↦ (tprod R) (update 0 i₀ x), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      lift { toFun := fun f ↦ f i₀, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    LinearMap.id

Tactic:
ext f

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
⊢ (({ toFun := fun x ↦ (tprod R) (update 0 i₀ x), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
            lift { toFun := fun f ↦ f i₀, map_update_add' := ⋯, map_update_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      f =
    (LinearMap.id.compMultilinearMap (tprod R)) f
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: 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'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (⊥.colon {x}).radical M
r : R
⊢ r ∈ (⊥.colon {x}).radical ↔ r ∈ (⊥.colon {f x}).radical

Tactic:
simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]

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

Goal state before:
pp: case mpr
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
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have : Module.Finite R (LinearMap.ker l) := by
      refine Module.Finite.of_surjective l' ?_
      exact Function.HasRightInverse.surjective ⟨_, DFunLike.congr_fun hl'⟩

Goal state after:
case mpr
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
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Free R (N ⧸ l.range)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite R ↥l.ker
⊢ ∃ l', l' ∘ₗ l = LinearMap.id
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type ?u.44} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
⊢ Nonempty (Basis (Fin n) R M)

Tactic:
have b' (P) := Module.finBasisOfFinrankEq _ _ (rk P)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
⊢ Nonempty (Basis (Fin n) R M)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I).num
hJunit : IsUnit ↑J
⊢ (↑↑I).IsPrincipal

Tactic:
have hJprin : J.IsPrincipal := isPrincipal_of_isUnit_fractionalIdeal J hJunit

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I).num
hJunit : IsUnit ↑J
hJprin : Submodule.IsPrincipal J
⊢ (↑↑I).IsPrincipal