mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |((Algebra.leftMulMatrix b₀) ((algebraMap R K) ↑I.den) * b₀.toMatrix (Subtype.val ∘ ⇑bI)).det| /
      |↑((Algebra.norm ℤ) ↑I.den)|

Tactic:
Matrix.det_mul,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |((Algebra.leftMulMatrix b₀) ((algebraMap R K) ↑I.den)).det * (b₀.toMatrix (Subtype.val ∘ ⇑bI)).det| /
      |↑((Algebra.norm ℤ) ↑I.den)|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ v₁ = v₂

Tactic:
← mk_embedding v₁,

Goal state after:
K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ mk v₁.embedding = v₂
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : (fun φ ↦ ⟨mk ↑φ, ⋯⟩) φ = (fun φ ↦ ⟨mk ↑φ, ⋯⟩) ψ
⊢ φ = ψ

pp: case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w

Tactic:
· rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ 1 ≤ w ↑a

Tactic:
suffices (1 : ℝ) ≤ |Algebra.norm ℚ (a : K)| by
    contrapose! this
    rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
    refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
    · exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _
    · refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
      by_cases hz : z = w
      · rwa [hz]
      · exact h hz
  rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
  exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr ha)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Equiv.Perm.sign (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) = (-1) ^ nrComplexPlaces K

Tactic:
rw [Equiv.Perm.sign_of_pow_two_eq_one, Embeddings.card, ← card_add_two_mul_card_eq_rank,
    ← card_real_embeddings, Fintype.card, Fintype.card, Nat.add_sub_cancel_left,
    Nat.mul_div_cancel_left _ zero_lt_two]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯ ^ 2 = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x : ℚ
⊢ v ↑x = ‖x‖

Tactic:
by
  rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
⊢ v ↑n = ↑n

Tactic:
by
  rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
z : ℤ
⊢ v ↑z = ‖z‖

Tactic:
by
  rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
⊢ (conjugate w.embedding) x = w.embedding x

Tactic:
RingHom.star_apply,

Goal state after:
F : Type u_1
inst✝³ : Field F
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
⊢ star (w.embedding x) = w.embedding x
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 : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ (w.comap f).embedding = w.embedding.comp f

Tactic:
by
   rw [← mk_embedding w, comap_mk, mk_embedding, embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, mk_embedding])]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (normAtPlace w) (-x) = (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (normAtPlace w) (x + y) ≤ (normAtPlace w) x + (normAtPlace w) y

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (normAtPlace w) (c • x) = |c| * (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) =
    |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ volume (convexBodySum K 1) = ↑(convexBodySumFactor K)

Tactic:
rw [MeasureTheory.measure_le_eq_lt _ ((convexBodySumFun_eq_zero_iff 0).mpr rfl)
      convexBodySumFun_neg convexBodySumFun_add_le
      (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx)
      (fun r x => le_of_eq (convexBodySumFun_smul r x))]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ volume {x | convexBodySumFun x < 1} = ↑(convexBodySumFactor K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : ¬(InfinitePlace.mk φ).embedding = φ
⊢ (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)
          ⋯)
      (Sum.inr (mkComplex ⟨φ, hφ⟩, 1)) =
    φ

Tactic:
simp [(embedding_mk_eq φ).resolve_left hw]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
· simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).re ^ 2 < 1

Tactic:
rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
        exact h_le₀.1

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝²⁹ : CommRing A
inst✝²⁸ : CommRing B
inst✝²⁷ : CommRing B₂
inst✝²⁶ : CommRing B₃
inst✝²⁵ : Algebra A B
inst✝²⁴ : Algebra A B₂
inst✝²³ : Algebra A B₃
inst✝²² : Field K
inst✝²¹ : Field L
inst✝²⁰ : Field L₂
inst✝¹⁹ : Field L₃
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra K L
inst✝¹⁶ : Algebra A L
inst✝¹⁵ : IsScalarTower A K L
inst✝¹⁴ : Algebra K L₂
inst✝¹³ : Algebra A L₂
inst✝¹² : IsScalarTower A K L₂
inst✝¹¹ : Algebra K L₃
inst✝¹⁰ : Algebra A L₃
inst✝⁹ : IsScalarTower A K L₃
inst✝⁸ : Algebra B L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : Algebra B₂ L₂
inst✝⁴ : IsScalarTower A B₂ L₂
inst✝³ : IsIntegralClosure B₂ A L₂
inst✝² : Algebra B₃ L₃
inst✝¹ : IsScalarTower A B₃ L₃
inst✝ : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
x : B
⊢ (galRestrict' A B B₃ (σ'.comp σ)) x = ((galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)) x

Tactic:
apply (IsIntegralClosure.equiv A (integralClosure A L₃) L₃ B₃).symm.injective

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝²⁹ : CommRing A
inst✝²⁸ : CommRing B
inst✝²⁷ : CommRing B₂
inst✝²⁶ : CommRing B₃
inst✝²⁵ : Algebra A B
inst✝²⁴ : Algebra A B₂
inst✝²³ : Algebra A B₃
inst✝²² : Field K
inst✝²¹ : Field L
inst✝²⁰ : Field L₂
inst✝¹⁹ : Field L₃
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra K L
inst✝¹⁶ : Algebra A L
inst✝¹⁵ : IsScalarTower A K L
inst✝¹⁴ : Algebra K L₂
inst✝¹³ : Algebra A L₂
inst✝¹² : IsScalarTower A K L₂
inst✝¹¹ : Algebra K L₃
inst✝¹⁰ : Algebra A L₃
inst✝⁹ : IsScalarTower A K L₃
inst✝⁸ : Algebra B L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : Algebra B₂ L₂
inst✝⁴ : IsScalarTower A B₂ L₂
inst✝³ : IsIntegralClosure B₂ A L₂
inst✝² : Algebra B₃ L₃
inst✝¹ : IsScalarTower A B₃ L₃
inst✝ : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
x : B
⊢ (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃).symm ((galRestrict' A B B₃ (σ'.comp σ)) x) =
    (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃).symm
      (((galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)) x)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L L₂ ↑σ).comp (galLift K L₂ L ↑σ.symm) = AlgHom.id K L₂

Tactic:
by simp [← galLift_comp]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L₂ L ↑σ.symm).comp (galLift K L L₂ ↑σ) = AlgHom.id K L

Tactic:
by simp [← galLift_comp]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w

Tactic:
simp_rw [normAtAllPlaces, normAtPlace_apply_of_isComplex hw]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : HasFiniteQuotients R
S : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
⊢ Finite (S ⧸ I)

Tactic:
by
    obtain hR | hR := subsingleton_or_nontrivial R
    · have : Finite S := Module.finite_of_finite R
      exact Quotient.finite _
    let J : Ideal R := Ideal.under R I
    have : Finite (R ⧸ J) := finiteQuotient <| Ideal.under_ne_bot R hI
    have : Module.Finite (R ⧸ J) (S ⧸ I) := Module.Finite.of_restrictScalars_finite R _ _
    exact Module.finite_of_finite (R ⧸ J)

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
p : Ideal R
⊢ IsUnramifiedIn S p ↔ ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P

Tactic:
refine ⟨fun h P hP hlo ↦ h P hP.isPrime hlo, fun h P hP hlo ↦ ?_⟩
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · exact isUnramifiedAt_bot
  · exact h P (hP.isMaximal hPbot) hlo

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

Goal state before:
pp: case neg
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ₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ

Tactic:
· have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
      infer_instance

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1

Tactic:
apply Ideal.count_normalizedFactors_eq <;> simpa

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
⊢ (↑I).IsPrincipal

Tactic:
let s := hf.toFinset

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
⊢ (↑I).IsPrincipal
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : ∑ i ∈ s, a M * u i • b i ∈ IsLocalization.coeSubmodule A M
⊢ False

Tactic:
mul_smul_comm

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : ∑ x ∈ s, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
⊢ False
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
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
⊢ ∀ Q ∈ (p.primesOver S).toFinset, (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)

Tactic:
intro Q

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
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
Q : Ideal S
⊢ Q ∈ (p.primesOver S).toFinset → (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_3
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ a ∈ normalizedFactors I, absNorm ((relNorm R) a) = absNorm a

Tactic:
intro Q

Goal state after:
case neg.refine_3
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
⊢ Q ∈ normalizedFactors I → absNorm ((relNorm R) Q) = absNorm Q