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

Goal state before:
pp: 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
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ f.range = ⊤

Tactic:
]

Goal state after:
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
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ f.range = ⊤
Module: Mathlib.Algebra.Module.LocalizedModule.Int

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

Tactic:
]

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
s : Finset M'
⊢ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach = commonDenomOfFinset S f s • ↑s
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I
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
⊢ commonDenom S f s id • id ↑x ∈ commonDenomOfFinset S f s • ↑s

Tactic:
]

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.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ 0
hb : b = 0
⊢ span {a} ∈ 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ 0
hb : b = 0
⊢ span {a} ∈ 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: 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
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ l.ker = l.ker

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ 0

Tactic:
rw [hb, normalizedFactors_zero] at ha

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ 0
hb : b = 0
⊢ span {a} ∈ 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ c ∈ normalizedFactors (span {b})

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ c ∈ normalizedFactors (span {b})
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ (span {a}).IsPrime

pp: case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ≠ ⊥

Tactic:
]

Goal state after:
case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ (span {a}).IsPrime

case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ≠ ⊥
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:
]

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'
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)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = ↑(multiplicity a b)

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = ↑(multiplicity a b)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ a ^ multiplicity a b ∣ b

Tactic:
]

Goal state after:
case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ a ^ multiplicity a b ∣ b
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b

Tactic:
]

Goal state after:
case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b
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'
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 : f (↑y • x) ∈ Submodule.map f (Submodule.span R ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
]

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 : f (↑y • x) ∈ Submodule.map f (Submodule.span R ↑(finsetIntegerMultiple S f 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
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
this : ¬FiniteMultiplicity (span {a}) (span {b})
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ n ∣ b

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ n ∣ b
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
b : R
hb : b ∈ {d | d ∈ normalizedFactors r}
h : Associated a b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
]

Goal state after:
case refine_2.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
b : R
hb : b ∈ {d | d ∈ normalizedFactors r}
h : Associated a b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: 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
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype f.ker).FG

Tactic:
]

Goal state after:
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
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype f.ker).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩)) (span {r}) =
    emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩)) (span {r})

Tactic:
]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (↑e.symm ∘ₗ LinearMap.inr R M P).range.FG

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (↑e.symm ∘ₗ LinearMap.inr R M P).range.FG
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Sort ?u.18
inst✝² : Finite ι
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
hf : Function.Surjective ⇑(LinearMap.fst R M N)
⊢ FinitePresentation R ↥(LinearMap.inr R M N).range

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Sort ?u.18
inst✝² : Finite ι
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
hf : Function.Surjective ⇑(LinearMap.fst R M N)
⊢ FinitePresentation R ↥(LinearMap.inr R M N).range
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ p.primesOver B ↔ P ∈ p.primesOver B

Tactic:
]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
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✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this : (LinearMap.baseChange A f).ker = (LinearMap.baseChange A f.ker.subtype).range
⊢ (LinearMap.baseChange A f).ker.FG

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
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✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this : (LinearMap.baseChange A f).ker = (LinearMap.baseChange A f.ker.subtype).range
⊢ (LinearMap.baseChange A f).ker.FG
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 ≠ ⊥
this : IsDomain R
⊢ {maximalIdeal A} = {maximalIdeal A}

Tactic:
]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
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✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this : (LinearMap.baseChange A f).ker = (LinearMap.baseChange A f.ker.subtype).range
⊢ (LinearMap.baseChange A f.ker.subtype).range.FG

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
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✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this : (LinearMap.baseChange A f).ker = (LinearMap.baseChange A f.ker.subtype).range
⊢ (LinearMap.baseChange A f.ker.subtype).range.FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A✝
inst✝⁶ : Field K
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
hp : p ≠ 0
v : HeightOneSpectrum B
hv : v ∈ fun v ↦ ∃ c, map (algebraMap A B) p = v.asIdeal * c
⊢ v.asIdeal ∣ map (algebraMap A B) p

Tactic:
]

Goal state after:
R : Type u_1
A✝ : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A✝
inst✝⁶ : Field K
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
hp : p ≠ 0
v : HeightOneSpectrum B
hv : v ∈ fun v ↦ ∃ c, map (algebraMap A B) p = v.asIdeal * c
⊢ v.asIdeal ∣ map (algebraMap A B) p
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite

Tactic:
]

Goal state after:
case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ {⊥}.Finite

Tactic:
]

Goal state after:
case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ {⊥}.Finite