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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |(Algebra.norm ℚ) ((algebraMap R K) ↑d) * (Algebra.norm ℚ) x| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| =
    |(Algebra.norm ℚ) x|

Tactic:
abs_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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| * |(Algebra.norm ℚ) x| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| =
    |(Algebra.norm ℚ) x|
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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑(Ideal.absNorm (Ideal.span {r})) / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
· rw [Ideal.absNorm_span_singleton]
    simp_rw [Nat.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
    rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]

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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ y = 2 * -m * -n

Tactic:
rw [h_odd.2]

Goal state after:
case h.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ 2 * m * n = 2 * -m * -n
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w, f w = (∏ w, f ↑w) * ∏ w, f ↑w

Tactic:
rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]

Goal state after:
K : Type u_1
inst✝² : Field K
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w, f w = (∏ w, f ↑w) * ∏ i, f ↑((Equiv.subtypeEquivRight ⋯) i)
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (↑k) (𝓞 K) ↔ ζ = 1

Tactic:
rw [mem_rootsOfUnity]
  refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
  refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
  · exact orderOf_dvd_of_pow_eq_one h
  · have hζ : ζ ∈ torsion K := by
      rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
      exact ⟨k, k.prop, h⟩
    rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
    apply orderOf_dvd_natCard

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
⊢ torsionOrder K = 2

Tactic:
let := Fintype.ofFinite (torsion K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
⊢ torsionOrder K = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
h₁ : ∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)
h₂ :
  ∀ (a : InfinitePlace K) (b : a.IsComplex),
    a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
⊢ |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

pp: case refine_3
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsReal
⊢ w x < ↑(f w)

pp: case refine_4
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)

Tactic:
· simpa [if_true] using h₂ w₀.val w₀.prop

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsReal
⊢ w x < ↑(f w)

case refine_4
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
⊢ IsTotallyReal ↥E ↔ E ≤ maximalRealSubfield K

Tactic:
refine ⟨fun h ↦ h.le_maximalRealSubfield, fun h ↦ ?_⟩

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
⊢ IsTotallyReal ↥E
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
⊢ volume (convexBodyLT' K f w₀) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
      rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
      congr 2
      · refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
        rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]
      · simpa only [ite_true] using vol_box (f w₀)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).det.im = 0 ↔ Even (nrComplexPlaces K)

Tactic:
← conj_eq_iff_im,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (starRingEnd ℂ) (basisMatrix K).det = (basisMatrix K).det ↔ Even (nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑↑((-1) ^ nrComplexPlaces K) = 1 ↔ Even (nrComplexPlaces K)

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).det ≠ 0

Tactic:
· simp only [Units.val_pow_eq_pow_val, Units.val_neg, Units.val_one, Int.reduceNeg,
        Int.cast_pow, Int.cast_neg, Int.cast_one]
      rw [neg_one_pow_eq_one_iff_even (by norm_num)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).det ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ volume (convexBodySum K B) = 0

Tactic:
by
  obtain hB | hB := lt_or_eq_of_le hB
  · suffices convexBodySum K B = ∅ by rw [this, measure_empty]
    ext x
    refine ⟨fun hx => ?_, fun h => h.elim⟩
    rw [Set.mem_ofPred] at hx
    linarith [convexBodySumFun_nonneg x]
  · suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]
    ext
    rw [convexBodySum, Set.mem_ofPred_eq, Set.mem_singleton_iff, hB, ← convexBodySumFun_eq_zero_iff]
    exact (convexBodySumFun_nonneg _).ge_iff_eq'

Goal state after:
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
⊢ ENNReal.ofReal ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / ↑(finrank ℚ K).factorial) =
    ↑(convexBodySumFactor K)

Tactic:
ofReal_div_of_pos
      (Nat.cast_pos.mpr (Nat.factorial_pos _)),

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal (∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / ENNReal.ofReal ↑(finrank ℚ K).factorial =
    ↑(convexBodySumFactor K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K)

Tactic:
refine Fintype.equivOfCardEq ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥↑↑I) = Fintype.card (Free.ChooseBasisIndex ℤ (𝓞 K))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹

Tactic:
simp_rw [minkowskiBound, convexBodySumFactor,
        volume_fundamentalDomain_fractionalIdealLatticeBasis,
        volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal,
        toReal_ofNat, mixedEmbedding.finrank, mul_assoc]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ (unmixedEmbeddingsOver L v.embedding).ncard + (mixedEmbeddingsOver L v.embedding).ncard = Fintype.card (L →ₐ[K] ℂ)

Tactic:
← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ (unmixedEmbeddingsOver L v.embedding ∪ mixedEmbeddingsOver L v.embedding).ncard = Fintype.card (L →ₐ[K] ℂ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I

Tactic:
refine Fintype.equivOfCardEq ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Fintype.card (ChooseBasisIndex ℤ (𝓞 K)) = Fintype.card (ChooseBasisIndex ℤ ↥↑↑I)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) ^ 2 * ↑m.factorial ^ 2 =
    ↑((m + 1) * m.factorial) ^ 2 * ↑m ^ (m * 2) * ((↑m + 1) / ↑m) ^ (2 * m)

Tactic:
simp [field, div_pow]

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ (↑m + 1) ^ (m * 2) * ↑m ^ (2 * m) = ↑m ^ (m * 2) * (↑m + 1) ^ (2 * m)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ volume (⇑(negAt s).symm '' plusPart A) = volume (plusPart A)

Tactic:
ContinuousLinearEquiv.image_symm_eq_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ volume (⇑(negAt s) ⁻¹' plusPart A) = volume (plusPart A)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ volume (⇑(negAt s) '' plusPart A) = volume (plusPart A)

Tactic:
by
  rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]

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✝³ : Module.Finite ℤ R
inst✝² : CharZero R
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsIntegral R S
𝔭 : Ideal R
⊢ IsUnramifiedIn S 𝔭 ↔ ∀ (𝔓 : Ideal S) [𝔓.IsPrime], 𝔓.LiesOver 𝔭 → e(𝔓|R) = 1

Tactic:
refine ⟨fun hunr 𝔓 _ hP ↦ hunr.ramificationIdx_eq_one hP, fun h 𝔓 _ hP ↦ ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : Module.Finite ℤ R
inst✝² : CharZero R
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsIntegral R S
𝔭 : Ideal R
h : ∀ (𝔓 : Ideal S) [𝔓.IsPrime], 𝔓.LiesOver 𝔭 → e(𝔓|R) = 1
𝔓 : Ideal S
x✝ : 𝔓.IsPrime
hP : 𝔓.LiesOver 𝔭
⊢ IsUnramifiedAt R 𝔓
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case h₁
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) ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
have : Function.Surjective
      (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R R (R ⧸ I) s).symm.toLinearMap) :=
    (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)

Goal state after:
case h₁
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) ⋯
hf : Function.Surjective ⇑f
this : Function.Surjective ⇑(LinearMap.lTensor (R ⧸ I) f ∘ₗ ↑(finsuppScalarRight R R (R ⧸ I) ↥s).symm)
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S

Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ Fintype.card (Free.ChooseBasisIndex R S)
Module: Mathlib.RingTheory.LocalRing.Quotient

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

Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ finrank R S ≤ Fintype.card (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS))
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : absNorm (under ℤ I) = 0
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}

pp: case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}

Tactic:
· have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ := by
      refine Set.eq_empty_of_forall_notMem ?_
      intro x ⟨hx₁, hx₂⟩
      rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
      rw [Nat.pos_iff_ne_zero] at hx₁
      exact hx₁ hx₂
    rw [h, this, Nat.sInf_empty]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
h₁ : absNorm (under ℤ I) ∈ {d | 0 < d ∧ ↑d ∈ I}
h₀ : sInf {d | 0 < d ∧ ↑d ∈ I} < absNorm (under ℤ I)
h₂ : ↑(sInf {d | 0 < d ∧ ↑d ∈ I}) ∈ I
⊢ False

Tactic:
rw [← cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast] at h₂

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
h₁ : absNorm (under ℤ I) ∈ {d | 0 < d ∧ ↑d ∈ I}
h₀ : sInf {d | 0 < d ∧ ↑d ∈ I} < absNorm (under ℤ I)
h₂ : absNorm (under ℤ I) ∣ sInf {d | 0 < d ∧ ↑d ∈ I}
⊢ False
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, ↑d ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ absNorm (under ℤ I) ∣ Fintype.card (S ⧸ I)

Tactic:
simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]

Goal state after:
case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, ↑d ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ AddMonoid.exponent (S ⧸ I) ∣ Fintype.card (S ⧸ I)
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✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
⊢ Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1) = (discr K).natAbs

Tactic:
FractionalIdeal.coe_one,

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
⊢ Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype 1) = (discr K).natAbs