mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

Goal state before:
pp: 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
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K w.Completion) x = completionMap ((algebraMap K v.Completion) x)

Tactic:
h,

Goal state after:
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
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K w.Completion) x = completionMap { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: 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
⊢ v.inertiaDeg w = ⊥.inertiaDeg v.Completion

Tactic:
simp only [InfinitePlace.inertiaDeg, dif_pos]

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

Goal state before:
pp: case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ ↑(E ⊔ maximalRealSubfield K) = ↑E

Tactic:
h,

Goal state after:
case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ ↑⊥ = ↑E
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |LinearMap.det
          (LinearMap.pi fun i ↦
            ↑(smulRight 1 (deriv_expMap_single i ((completeBasis K).equivFun.symm x i))) ∘ₗ LinearMap.proj i) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
LinearMap.det_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |(∏ i, LinearMap.det ↑(smulRight 1 (deriv_expMap_single i ((completeBasis K).equivFun.symm x i)))) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
            regulator K) *
        f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)

Tactic:
have : Measurable expMapBasis := (continuous_expMapBasis K).measurable

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this : Measurable ↑expMapBasis
⊢ ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
            regulator K) *
        f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
h,

Goal state after:
case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (0 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
⊢ Associated (-2) ↑p

Tactic:
h,

Goal state after:
case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
⊢ Associated (-2) ↑2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {p ^ (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
h,

Goal state after:
case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 1 + 1)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 1 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 2)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 2))
⊢ Associated 2 ↑p

Tactic:
h,

Goal state after:
case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 2)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 2))
⊢ Associated 2 ↑2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in paramSet K,
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w)) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K)))) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x ↦ y ^ i) l).sum = ∑ i ∈ Finset.range l.length, y ^ i

Tactic:
List.mapIdx_eq_zipIdx_map,

Goal state after:
T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.map
        (fun x ↦
          match x with
          | (a, i) => y ^ i)
        l.zipIdx).sum =
    ∑ i ∈ Finset.range l.length, y ^ i
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 / g ↑z.den

Tactic:
h,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ∏ x, (∑ x_1, ↑B * ↑(A x x_1)⁺ - ∑ x_1, ↑B * -↑(A x x_1)⁻ + 1) ≤ ∏ x, (↑n * max 1 ‖A‖ * ↑B + 1)

Tactic:
refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
      · have h := N_le_P_add_one A i
        rify at h
        linarith only [h]
      · simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
        gcongr with j _
        rw [posPart_add_negPart (A i j), Int.cast_abs]
        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ }) / s + s⁻¹ = ↑(Nat.card { I // absNorm I ≤ ⌊s⌋₊ }) / s

Tactic:
Ideal.card_norm_le_eq_card_norm_le_add_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ }) / s + s⁻¹ = ↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ } + 1) / s
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.mapIdx (fun x x_1 ↦ ↑n₀) L).sum = ↑n₀ * (↑(Nat.log n₀ m) + 1)

Tactic:
List.mapIdx_eq_zipIdx_map,

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.map
        (fun x ↦
          match x with
          | (a, i) => ↑n₀)
        L.zipIdx).sum =
    ↑n₀ * (↑(Nat.log n₀ m) + 1)
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fun x ↦ ‖x‖) = Valued.v.norm

Tactic:
apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)
  · exact uniformContinuous_norm
  · let S := (Valued.toNormedField ℂ_[p] NNReal).toNormedCommRing.toNormedRing.toSeminormedRing
    let := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup
    exact @uniformContinuous_norm ℂ_[p] this
  · intro x
    simp only [Valued.v.norm_def, RankOne.hom_eq_embedding]
    rw [embedding_restrict (PadicComplex.valued p).v x, valuation_extends,
      ← PadicAlgCl.valuation_coe]

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
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k

Tactic:
intro k

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n k : ℕ
⊢ k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: case refine_2
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
k : Fin #t
⊢ ∃ i, ↑((fun k ↦ W ↑(t.equivFin.symm k)) k) ⊆ ↑(U i)

pp: case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)

pp: case refine_4
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
⊢ Pairwise (Disjoint on fun k ↦ W ↑(t.equivFin.symm k))

Tactic:
· exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩

Goal state after:
case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)

case refine_4
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
⊢ Pairwise (Disjoint on fun k ↦ W ↑(t.equivFin.symm k))
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < (mk |x| |y| ⋯).x

Tactic:
rw [x_mk, ← one_lt_sq_iff_one_lt_abs, eq_add_of_sub_eq h, lt_add_iff_pos_right]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2
Module: Mathlib.NumberTheory.SelbergSieve

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

Tactic:
hd2

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
⊢ (∑ x ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ (norm a).natAbs * (norm b).natAbs = p ^ 2

Tactic:
rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = norm (a * b)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))

Tactic:
(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))

Goal state after:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ n = 0 ^ 2 * 1

Tactic:
h,

Goal state after:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ x ^ 2 + y ^ 2 = 0 ^ 2 * 1
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ n = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Tactic:
h,

Goal state after:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ x ^ 2 + y ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ 1 < ↑b

Tactic:
rw [← Int.cast_one]

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ ↑1 < ↑b
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ ↑(n - 1)! + 1 = 0

Tactic:
h,

Goal state after:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ -1 + 1 = 0
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) → Bounded r s

Tactic:
rintro ⟨b, hb⟩

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b | ¬r b a} → r b_1 b
⊢ Bounded r s
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + ↑r)

Tactic:
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  refine ⟨r.den ^ p * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
  rintro n ⟨hn, m, hne, hlt⟩
  have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
    rw [smul_eq_mul, id]
    nth_rewrite 4 [← Rat.num_div_den r]
    push_cast
    rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
  refine ⟨r.den * m + r.num * n, ?_⟩; rw [this, add_sub_add_right_eq_sub]
  refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
  have : (r.den ^ p : ℝ) ≠ 0 := by positivity
  simp [mul_rpow, mul_div_mul_left, this]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_int_iff]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
⊢ Surjective f

Tactic:
rintro ⟨b, hb⟩

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ ∃ a, f a = ⟨b, hb⟩
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
⊢ ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p

Tactic:
rintro p ⟨hA, hB⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
p : Nat.Primes
hA : A ↑p =ᵐ[μ] ∅
hB : B ↑p =ᵐ[μ] ∅
⊢ E =ᵐ[μ] C ↑p
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
⊢ f '' A.left ⊆ lowerBounds (f '' A.right)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.left
y : α
hy : y ∈ A.right
⊢ f x ≤ f y
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
⊢ f '' A.right ⊆ upperBounds (f '' A.left)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.right
y : α
hy : y ∈ A.left
⊢ f y ≤ f x
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
⊢ CountableInterFilter l

Tactic:
refine ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩
    rwa [lt_aleph_one_iff, le_aleph0_iff_set_countable]

Goal state after:
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁

Tactic:
· simpa [Filter.le_def, rcomap, SetRel.mem_image]
      using fun h t tl₂ => h _ t tl₂ Set.Subset.rfl

Goal state after: