mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 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
⊢ ⇑(IsLocalization.map W g hg) '' ↑(extended L hf I) ⊆ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
rintro _ ⟨x, hx, rfl⟩
    have hx' : x ∈ span B (IsLocalization.map L f hf '' (I : Set K)) :=
      (mem_extended_iff L hf I x).1 hx
    refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_) (fun b y _ hy ↦ ?_) hx'
    · rcases hy with ⟨z, hz, rfl⟩
      exact Submodule.subset_span ⟨z, hz, by rw [IsLocalization.map_map]⟩
    · rw [map_add]
      exact add_mem hy hz
    · rw [IsLocalization.map_smul]
      exact smul_mem _ (g b) hy

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : IsDomain T
inst✝⁵ : Algebra R S
P : Ideal R
inst✝⁴ : P.IsPrime
inst✝³ : FaithfulSMul R S
inst✝² : Algebra S T
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ IsLocalization P'' Tₚ

Tactic:
exact Localization.isLocalization

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : IsDomain T
inst✝⁵ : Algebra R S
P : Ideal R
inst✝⁴ : P.IsPrime
inst✝³ : FaithfulSMul R S
inst✝² : Algebra S T
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ algebraMap S Tₚ = (IsLocalization.map Tₚ (algebraMap S T) ⋯).comp (algebraMap S Sₚ)

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : IsDomain T
inst✝⁵ : Algebra R S
P : Ideal R
inst✝⁴ : P.IsPrime
inst✝³ : FaithfulSMul R S
inst✝² : Algebra S T
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ algebraMap S Tₚ = (algebraMap T Tₚ).comp (algebraMap S T)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
⊢ algebraMap R K = f.comp (algebraMap R Rₘ)

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
⊢ algebraMap R K = (algebraMap R K).comp (RingHom.id R)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
⊢ algebraMap S L = g.comp (algebraMap S Sₘ)

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
⊢ algebraMap S L = (algebraMap S L).comp (RingHom.id S)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this : IsScalarTower S Sₘ L
⊢ (algebraMap K L).comp (f.comp (algebraMap R Rₘ)) = g.comp ((algebraMap S Sₘ).comp (algebraMap R S))

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this : IsScalarTower S Sₘ L
⊢ (algebraMap K L).comp ((algebraMap R K).comp (RingHom.id R)) = g.comp ((algebraMap S Sₘ).comp (algebraMap R S))
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this : IsScalarTower S Sₘ L
⊢ (algebraMap K L).comp (algebraMap R K) = (g.comp (algebraMap S Sₘ)).comp (algebraMap R S)

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
inst✝²⁴ : CommRing R
inst✝²³ : IsDomain R
S : Type u_3
inst✝²² : CommRing S
inst✝²¹ : IsDomain S
inst✝²⁰ : IsIntegrallyClosed R
inst✝¹⁹ : IsIntegrallyClosed S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Module.Finite R S
inst✝¹⁶ : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this : IsScalarTower S Sₘ L
⊢ (algebraMap K L).comp (algebraMap R K) = ((algebraMap S L).comp (RingHom.id S)).comp (algebraMap R S)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

Tactic:
cases subsingleton_or_nontrivial S

Goal state after:
case inl
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Subsingleton S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

case inr
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
⊢ ¬p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})

Tactic:
by
  have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
  have := CharZero.of_module (R := 𝒪) K
  rw [not_dvd_discr_iff_forall_liesOver K 𝒪 hp]
  exact (Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain'
    (Ideal.span_singleton_eq_bot.not.mpr hp.ne_zero)).symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case a.f
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
x✝ : ℕ
| (↑(p.choose (x✝ + 1)) * X ^ x✝).coeff i

Tactic:
← C_eq_natCast,

Goal state after:
case a.f
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
x✝ : ℕ
| (C ↑(p.choose (x✝ + 1)) * X ^ x✝).coeff i
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
⊢ x ∈ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

Tactic:
let b₂ := (Free.chooseBasis A R₂).localizationLocalization K A⁰ F₂

Goal state after:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
⊢ x ∈ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1.succ
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
⊢ x ∈ ℤ[ζ]

Tactic:
have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {(p : ℤ)}) := by
      have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
      have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (NeZero.pos _))
      rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
      rw [h₁, ← map_cyclotomic_int, ← algebraMap_int_eq,
        show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
      rw [IsPrimitiveRoot.subOnePowerBasis_gen,
        map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
      exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _

Goal state after:
case refine_1.succ
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
hmin : (minpoly ℤ B.gen).IsEisensteinAt (ℤ ∙ ↑p)
⊢ x ∈ ℤ[ζ]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = (pB.basis.coord ⟨1, hdim⟩) (↑p • x) + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ False

Tactic:
map_smul,

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑p • (pB.basis.coord ⟨1, hdim⟩) x + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑p • (pB.basis.coord ⟨1, hdim⟩) x + (pB.basis.coord ⟨1, hdim⟩) (n • 1)
⊢ False

Tactic:
map_smul,

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑p • (pB.basis.coord ⟨1, hdim⟩) x + n • (pB.basis.coord ⟨1, hdim⟩) 1
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ ⊤ᵛ = if IsField A then ⊤ else ⊥

Tactic:
by
  convert! traceDual_top'
  rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
    LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L),
    ← RingHom.range_eq_top, _root_.eq_top_iff]
  simp [SetLike.le_def]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ ↑hζ.toInteger = ↑(-1)

Tactic:
exact hζ'

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : hζ.toInteger - 1 ∣ ↑↑p
⊢ hζ.toInteger - 1 ∣ ↑p

Tactic:
by simpa

Goal state after: