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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : index K
⊢ K →+* ℂ

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective fun c ↦ ?refine_1

pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (index K) = Fintype.card (K →+* ℂ)

Tactic:
· cases c with
    | inl w => exact w.val.embedding
    | inr wj => rcases wj with ⟨w, j⟩
                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective fun c ↦
    Sum.casesOn (motive := fun t ↦ c = t → K →+* ℂ) c (fun w h ↦ (↑w).embedding)
      (fun wj h ↦ Prod.casesOn wj fun w j ↦ if j = 0 then (↑w).embedding else ComplexEmbedding.conjugate (↑w).embedding)
      ⋯

case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (index K) = Fintype.card (K →+* ℂ)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace K
⊢ InfinitePlace.IsUnramified k w

Tactic:
obtain ⟨w, rfl⟩ := InfinitePlace.comap_surjective (K := F) w

Goal state after:
k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace F
⊢ InfinitePlace.IsUnramified k ((fun x ↦ x.comap (algebraMap K F)) w)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
by
  have hB : 0 ≤ B := by
    contrapose! h
    rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]
    exact minkowskiBound_pos K I
  -- Some inequalities that will be useful later on
  have h1 : 0 < (finrank ℚ K : ℝ)⁻¹ := inv_pos.mpr (Nat.cast_pos.mpr finrank_pos)
  have h2 : 0 ≤ B / (finrank ℚ K) := div_nonneg hB (Nat.cast_nonneg _)
  have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
  have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
    change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
    infer_instance
  obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure
      h_fund (fun _ ↦ convexBodySum_neg_mem K B) (convexBodySum_convex K B)
      (convexBodySum_compact K B) h
  rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx
  obtain ⟨a, ha, rfl⟩ := hx
  refine ⟨a, ha, by simpa using h_nz, ?_⟩
  rw [← rpow_natCast, ← rpow_le_rpow_iff (by simp only [Rat.cast_abs, abs_nonneg])
      (rpow_nonneg h2 _) h1, ← rpow_mul h2, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr
      (ne_of_gt finrank_pos)), rpow_one, le_div_iff₀' (Nat.cast_pos.mpr finrank_pos)]
  refine le_trans ?_ ((convexBodySum_mem K B).mp h_mem)
  rw [← le_div_iff₀' (Nat.cast_pos.mpr finrank_pos), ← sum_mult_eq, Nat.cast_sum]
  refine le_trans ?_ (geom_mean_le_arith_mean Finset.univ _ _ (fun _ _ => Nat.cast_nonneg _)
    ?_ (fun _ _ => AbsoluteValue.nonneg _ _))
  · simp_rw [← prod_eq_abs_norm, rpow_natCast]
    exact le_of_eq rfl
  · rw [← Nat.cast_sum, sum_mult_eq, Nat.cast_pos]
    exact finrank_pos

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := ⋯
L : Type u_6 := ⋯
E : Type u_6 := ⋯
this : IsIntegral A (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))
y : B
hy : (algebraMap B L) y = ((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)
⊢ (algebraMap B L) ((algebraMap A B) ((intNorm A B) x)) = (algebraMap B L) (x * y)

Tactic:
← algebraMap_apply,

Goal state after:
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsIntegral A (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))
y : B
hy : (algebraMap B L) y = ((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)
⊢ (algebraMap A L) ((intNorm A B) x) = (algebraMap B L) (x * y)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A
    (((algebraMap L E) ((algebraMap B L) x))⁻¹ * (algebraMap L E) ((algebraMap K L) ((norm K) ((algebraMap B L) x))))

Tactic:
← algebraMap_apply,

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A (((algebraMap B E) x)⁻¹ * (algebraMap L E) ((algebraMap K L) ((norm K) ((algebraMap B L) x))))
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A (((algebraMap B E) x)⁻¹ * (algebraMap L E) ((algebraMap K L) ((norm K) ((algebraMap B L) x))))

Tactic:
← algebraMap_apply,

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A (((algebraMap B E) x)⁻¹ * (algebraMap K E) ((norm K) ((algebraMap B L) x)))
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝² : Algebra.IsIntegral A C
this✝¹ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝¹ : Q.IsPrime
right✝¹ : Q.LiesOver P
this✝ : Q.LiesOver p
Q' : Ideal C
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver P
this : Q'.LiesOver p
g : GAC
hg : Q' = g • Q
⊢ Q' ∈ orbit (↥H) Q

Tactic:
exact ⟨⟨g, key Q Q' g hg.symm⟩, by simpa [Subgroup.smul_def] using hg.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal ℤ
hI : I ≠ ⊥
⊢ Finite (ℤ ⧸ I)

Tactic:
by
    obtain ⟨n, rfl⟩ := Submodule.IsPrincipal.principal I
    have : NeZero n := ⟨by simpa using hI⟩
    exact inferInstanceAs <| Finite (ℤ ⧸ Ideal.span {n})

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Tactic:
have : Module.Finite R N := .of_fg hN

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
this : Module.Finite R ↥N
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0
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 I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ ↑I, IsInteger A (a • b)
b : L
hb : b ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
x : L
hx : x ∈ ⇑(IsLocalization.map L f hf) '' ↑I
⊢ IsInteger B (f a • x)

pp: case refine_2
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 I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ ↑I, IsInteger A (a • b)
b✝ : L
hb : b✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
c : L
x✝ : c ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hc : IsInteger B (f a • c)
⊢ IsInteger B (f a • b • c)

Tactic:
· rcases hx with ⟨k, kI, rfl⟩
      obtain ⟨c, hc⟩ := frac k kI
      exact ⟨f c, by simp [← IsLocalization.map_smul, ← hc]⟩

Goal state after:
case refine_2
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 I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ ↑I, IsInteger A (a • b)
b✝ : L
hb : b✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
c : L
x✝ : c ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hc : IsInteger B (f a • c)
⊢ IsInteger B (f a • b • c)
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
f : (↥s →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
⊢ ∃ a, f a = x

Tactic:
by
    obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
⊢ Finite (R ⧸ ∏ i ∈ insert a s, I i)

Tactic:
Finset.prod_insert has,

Goal state after:
case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
⊢ Finite (R ⧸ I a * ∏ x ∈ s, I x)
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
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
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact ((quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq).ge

Goal state after:
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 J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' ↑I) * span (⇑(Algebra.intNorm R S) '' ↑J) ≤ map (Algebra.intNorm R S) (I * J)

Tactic:
rw [Ideal.span_mul_span', ← Set.image_mul]

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 J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ map (Algebra.intNorm R S) (I * J)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst✝ : IsGalois ℚ ↥K₁
h : IsCoprime (discr ↥K₁) (discr ↥K₂)
⊢ K₁.LinearDisjoint ↥K₂

Tactic:
by
  apply IntermediateField.LinearDisjoint.of_inf_eq_bot
  suffices IsUnit (discr ↥(K₁ ⊓ K₂)) by
    contrapose! this
    have : 1 < Module.finrank ℚ ↥(K₁ ⊓ K₂) := by
      refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
      rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
    exact Int.isUnit_iff_abs_eq.not.mpr <| by linarith [abs_discr_gt_two this]
  exact h.isUnit_of_dvd' (NumberField.discr_dvd_discr _ _) (NumberField.discr_dvd_discr _ _)

Goal state after:
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 P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := ⋯
Rₚ : Type u_1 := ⋯
K : Type u_1 := ⋯
⊢ (algebraMap Rₚ K)
      ((Algebra.intNorm (Localization.AtPrime P) (Localization P'))
        ((algebraMap Rₚ (Localization P')) (IsPrincipal.generator (map (algebraMap R Rₚ) I)))) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I) ^ finrank R S)

Tactic:
Algebra.algebraMap_intNorm (L := FractionRing S),

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
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ (Algebra.norm K)
      ((algebraMap (Localization P') (FractionRing S))
        ((algebraMap Rₚ (Localization P')) (IsPrincipal.generator (map (algebraMap R Rₚ) I)))) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I) ^ finrank R S)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
⊢ ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p

Tactic:
intro i hi
      rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
        show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map, map_comp, map_cyclotomic,
        Polynomial.map_add, map_X, Polynomial.map_one, pow_add, pow_one,
        cyclotomic_mul_prime_dvd_eq_pow, pow_comp, ← ZMod.expand_card, coeff_expand hp.out.pos]
      · simp only [ite_eq_right_iff]
        rintro ⟨k, hk⟩
        rw [natDegree_comp, show (X + 1 : ℤ[X]) = X + C 1 by simp, natDegree_X_add_C, mul_one,
          natDegree_cyclotomic, Nat.totient_prime_pow hp.out (Nat.succ_pos _), Nat.add_one_sub_one]
          at hn hi
        rw [hk, pow_succ', mul_assoc] at hi
        rw [hk, mul_comm, Nat.mul_div_cancel _ hp.out.pos]
        replace hn := hn (lt_of_mul_lt_mul_left' hi)
        rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
           show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map] at hn
        simpa [map_comp] using hn
      · exact ⟨p ^ n, by rw [pow_succ']⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
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
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
h₀ : ∀ Q ∈ (p.primesOver S).toFinset, (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)
h : p ^ (p.ramificationIdxIn S * s * (p.primesOver S).toFinset.card) = p ^ finrank R S
⊢ s = P.inertiaDeg R

Tactic:
← IsGaloisGroup.card_eq_finrank' G R S,

Goal state after:
case neg
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
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
h₀ : ∀ Q ∈ (p.primesOver S).toFinset, (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)
h : p ^ (p.ramificationIdxIn S * s * (p.primesOver S).toFinset.card) = p ^ Nat.card G
⊢ s = P.inertiaDeg R
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
rw [← pow_one p] at hζ hcycl
  exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ

Goal state after:
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✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
⊢ ∀ a ∈ I, ((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range

Tactic:
intro a ha

Goal state after:
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✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ ((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e'_2
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ Algebra.discr ℚ ⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

pp: case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (algebraMap ℤ ℚ) ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
· have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim := by
      rw [← PowerBasis.finrank, ← PowerBasis.finrank]
      exact RingOfIntegers.rank K
    rw [← Algebra.discr_reindex _ _ (finCongr this)]
    congr 1
    ext i
    simp_rw [Function.comp_apply, Module.Basis.localizationLocalization_apply, powerBasis_dim,
      PowerBasis.coe_basis, pB₁, integralPowerBasisOfPrimePow_gen]
    convert! ← ((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm using 1

Goal state after:
case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (algebraMap ℤ ℚ) ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))