mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n ↦ χ ↑n) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
a : ℝ
⊢ ∃ p, 0 < p ∧ sinKernel ↑a =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
| H a =>

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : 0 < c
⊢ False

Tactic:
exact (by positivity : 0 < c ^ n).not_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
        hn.pow_neg hb

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
| DifferentiableAt ℂ
    (fun s ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Tactic:
enter [2, s, 2]

Goal state after:
a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ 1 ^ n + 1 ^ n ≠ 1 ^ n

Tactic:
simp only [one_pow, Nat.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
have hF t (ht : 0 < t) :
      HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) := by
    refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
    rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
let c (n : ℤ) : ℂ := -I * cexp (2 * π * I * a * n) / 2
  have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
    simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
  have hF t (ht : 0 < t) :
      HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) := by
    refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
    rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
  have h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re := by
    simp_rw [hc, div_right_comm]
    apply Summable.div_const
    apply Summable.of_nat_of_neg <;>
    simpa
  rw [completedSinZeta, (isStrong_hurwitzOddFEPair _).symm_Λ_eq]
  refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun
    fun n ↦ ?_
  simp [Int.sign_eq_sign, ← Int.cast_abs] -- non-terminal simp OK when `ring` follows
  ring

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
rcases Int.emod_two_eq_zero_or_one a0 with hap | hap

Goal state after:
case inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1

case inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 1
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
p : Primes
k : ℕ
⊢ (χ ↑↑p * ↑↑p ^ (-s)) ^ (k + 1) / (↑k + 1) =
    χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1)))

Tactic:
have : Complex.log p ≠ 0 := mod_cast p.prop.log_ne_zero

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
p : Primes
k : ℕ
this : Complex.log ↑↑p ≠ 0
⊢ (χ ↑↑p * ↑↑p ^ (-s)) ^ (k + 1) / (↑k + 1) =
    χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1)))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ z * z - y * y

Tactic:
rw [← Int.natCast_dvd] at hpy hpz

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Tactic:
rw [WithBot.add_lt_add_iff_right hb]

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree < a.degree
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
⊢ a = 0 ∨ IsUnit a

Tactic:
rw [or_iff_not_imp_left]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
⊢ ¬a = 0 → IsUnit a
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
⊢ IsCoprime b c

Tactic:
apply rot_coprime heq <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hbc : IsCoprime b c
⊢ IsCoprime c a

Tactic:
apply rot_coprime heq <;> assumption

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
have :=
      (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
        (Subfield.toIntermediateField K this).toSubalgebra

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : (K.toIntermediateField this✝).toSubalgebra = ⊥ ∨ (K.toIntermediateField this✝).toSubalgebra = ⊤
⊢ K = ofRealHom.fieldRange ∨ K = ⊤
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hca : ca.natDegree = 0
⊢ d + 1 = 0

Tactic:
by
        rw [← eq_d, eq_deg_a, hca, zero_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ x, 2 = 2 * ∑ x, 1

Tactic:
Finset.mul_sum,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ x, 2 = ∑ i, 2 * 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = #{φ | mk φ = w}

Tactic:
← Fintype.card_subtype

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = card { x // mk x = w }
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✝² : IsTotallyReal K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F K
w : InfinitePlace F
⊢ w.IsReal

Tactic:
obtain ⟨W, rfl⟩ : ∃ W : InfinitePlace K, W.comap (algebraMap F K) = w := comap_surjective w
    exact IsReal.comap _ (IsTotallyReal.isReal W)

Goal state after:
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
h : E ≤ maximalRealSubfield K
x✝ : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
⊢ IsTotallyReal ↥E

Tactic:
have : IsScalarTower E (maximalRealSubfield K) K := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x✝ : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
⊢ IsTotallyReal ↥E
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
E F : Subfield K
hE : IsTotallyReal ↥E
hF : IsTotallyReal ↥F
⊢ IsTotallyReal ↥E ∧ F ≤ maximalRealSubfield K

Tactic:
← isTotallyReal_iff_le_maximalRealSubfield

Goal state after:
F✝ : Type u_1
inst✝³ : Field F✝
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal ↥E
hF : IsTotallyReal ↥F
⊢ IsTotallyReal ↥E ∧ IsTotallyReal ↥F
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
B : ℝ≥0
⊢ volume
      {a | |(Complex.measurableEquivRealProd.symm a).re| < 1 ∧ |(Complex.measurableEquivRealProd.symm a).im| < ↑B ^ 2} =
    4 * ↑B ^ 2

Tactic:
Complex.measurableEquivRealProd_symm_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume {a | |a.1| < 1 ∧ |a.2| < ↑B ^ 2} = 4 * ↑B ^ 2
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
⊢ (∏ i, volume (ball 0 ↑(f ↑i))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
Real.volume_ball

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
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

Tactic:
rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ ∀ (x y : (K →+* ℂ) → ℂ),
    (fun w ↦ ((x + y) (↑w).embedding).re, fun w ↦ (x + y) (↑w).embedding) =
      (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding) +
        (fun w ↦ (y (↑w).embedding).re, fun w ↦ y (↑w).embedding)

Tactic:
simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]

Goal state after:
K : Type u_1
inst✝ : Field K
⊢ ∀ (x y : (K →+* ℂ) → ℂ),
    ((fun w ↦ (x (↑w).embedding).re + (y (↑w).embedding).re) =
        (fun w ↦ (x (↑w).embedding).re) + fun w ↦ (y (↑w).embedding).re) ∧
      (fun w ↦ x (↑w).embedding + y (↑w).embedding) = (fun w ↦ x (↑w).embedding) + fun w ↦ y (↑w).embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, |c| * ↑x_1.mult * (normAtPlace x_1) x = |c| * ∑ w, ↑w.mult * (normAtPlace w) x

Tactic:
Finset.mul_sum,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, |c| * ↑x_1.mult * (normAtPlace x_1) x = ∑ i, |c| * (↑i.mult * (normAtPlace i) x)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inl
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
e : Nat.card ↥(Stab w) = 1
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

Tactic:
rw [e]

Goal state after:
case inl
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
e : Nat.card ↥(Stab w) = 1
⊢ ¬1 = 1 ↔ 1 = 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inr
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
e : Nat.card ↥(Stab w) = 2
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

Tactic:
rw [e]

Goal state after:
case inr
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
e : Nat.card ↥(Stab w) = 2
⊢ ¬2 = 1 ↔ 2 = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-∑ w, ‖x.1 w‖ + -2 * ∑ w, ‖x.2 w‖) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)

Tactic:
Finset.mul_sum,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-∑ w, ‖x.1 w‖ + ∑ i, -2 * ‖x.2 i‖) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (index K) = finrank ℚ K

Tactic:
← mixedEmbedding.finrank K,

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (index K) = finrank ℝ (mixedSpace 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
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ card (InfinitePlace K) = card (InfinitePlace k) * finrank k K

Tactic:
InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K),

Goal state after:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ {w | InfinitePlace.IsUnramifiedIn K w}.card * finrank k K +
      {w | InfinitePlace.IsUnramifiedIn K w}ᶜ.card * (finrank k K / 2) =
    card (InfinitePlace k) * finrank k K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case 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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
⊢ ℚ⟮↑a⟯ = ⊤

Tactic:
exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! if_neg h_ne ▸ h_le w h_ne) (Or.inr h_le₀.1)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(euclidean.integerLattice K)

Tactic:
rw [euclidean.integerLattice]
  infer_instance

Goal state after:
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
P : Ideal B
hPp : P.IsPrime
hp : 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✝¹¹ : Algebra A C
inst✝¹⁰ : Algebra B C
inst✝⁹ : Nonempty ↑(P.primesOver 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
GBC : Type u_6
inst✝³ : Group GBC
inst✝² : Finite GBC
inst✝¹ : MulSemiringAction GBC C
inst✝ : IsGaloisGroup GBC B C
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.inertiaDeg A * P.inertiaDegIn C = p.inertiaDegIn C

Tactic:
inertiaDegIn_eq_inertiaDeg p Q GAC,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : 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✝¹¹ : Algebra A C
inst✝¹⁰ : Algebra B C
inst✝⁹ : Nonempty ↑(P.primesOver 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
GBC : Type u_6
inst✝³ : Group GBC
inst✝² : Finite GBC
inst✝¹ : MulSemiringAction GBC C
inst✝ : IsGaloisGroup GBC B C
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.inertiaDeg A * P.inertiaDegIn C = Q.inertiaDeg A
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg.refine_2
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 : IsTorsionFree B E
a : E
ha : ¬minpoly K ((algebraMap B L) x) = 0 ∧ (aeval a) (minpoly K ((algebraMap B L) x)) = 0
⊢ (aeval a) (minpoly K ((algebraMap B L) x)) = 0

Tactic:
exact ha.2

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
⊢ ({I | Submodule.cardQuot I ≤ B} \ {⊥}).Finite

Tactic:
suffices {I | Submodule.cardQuot I ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I} from
    (t.finite_toSet.biUnion fun x hx ↦ finite_setOfPred_mem x (by grind)).subset this

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
⊢ {I | I.cardQuot ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I}
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁸ : CommRing A
B : Type u_2
inst✝⁷ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁶ : CommRing K
inst✝⁵ : Algebra A K
inst✝⁴ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝³ : CommRing L
inst✝² : Algebra B L
inst✝¹ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
⊢ ∃ x, ∃ (_ : x ∈ I), ¬(IsLocalization.map L f hf) x = 0

Tactic:
obtain ⟨x, hx₁, hx₂⟩ : ∃ x ∈ I, x ≠ 0 := by simpa [ne_eq, eq_zero_iff] using hI

Goal state after:
A : Type u_1
inst✝⁸ : CommRing A
B : Type u_2
inst✝⁷ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁶ : CommRing K
inst✝⁵ : Algebra A K
inst✝⁴ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝³ : CommRing L
inst✝² : Algebra B L
inst✝¹ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
x : K
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ ∃ x, ∃ (_ : x ∈ I), ¬(IsLocalization.map L f hf) x = 0
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝¹ : Nontrivial (R ⧸ I)
this✝ : IsLocalRing (R ⧸ I)
this : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : ⊥.jacobson ^ n = 0
⊢ ∃ n, p ^ n ≤ I

Tactic:
have : (maximalIdeal R).map (Ideal.Quotient.mk I) = maximalIdeal (R ⧸ I) := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp [sup_eq_left.mpr (le_maximalIdeal hI)]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝² : Nontrivial (R ⧸ I)
this✝¹ : IsLocalRing (R ⧸ I)
this✝ : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : ⊥.jacobson ^ n = 0
this : Ideal.map (Ideal.Quotient.mk I) p = maximalIdeal (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I