mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ Submodule.IsPrincipal ⊤

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ Submodule.IsPrincipal ⊤
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ Submodule.restrictScalars R pS

Tactic:
]

Goal state after:
case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ Submodule.restrictScalars R pS
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
⊢ 1 ∈ extended L hf I

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
⊢ 1 ∈ extended L hf I
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
⊢ (IsLocalization.map L f hf) 1 = 1

Tactic:
by rw [map_one]

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

Goal state before:
pp: case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) i + (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))

Tactic:
]

Goal state after:
case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) i + (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x)).trace =
    (((leftMulMatrix b) x).map ⇑(Ideal.Quotient.mk p)).trace

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x)).trace =
    (((leftMulMatrix b) x).map ⇑(Ideal.Quotient.mk p)).trace
Module: Mathlib.RingTheory.Trace.Quotient

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.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ (algebraMap Rₚ (Sₚ ⧸ pSₚ)).comp (algebraMap R Rₚ) = (algebraMap Rₚ (Sₚ ⧸ pSₚ)).comp (algebraMap R Rₚ)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (algebraMap R (Sₚ ⧸ pSₚ)) x = (algebraMap R (Sₚ ⧸ pSₚ)) x

Tactic:
]

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

Goal state before:
pp: case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
this : (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).ker = Submodule.restrictScalars R pS
⊢ ↑(IsScalarTower.toAlgHom R S (S ⧸ pS)) x ∈ ⊤

Tactic:
]

Goal state after:
case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
this : (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).ker = Submodule.restrictScalars R pS
⊢ ↑(IsScalarTower.toAlgHom R S (S ⧸ pS)) x ∈ ⊤
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
]

Goal state after:
case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.Trace.Quotient

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.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ algebraMap R Sₚ = algebraMap R Sₚ

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Trace.Quotient

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.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ algebraMap R Sₚ = (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ)

Tactic:
by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ |↑((minpoly ℤ ↑x).coeff i)| = |↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)|

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Trace.Quotient

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.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
hs : span R s = ⊤
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑↑(IsScalarTower.toAlgHom R S (S ⧸ pS))

Tactic:
]

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
hs : span R s = ⊤
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑↑(IsScalarTower.toAlgHom R S (S ⧸ pS))
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑(Ideal.Quotient.mk pS)

Tactic:
]

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑(Ideal.Quotient.mk pS)
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span R s = ⊤ → span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

Tactic:
· intro hs
    rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr,
      restrictScalars_eq_top_iff] at H
    rw [LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
    exact Ideal.Quotient.mk_surjective

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

Goal state before:
pp: case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ f a • (IsLocalization.map L f hf) y ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
]

Goal state after:
case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ f a • (IsLocalization.map L f hf) y ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case a.hv
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ span (R ⧸ p) (?a.hv.g✝ '' Set.range ?a.hv.f✝) = ⊤

pp: case a.hv.g
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ ?m.104 → S ⧸ pS

pp: case a.hv.f
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ Free.ChooseBasisIndex R S → ?m.104

pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ Type ?u.64

Tactic:
]

Goal state after:
case a.hv
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ span (R ⧸ p) (?a.hv.g✝ '' Set.range ?a.hv.f✝) = ⊤

case a.hv.g
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ ?m.104 → S ⧸ pS

case a.hv.f
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ Free.ChooseBasisIndex R S → ?m.104

R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := ⋯
⊢ Type ?u.64
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ span C (⇑(IsLocalization.map W g hg) '' ↑(extended L hf I)) = span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I)

Tactic:
]

Goal state after:
A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ span C (⇑(IsLocalization.map W g hg) '' ↑(extended L hf I)) = span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I)
Module: Mathlib.RingTheory.Trace.Quotient

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.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
z : K
hz : z ∈ ↑I
⊢ (IsLocalization.map W (g.comp f) ⋯) z = (IsLocalization.map W (g.comp f) ⋯) z

Tactic:
]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span (R ⧸ p) (Set.range ⇑b) = ⊤

Tactic:
]

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span (R ⧸ p) (Set.range ⇑b) = ⊤