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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < x.1 w

Tactic:
rw [← this]

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < a.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : y ∈ normLeOne K
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ x ∈ normLeOne K

Tactic:
rw [mem_normLeOne, ← normAtAllPlaces_mem_fundamentalCone_iff, ← norm_normAtAllPlaces,
    ← mem_normLeOne] at hy₁ ⊢

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : mixedSpaceOfRealSpace (normAtAllPlaces y) ∈ normLeOne K
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ normLeOne K
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
x✝ : InfinitePlace K
⊢ x✝ ≠ w' ↔ f.symm x✝ ≠ f.symm w'

Tactic:
by simp [f]

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

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
hv : v = w.comap (algebraMap K L)
h : IsUnramified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

Tactic:
rw [h.finrank_eq_one v, hv, h.eq, mul_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑expMap ((completeBasis K) w₀) = fun x ↦ Real.exp 1

Tactic:
by
  ext
  simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ mixedEmbedding.norm
      (mixedSpaceOfRealSpace (↑expMap ((completeBasis K).equivFun.symm fun i ↦ if i = w₀ then 0 else x i))) =
    1

Tactic:
← expMapBasis_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMapBasis fun i ↦ if i = w₀ then 0 else x i)) = 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
suffices ∀ {j}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1) by
    grind [Associated.trans, Associated.symm]

Goal state after:
n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
⊢ ↑expMapBasis (↑expMapBasis.symm x) ∈ normAtAllPlaces '' normLeOne K ↔ ↑expMapBasis.symm x ∈ paramSet K

Tactic:
simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_ofPred_eq, expMapBasis_nonneg,
      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
⊢ (∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1) ∧ ↑expMapBasis.symm x w₀ ≤ 0 ↔
    ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
h : 2 < p
⊢ 2 ∉ span {hζ.toInteger - 1}

Tactic:
rw [mem_span_singleton]
  rw [← pow_one p] at hK hζ
  exact hζ.toInteger_sub_one_not_dvd_two h.ne'

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec n ℚ K
  let τ := IsFractionRing.stabilizerHom Gal(K/ℚ) (Ideal.span {(p : ℤ)}) P
     (ℤ ⧸ span {(p : ℤ)}) (𝓞 K ⧸ P) ⟨σ, hσ⟩
  have : CharP (ℤ ⧸ span {(p : ℤ)}) p := ringChar.of_eq <| Int.ringChar_idealQuot p
  have : Finite (𝓞 K ⧸ P) := Ring.HasFiniteQuotients.finiteQuotient (NeZero.ne P)
  obtain ⟨i, hi⟩ := FiniteField.exists_forall_apply_eq_pow (ℤ ⧸ span {(p : ℤ)}) p (𝓞 K ⧸ P) τ
  refine ⟨i, ?_⟩
  have h₀ : IsPrimitiveRoot (Ideal.Quotient.mk P hζ.toInteger) n := by
    refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_
    rw [← pow_inertiaDeg p]
    exact Nat.Coprime.pow_left _ hn
  have h₁ := IsFractionRing.stabilizerHom_apply_apply_mk Gal(K/ℚ) (Ideal.span {(p : ℤ)}) P
      (ℤ ⧸ span {(p : ℤ)}) (𝓞 K ⧸ P) ⟨σ, hσ⟩ hζ.toInteger
  simp only [Algebra.algebraMap_self, RingHomCompTriple.comp_apply] at h₁
  specialize hi (Ideal.Quotient.mk P hζ.toInteger)
  rwa [h₁, Int.card_ideal_quot, galEquivZMod_smul_of_pow_eq n _ _
    (hζ.toInteger_isPrimitiveRoot.pow_eq_one), map_pow, (h₀.isOfFinOrder (NeZero.ne _)).pow_inj_mod,
    ← h₀.eq_orderOf, ← ZMod.natCast_eq_natCast_iff', Nat.cast_pow, ← ZMod.coe_unitOfCoprime p hn,
    ← Units.val_pow_eq_pow_val, ZMod.natCast_zmod_val, ← Units.ext_iff, eq_comm] at hi

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Tendsto (fun s ↦ (↑s - 1) * dedekindZeta K ↑s) (𝓝[>] 1) (𝓝 ↑(dedekindZeta_residue K))

Tactic:
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg _ ?_
    (fun _ ↦ Nat.cast_nonneg _)
  refine ((Ideal.tendsto_norm_le_div_atTop₀ K).comp tendsto_natCast_atTop_atTop).congr fun n ↦ ?_
  simp only [Function.comp_apply, Nat.cast_le, ← Nat.cast_sum]
  congr
  rw [← add_left_inj 1, ← card_norm_le_eq_card_norm_le_add_one,
    show Finset.Icc 1 n = Finset.Ioc 0 n from Finset.Icc_succ_left_eq_Ioc _ _,
    show 1 = Nat.card {I : Ideal (𝓞 K) // absNorm I = 0} by simp [Ideal.absNorm_eq_zero_iff],
    Finset.sum_Ioc_add_eq_sum_Icc (n.zero_le),
    ← Finset.card_preimage_eq_sum_card_image_eq (fun k _ ↦ finite_setOfPred_absNorm_eq k)]
  simp [Set.coe_eq_subtype]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁸ : NeZero n
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1) ↔ (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker

Tactic:
SetLike.le_def,

Goal state after:
n : ℕ
inst✝⁸ : NeZero n
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ ⦃x : (ZMod n)ˣ⦄, x ∈ (ZMod.unitsMap hdiv).ker → x ∈ (toUnitHom χ).ker
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * (↑(finrank ℚ K) * c₂ K) * A) ^ (↑p / (↑q - ↑p))

Tactic:
← mul_assoc (q : ℝ),

Goal state after:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * ↑(finrank ℚ K) * c₂ K * A) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Valued.v ↑p = 1 / ↑p

Tactic:
by
  rw [← map_natCast (algebraMap ℚ_[p] (PadicAlgCl p))]
  ext
  rw [valuation_coe, norm_extends, Padic.norm_p, one_div, NNReal.coe_inv,
    NNReal.coe_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ 0 < (a ^ n.succ).y

Tactic:
by
  induction n with
  | zero => simp only [pow_one, hay]
  | succ n ih => rw [pow_succ']; exact y_mul_pos hax hay (x_pow_pos hax _) ih

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z' - a = 0

Tactic:
rw [← this]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
⊢ ∃ a, IsFundamental a

Tactic:
classical
  -- to avoid having to show that the predicate is decidable
  let x₁ := Nat.find P
  obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
  refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩
  rw [x_mk]
  have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
  have hb'' := hb
  rw [hb'] at hb ⊢
  norm_cast at hb ⊢
  refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩
  rw [← hb', sq_abs]
  exact b.prop

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval (newton_seq n)) (Polynomial.derivative F)‖

Tactic:
newton_seq_gen,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖↑(newton_seq_aux hnorm (n + 1)) - newton_seq n‖ =
    ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval (newton_seq n)) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
rw [← zpow_zero a₁, eq_comm] at hn₁

Goal state after:
case inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ 0 = -a₁ ^ (n₂ * n₁ - 1)
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖↑(newton_seq_aux hnorm (n + 1)) - newton_seq n‖ =
    ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval (newton_seq n)) (Polynomial.derivative F)‖

Tactic:
newton_seq_gen,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖↑(newton_seq_aux hnorm (n + 1)) - ↑(newton_seq_aux hnorm n)‖ =
    ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) F‖ /
      ‖(Polynomial.aeval ↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Tactic:
set π := πᵥ

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ beattySeq r (⌈(↑j + 1) / r⌉ - 1) = j

Tactic:
rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add]

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑⌈(↑j + 1) / r⌉ < (↑j + 1) / r + 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∀ i ∈ d.primeFactors, 0 < s.nu i

Tactic:
intro p hpd

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < s.nu p
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ ∀ i ∈ d.primeFactors, s.nu i < 1

Tactic:
intro p hpd

Goal state after:
case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : p ∈ d.primeFactors
⊢ s.nu p < 1
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
⊢ ∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0

Tactic:
obtain ⟨a, hag, j, hjs, hgI⟩ := Ideal.exist_integer_multiples_notMem hRS s g hj's hj'g

Goal state after:
case h
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)
j : ι
hjs : j ∈ s
hgI : a * g j ∉ ↑(RingHom.ker f)
⊢ ∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ ∑ x ∈ n.divisors, ∑ i ∈ n.divisors, weights i * weights x =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0

Tactic:
congr! 1 with d1 hd1

Goal state after:
case neg.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ ∑ i ∈ n.divisors, weights i * weights d1 =
    ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
by
  rcases hp.1.eq_two_or_odd' with (rfl | hodd)
  · use 1, 0, 1; simp
  rcases Nat.sq_add_sq_zmodEq p (-1) with ⟨a, b, ha, hb, hab⟩
  rcases Int.modEq_iff_dvd.1 hab.symm with ⟨k, hk⟩
  rw [sub_neg_eq_add, mul_comm] at hk
  have hk₀ : 0 < k := by
    refine pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)
    rw [← hk]
    positivity
  lift k to ℕ using hk₀.le
  refine ⟨a, b, k, Nat.cast_pos.1 hk₀, ?_, mod_cast hk⟩
  replace hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p := mod_cast hk
  refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_
  · exact (mul_le_mul' le_rfl ha).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)
  · exact (mul_le_mul' le_rfl hb).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)
  · exact lt_of_le_of_ne hp.1.two_le (hodd.ne_two_of_dvd_nat (dvd_refl _)).symm
  · exact hp.1.pos

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
⊢ ∀ (x : HeightOneSpectrum K[X]), v.IsEquiv (valuation K⟮X⟯ x) → ∃ x_1, ∃ (_ : v.IsEquiv (valuation K⟮X⟯ x_1)), ¬x_1 = x

Tactic:
intro pw hw

Goal state after:
case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
pw : HeightOneSpectrum K[X]
hw : v.IsEquiv (valuation K⟮X⟯ pw)
⊢ ∃ x, ∃ (_ : v.IsEquiv (valuation K⟮X⟯ x)), ¬x = pw
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ mainSum (lambdaSquared w) =
    ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
calc mainSum (lambdaSquared w)
      = ∑ d ∈ divisors s.prodPrimes, ∑ d1 ∈ divisors d, ∑ d2 ∈ divisors d,
          if d = d1.lcm d2 then w d1 * w d2 * s.nu d else 0 := ?caseA
    _ = ∑ d ∈ divisors s.prodPrimes, ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes,
          if d = d1.lcm d2 then w d1 * w d2 * s.nu d else 0 := sum_divisors_lambda_sq_larger_sum _ _
    _ = ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes,
          s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ := ?caseB

Goal state after:
case caseA
s : BoundingSieve
w : ℕ → ℝ
⊢ mainSum (lambdaSquared w) =
    ∑ d ∈ s.prodPrimes.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * s.nu d else 0

case caseB
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ d ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if d = d1.lcm d2 then w d1 * w d2 * s.nu d else 0) =
    ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
⊢ p % 4 ≠ 3

Tactic:
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd (Nat.dvd_of_mem_primeFactors hp) hs
  rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h
  have : Fact p.Prime := ⟨Nat.prime_of_mem_primeFactors hp⟩
  exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsSquare (-1)

Tactic:
obtain ⟨u, v, huv⟩ : IsCoprime x n := by
    have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
    rw [show y ^ 2 = n + -1 * x ^ 2 by lia] at hc2
    exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
  have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
    linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
  refine ⟨u * y, ?_⟩
  conv_rhs => tactic => norm_cast
  rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
  exact (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case mpr
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: p : ℂ[X]
s : ℂ
⊢ s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) p = -(cexp (-s) * eval s (sumIDeriv p)) + eval 0 (sumIDeriv p)

Tactic:
by
  rw [← intervalIntegral.integral_const_mul,
    intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun x hx => hasDerivAt_cexp_mul_sumIDeriv p s x)
      (ContinuousOn.intervalIntegrable (by fun_prop))]
  simp

Goal state after: