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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) *
        (↑2 ^ 2 * ↑(f ↑w₀) ^ 2)) =
    (↑(convexBodyLT'Factor K) * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2

Tactic:
convexBodyLT'Factor,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) *
        (↑2 ^ 2 * ↑(f ↑w₀) ^ 2)) =
    (↑(2 ^ (nrRealPlaces K + 2) * pi ^ (nrComplexPlaces K - 1)) * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ volume (fundamentalDomain ((latticeBasis K).reindex e.symm)) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖₊

Tactic:
← norm_toNNReal,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ volume (fundamentalDomain ((latticeBasis K).reindex e.symm)) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖.toNNReal
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ‖I‖₊ = 1

Tactic:
← norm_toNNReal,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ‖I‖.toNNReal = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

Tactic:
by
  refine ⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩
  obtain ⟨σ, rfl⟩ := exists_smul_eq_of_comap_eq hv
  rwa [isUnramified_smul_iff] at H

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this✝ : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
this : ‖I‖₊ = 1
⊢ ↑‖2‖₊⁻¹ ^ nrComplexPlaces K * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)

Tactic:
← norm_toNNReal,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this✝ : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
this : ‖I‖₊ = 1
⊢ ↑‖2‖.toNNReal⁻¹ ^ nrComplexPlaces K * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : index K
⊢ ofRealHom ((mixedEmbedding.stdBasis K).toMatrix (⇑((latticeBasis K).reindex e.symm)) i✝ j✝) =
    (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝

Tactic:
Basis.toMatrix_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : index K
⊢ ofRealHom (((mixedEmbedding.stdBasis K).repr (((latticeBasis K).reindex e.symm) j✝)) i✝) =
    (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j =
    (algebraMap ℚ ℝ) ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j)

Tactic:
Basis.toMatrix_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ ((latticeBasis K).repr ((⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) j)) i =
    (algebraMap ℚ ℝ) (((integralBasis K).repr ((⇑(basisOfFractionalIdeal K I) ∘ ⇑e) j)) i)
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
B : Type u_6
B₂ : Type u_7
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing B₂
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A B₂
inst✝¹⁶ : Field K
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 B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra B₂ L₂
inst✝¹ : IsScalarTower A B₂ L₂
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
x : B
⊢ (galLift K L L₂ σ) ((algebraMap B L) x) = (algebraMap B₂ L₂) (σ x)

Tactic:
simp [galLift]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
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 B L
inst✝² : IsScalarTower A B L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (galLift K L L (AlgHom.id A B)) x✝ = (AlgHom.id K L) x✝

Tactic:
simp [galLift]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsReal
⊢ ‖(fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)).1 ⟨w, hw⟩‖ = x w

Tactic:
Real.norm_of_nonneg hx

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsReal
⊢ x w = x w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces (mixedSpaceOfRealSpace x) w = x w

Tactic:
normAtComplexPlaces_apply_isComplex ⟨w, hw⟩,

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ ‖(mixedSpaceOfRealSpace x).2 ⟨w, hw⟩‖ = x w
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
⊢ S.Finite

Tactic:
refine Set.finite_coe_iff.mp <| Finite.of_injective
    (fun ⟨F, hF⟩ ↦ (⟨(h F hF).choose, (h F hF).choose_spec.1⟩ : T)) (fun _ _ h_eq ↦ ?_)

Goal state after:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
σ τ : Gal(L/K)
Q : ↑(p.primesOver B)
⊢ (σ * τ) • Q = σ • τ • Q

Tactic:
apply Subtype.val_inj.mp

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
σ τ : Gal(L/K)
Q : ↑(p.primesOver B)
⊢ ↑((σ * τ) • Q) = ↑(σ • τ • Q)
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
Q : ↑(p.primesOver B)
⊢ 1 • Q = Q

Tactic:
apply Subtype.val_inj.mp

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
Q : ↑(p.primesOver B)
⊢ ↑(1 • Q) = ↑Q
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 := 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))
⊢ x ∣ (algebraMap A B) ((intNorm A B) x)

Tactic:
by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
this✝⁵ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
heq :
  (algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P)) =
    (algebraMap p.ResidueField P.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField)
this✝⁴ : Algebra (R ⧸ p) P.ResidueField :=
  ((algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P))).toAlgebra
this✝³ : IsScalarTower (R ⧸ p) (S ⧸ P) P.ResidueField
this✝² : IsScalarTower (R ⧸ p) p.ResidueField P.ResidueField
this✝¹ : IsGalois p.ResidueField P.ResidueField
this✝ : Module.Finite p.ResidueField P.ResidueField
this : (inertia (↥(MulAction.stabilizer G P)) P).index = Nat.card Gal(P.ResidueField/p.ResidueField)
⊢ Nat.card ↥(MulAction.stabilizer G P) = Nat.card ↥(inertia G P) * P.inertiaDeg R

Tactic:
inertiaDeg_eq p P,

Goal state after:
R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
this✝⁵ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
heq :
  (algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P)) =
    (algebraMap p.ResidueField P.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField)
this✝⁴ : Algebra (R ⧸ p) P.ResidueField :=
  ((algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P))).toAlgebra
this✝³ : IsScalarTower (R ⧸ p) (S ⧸ P) P.ResidueField
this✝² : IsScalarTower (R ⧸ p) p.ResidueField P.ResidueField
this✝¹ : IsGalois p.ResidueField P.ResidueField
this✝ : Module.Finite p.ResidueField P.ResidueField
this : (inertia (↥(MulAction.stabilizer G P)) P).index = Nat.card Gal(P.ResidueField/p.ResidueField)
⊢ Nat.card ↥(MulAction.stabilizer G P) = Nat.card ↥(inertia G P) * finrank p.ResidueField P.ResidueField
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ]

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : p = ⊥
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)

Tactic:
have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)
    rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
⊢ ↑B = 1 * ↑B

Tactic:
by rw [one_mul]

Goal state after:
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
s : Set S
⊢ Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)

Tactic:
rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

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

Goal state before:
pp: case refine_2
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 ∈ Set.Icc (-↑C) ↑C

Tactic:
rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ]

Goal state after:
case refine_2
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| ≤ ↑↑C
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: 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}
⊢ ↑B = 1 * ↑B

Tactic:
by rw [one_mul]

Goal state after: