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

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : oddKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
rw [← isBigO_norm_left] at hv' ⊢

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖oddKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : sinKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ sinKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
rw [← isBigO_norm_left] at hv' ⊢

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖sinKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
n : ℕ
⊢ (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n * I))) / 2 / ↑n ^ s =
    (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s

Tactic:
rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
hc : h.IsClassified
⊢ ⋯.IsClassified

Tactic:
obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc <;> use k * l, m, n <;> grind

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

Goal state before:
pp: case left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)

pp: case right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs

Tactic:
· apply And.intro ha (And.intro hb _)
    rw [heq]
    exact (neg_sq c).symm

Goal state after:
case right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inr.inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
· use a0, b0, -c0, neg_of_minimal hf, hc
    exact neg_pos.mpr h1

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)

Tactic:
← mul_div_assoc,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)

Tactic:
← mul_div_assoc,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * completedSinZeta a s / (s + 1).Gammaℝ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)

Tactic:
← mul_div_assoc,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)

Tactic:
← mul_div_assoc,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * completedHurwitzZetaOdd a s / (s + 1).Gammaℝ
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
⊢ a ∈ primeFactors b ↔ a ∈ normalizedFactors b

Tactic:
simp only [primeFactors, Multiset.mem_toFinset]

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

Goal state before:
pp: p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
⊢ False

Tactic:
by simp at h

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (norm K) ((algebraMap (𝓞 K) (𝓞 L)) x) = x ^ finrank K L

Tactic:
rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]

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

Goal state before:
pp: case refine_2
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ a.natDegree = (contract (ringChar k) a).natDegree * ringChar k

Tactic:
rw [← natDegree_expand, ← heq]

Goal state after:
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 ℚ) (↑d • x)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|

Tactic:
Algebra.smul_def,

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 * x)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬(mk φ).IsReal

Tactic:
rw [not_isReal_iff_isComplex]

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ (mk φ).IsComplex
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ ↑w.mult

Tactic:
by
  rw [← Nat.cast_one, Nat.cast_le]
  exact mult_pos

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #((if w.embedding ∈ Finset.univ then {w.embedding} else ∅) ∪ {a | a = star w.embedding}) = w.mult

Tactic:
Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #((if w.embedding ∈ Finset.univ then {w.embedding} else ∅) ∪
        if ComplexEmbedding.conjugate w.embedding ∈ Finset.univ then {ComplexEmbedding.conjugate w.embedding} else ∅) =
    w.mult
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ |↑((RingOfIntegers.norm ℚ) x)| = |1| ↔ IsUnit ((RingOfIntegers.norm ℚ) x)

Tactic:
abs_eq_abs,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ ↑((RingOfIntegers.norm ℚ) x) = 1 ∨ ↑((RingOfIntegers.norm ℚ) x) = -1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)
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 ≤ |(Algebra.norm ℤ) a|

Tactic:
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:
by
  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]
  exact Equiv.ext (ComplexEmbedding.involutive_conjugate K).toPerm_involutive

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (K →+* ℂ) = Fintype.card (ChooseBasisIndex ℤ (𝓞 K))

Tactic:
rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ (w : InfinitePlace K), w ≠ w₁ → Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w = f w

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∏ w, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B

Tactic:
· exact fun w hw => Function.update_of_ne hw _ f

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∏ w, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
obtain ⟨a', eq_a⟩ := gcd_dvd_left a b

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
a' : k[X]
eq_a : a = gcd a b * a'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
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
⊢ IsTotallyReal ↥(algebraMap ℚ K).fieldRange

Tactic:
exact IsTotallyReal.ofRingEquiv (algebraMap ℚ K).rangeRestrictFieldEquiv

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    ∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K) x_1 = x

Tactic:
Set.mem_image

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ (∃ x_1 ∈ ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))), (canonicalEmbedding K).toIntAlgHom.toLinearMap x_1 = x) ↔
    ∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K) x_1 = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

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

Tactic:
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.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
φ : K →+* ℂ
h : IsRamified k (mk φ)
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ

Tactic:
rw [isRamified_iff_card_stabilizer_eq_two, Nat.card_eq_two_iff] at h

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
h : ∃ x y, x ≠ y ∧ {x, y} = Set.univ
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        ∑ y,
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, y)) *
            x ((indexEquiv K) (Sum.inr (x_1, y)))

Tactic:
Fin.sum_univ_two,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x ((indexEquiv K) (Sum.inr (x_1, 0))) +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x ((indexEquiv K) (Sum.inr (x_1, 1))))
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
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hv : ∃ x, ¬(conjugate v.embedding) x = v.embedding x
⊢ ∃ x, ¬(conjugate w.embedding) x = w.embedding x

Tactic:
obtain ⟨x, hx⟩ := hv

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
x : K
hx : ¬(conjugate v.embedding) x = v.embedding x
⊢ ∃ x, ¬(conjugate w.embedding) x = w.embedding x
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case e_a.e_a.e_a.e_a.e_a
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
⊢ ↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K) = 2 * ↑(nrComplexPlaces K)

Tactic:
rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]

Goal state after:
case e_a.e_a.e_a.e_a.e_a
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
⊢ ↑(nrRealPlaces K) + 2 * ↑(nrComplexPlaces K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K) =
    2 * ↑(nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : { w // w.IsReal }
⊢ MeasurableSet {x | 0 < x.1 x✝}

Tactic:
exact measurableSet_lt measurable_const (by fun_prop)

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
⊢ ∀ (x y : ↑(p.primesOver B)), ∃ g, g • x = y

Tactic:
intro ⟨P, _, _⟩

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✝ Q : Ideal B
hPp : P✝.IsPrime
hp : P✝.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
P : Ideal B
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ ∀ (y : ↑(p.primesOver B)), ∃ g, g • ⟨P, ⋯⟩ = y
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 1 ≤ ↑N * (9 / 4)

Tactic:
← mul_div_assoc,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 1 ≤ ↑N * 9 / 4
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
⊢ ∃ I,
    ClassGroup.mk0 I = C ∧
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, h_nz, h_nm⟩ :=
    exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K (FractionalIdeal.mk0 K J)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ∃ I,
    ClassGroup.mk0 I = C ∧
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h✝ :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
h : p = 0
⊢ Ideal.comap (algebraMap ℤ (𝓞 K)) ↑⟨P, HP⟩ = ⊥

Tactic:
by simpa only [hp, submodule_span_eq, span_singleton_eq_bot]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (under ℤ P).IsPrime → _root_.Prime p
hlies : P.LiesOver (span {p})
hspan : span {↑p.natAbs} = span {p}
⊢ ↑⟨P, HP⟩ ≠ ⊥

Tactic:
simpa using HP.2

Goal state after: