mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)) =
    1

Tactic:
refine multiplicity_eq_of_emultiplicity_eq_some (le_antisymm ?_ ?_)

Goal state after:
case refine_1
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)) ≤
    ↑1

case refine_2
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ ↑1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
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
⊢ (galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)}),
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime, inertiaDegIn_eq_of_not_dvd p K hn]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ‖∑ x ∈ s, (canonicalEmbedding K) (α x)‖ ≤ ∑ i ∈ s, ‖(canonicalEmbedding K) (α i)‖

Tactic:
apply norm_sum_le_of_le

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ∀ b ∈ s, ‖(canonicalEmbedding K) (α b)‖ ≤ ‖(canonicalEmbedding K) (α b)‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ house (↑c * α) = ↑c * house α

Tactic:
house_eq_sup',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ ↑(univ.sup' ⋯ fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * house α
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ ↑(univ.sup' ⋯ fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * house α

Tactic:
house_eq_sup',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ ↑(univ.sup' ⋯ fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * ↑(univ.sup' ⋯ fun φ ↦ ‖φ α‖₊)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f (↑z.num / ↑z.den) = g (↑z.num / ↑z.den)

Tactic:
map_div₀,

Goal state after:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f ↑z.num / f ↑z.den = g (↑z.num / ↑z.den)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f ↑z.num / f ↑z.den = g (↑z.num / ↑z.den)

Tactic:
map_div₀,

Goal state after:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f ↑z.num / f ↑z.den = g ↑z.num / g ↑z.den
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ x✝¹ • (toMixed K) x✝² ∈ fundamentalCone K

Tactic:
smul_mem_iff_mem h.ne'

Goal state after:
case convert_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ (toMixed K) x✝² ∈ fundamentalCone K
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f (↑x.num / ↑x.den) ^ c = g (↑x.num / ↑x.den)

Tactic:
map_div₀,

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ (f ↑x.num / f ↑x.den) ^ c = g (↑x.num / ↑x.den)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ (f ↑x.num / f ↑x.den) ^ c = g (↑x.num / ↑x.den)

Tactic:
map_div₀,

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ (f ↑x.num / f ↑x.den) ^ c = g ↑x.num / g ↑x.den
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
hξ : ¬ξ K x = 0
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
funext_iff,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
hξ : ¬∀ (x_1 : β), ξ K x x_1 = 0 x_1
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
exact tendsto_mul_cofinite_nhds_zero hf hg

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
⊢ Fintype.card (α × (K →+* ℂ)) < Fintype.card (β × (K →+* ℂ))

Tactic:
rwa [hfinp, hfinq]

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℤ_[p] E
inst✝ : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ ‖mahlerTerm a n‖ ≤ ‖a‖

Tactic:
rw [ContinuousMap.norm_le_of_nonempty]
    refine fun _ ↦ (norm_smul_le _ _).trans <| mul_le_of_le_one_left (norm_nonneg _) (norm_le_one _)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
a✝ : E
n : ℕ
x : ℤ_[p]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ ‖{ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ }, map_add' := ⋯,
          map_smul' := ⋯, invFun := fun a ↦ mahlerSeries ⇑a, left_inv := ⋯, right_inv := ⋯ }
        f‖ =
    ‖f‖

Tactic:
simp only [LinearEquiv.coe_mk, ← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm]
    apply le_antisymm
    · exact BoundedContinuousFunction.norm_le_of_nonempty.mpr
        (fun n ↦ norm_fwdDiff_iter_apply_le 1 f 0 n)
    · rw [← (hasSum_mahler f).tsum_eq]
      refine (norm_tsum_le _).trans (ciSup_le fun n ↦ ?_)
      refine le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)
      simp [(hasSum_mahler f).tsum_eq]

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs

Tactic:
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩

Goal state after:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < (eval (↑b) (cyclotomic (k + 1) ℤ)).natAbs
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ (n + 1)).y - (a ^ n).y

Tactic:
zpow_add,

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n * a ^ 1).y - (a ^ n).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ^ 2 ≤ a.x ^ 2

Tactic:
sq_le_sq,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ |a₁.x| ≤ |a.x|
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ^ 2 ≤ a.y ^ 2

Tactic:
sq_le_sq,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a₁.y| ≤ |a.y|
Module: Mathlib.NumberTheory.Pell

Goal state before:

Tactic:
a.x * (d * (a.y * a₁.y))
    _ = d * a.y * (a.x * a₁.y) := by ring
    _ ≤ d * a.y * (a.y * a₁.x) := by have := x_mul_y_le_y_mul_x h hax hay; have := h.d_pos; gcongr
    _ = (a.x ^ 2 - 1) * a₁.x := by rw [← a.prop_y]; ring
    _ < a.x * (a.x * a₁.x) := by linarith [h.1]

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

Goal state before:
pp: case f
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 q : K[X]
x✝ : q ≠ 0
h0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
h1 : v ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) < 1
⊢ {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty

Tactic:
| f p q =>

Goal state after:
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⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hπᵥ : ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne = a * b
hb : ¬IsUnit b
⊢ 1 ≤ v ↑a

Tactic:
by
  set πᵥ := degree_lt_wf.min _ hne
  have hda : a.degree < πᵥ.degree := by
    have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb
    simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢
    norm_cast
    simpa using hbpos
  have hlea := imp_not_comm.mp (degree_lt_wf.not_lt_min _) hda
  grind

Goal state after:
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
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Tactic:
have hπirr : Irreducible π := irreducible_min_polynomial_valuation_lt_one_and_ne_zero hne

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] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
⊢ 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 inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
refine Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

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

Goal state before:
pp: case h
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
a✝ : d ∈ s.prodPrimes.divisors
⊢ muPlus d * rem d ≤ |muPlus d * rem d|

Tactic:
exact le_abs_self (muPlus d * s.rem d)

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
congr! 2 with d1 hd1 d2 hd2

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ ↑(a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2) = ↑k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k

Tactic:
push_cast [sq_abs]

Goal state after:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ZMod p
hk : -1 = k * k
⊢ ∃ k', ∃ (_ : k' < p), ↑k' = k

Tactic:
exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
exfalso

Goal state after:
case inr
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
⊢ False
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case prime_mul
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ q ∈ n.primeFactors, q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) → ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

pp: case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
· rintro ⟨x, y, h⟩
    by_cases hxy : x = 0 ∧ y = 0
    · exact ⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul],
        ⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩
    · have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
      obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
      exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring,
        ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩

Goal state after:
case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
i : ℕ
val✝¹ : S ⧸ P ^ e
property✝¹ : val✝¹ ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
val✝ : S ⧸ P ^ e
property✝ : val✝ ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
h : (p.powQuotSuccInclusion P i) ⟨val✝¹, property✝¹⟩ = (p.powQuotSuccInclusion P i) ⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
Subtype.ext_iff

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
i : ℕ
val✝¹ : S ⧸ P ^ e
property✝¹ : val✝¹ ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
val✝ : S ⧸ P ^ e
property✝ : val✝ ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
h : ↑((p.powQuotSuccInclusion P i) ⟨val✝¹, property✝¹⟩) = ↑((p.powQuotSuccInclusion P i) ⟨val✝, property✝⟩)
⊢ ↑⟨val✝¹, property✝¹⟩ = ↑⟨val✝, property✝⟩
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)

Tactic:
refine (this.and_frequently hC).mono ?_

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∀ (x_1 : ℕ),
    (C < ↑x_1 ^ (p - q) ∧ 1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-q)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x)

Tactic:
rw [mul_comm]; exact h.mul_nat hn

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.extent = d.extent
⊢ c = d

Tactic:
obtain ⟨s₁, t₁, rfl, _⟩ := c
  obtain ⟨s₂, t₂, rfl, _⟩ := d
  subst h
  rfl

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent ⊂ d.intent ↔ d < c

Tactic:
ssubset_iff_subset_not_subset,

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent ⊆ d.intent ∧ ¬d.intent ⊆ c.intent ↔ d < c
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.left ∧ ¬x ≤ a)) ↔ c ≤ principal a

Tactic:
not_and,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ x ∈ c.left, ¬¬x ≤ a) ↔ c ≤ principal a
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.right ∧ ¬a ≤ x)) ↔ c.intent ⊆ (principal a).intent

Tactic:
not_and,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ x ∈ c.right, ¬¬a ≤ x) ↔ c.intent ⊆ (principal a).intent
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (↑(n + 1) * (T / ↑(n + 1)))

Tactic:
mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)

Goal state after:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal T
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
⊢ I.IsPrime

Tactic:
rw [isPrime_iff_mem_or_mem]
  intro x y
  contrapose!
  rintro ⟨hx, hynI⟩ hxy
  apply hynI
  let J := I ⊔ principal x
  have hJuniv : (J : Set P) = Set.univ :=
    IsMaximal.maximal_proper (lt_sup_principal_of_notMem ‹_›)
  have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
  rw [coe_sup_eq] at hyJ
  rcases hyJ with ⟨a, ha, b, hb, hy⟩
  rw [hy]
  refine sup_mem ha (I.lower (le_inf hb ?_) hxy)
  rw [hy]
  exact le_sup_right

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ _root_.sSupIndep {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}

Tactic:
rw [sSupIndep_iff_pairwiseDisjoint]
      intro a ha a' ha' h
      grind [Partition.eq_or_disjoint, Disjoint.inf_left, Disjoint.inf_left']

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
by
  rw [← @type_ne_zero_iff o.ToType, type_toType]

Goal state after: