mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S

Tactic:
let ⟨A, A_closure⟩ := S_fg

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
h_dom : f.dom = ⊤
h_cod : f.cod = ⊤
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Tactic:
by
  rcases f with ⟨dom, cod, g⟩
  cases h_dom
  cases h_cod
  rfl

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ y ∈ closure hs.periods, hs.base + y = x) →
    hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)

Tactic:
rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ x ∈ s ↔ hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)

Tactic:
classical
  nth_rw 1 [hs.eq_base_vadd_closure_periods]
  simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
  constructor
  · rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
  · intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
M_cg : Structure.CG L M
N_cg : Structure.CG L N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
by
  rcases M_cg with ⟨X, X_count, X_gen⟩
  rcases N_cg with ⟨Y, Y_count, Y_gen⟩
  have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
  have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
  have _ : Countable (↑Y : Type _) := by simpa only [countable_coe_iff]
  have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _
  let D : Sum X Y → Order.Cofinal (FGEquiv L M N) := fun p ↦
    Sum.recOn p (fun x ↦ ext_dom.definedAtLeft x) (fun y ↦ ext_cod.definedAtRight y)
  let S : ℕ →o M ≃ₚ[L] N :=
    ⟨Subtype.val ∘ (Order.sequenceOfCofinals g D),
      (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩
  let F := @DirectLimit.partialEquivLimit L M N _ _ ℕ _ _ _ S
  have _ : X ⊆ F.dom := by
    intro x hx
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)
    exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this
  have _ : Y ⊆ F.cod := by
    intro y hy
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inr ⟨y, hy⟩)
    exact cod_le_cod
      (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this
  have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
  have cod_top : F.cod = ⊤ := by rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
  refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩
  convert! le_partialEquivLimit S 0
  rw [toEquivOfEqTop_toEmbedding]
  apply Embedding.toPartialEquiv_toEmbedding

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K →
    ∃ M, Countable ↑M ∧ L.age ↑M = K

Tactic:
· rintro ⟨Kn, _, cq, hfg, hp, jep⟩
    obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep
    exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ (Std.Refl fun x y ↦ x ≤ y) ∧ IsTrans M fun x y ↦ x ≤ y

Tactic:
exact ⟨inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
rintro ⟨p, hp⟩

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
p : T.CompleteType α
hp : p ∈ {p | S ⊆ ↑p}
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith φ)ᶜ

Tactic:
by rw [← typesWith_not]; exact isOpen_typesWith _

Goal state after:
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: k l m n : ℕ
hm : k.IsAlmostPrime m
hn : l.IsAlmostPrime n
⊢ k + Ω n = k + l

Tactic:
hn.2

Goal state after:
k l m n : ℕ
hm : k.IsAlmostPrime m
hn : l.IsAlmostPrime n
⊢ k + l = k + l
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

Tactic:
intro p k hp

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, Λ i = Real.log ↑(p ^ k)
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p = 0

Tactic:
← map_natCast f,

Goal state after:
case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ f ↑p = 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
obtain hb | hb := le_or_gt 1 b
  · have : 1 ≤ ⌊b⌋₊ := (Nat.one_le_floor_iff _).mpr hb
    nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _), sum_cons, ← Icc_add_one_left_eq_Ioc,
      Icc_eq_cons_Ioc (by lia), sum_cons]
    rw [zero_add, ← Nat.floor_one (R := ℝ),
      sum_mul_eq_sub_sub_integral_mul c zero_le_one hb hf_diff hf_int, Nat.floor_one, Nat.cast_one,
      Icc_eq_cons_Ioc zero_le_one, sum_cons, show 1 = 0 + 1 by rfl, Nat.Ioc_succ_singleton,
      zero_add, sum_singleton, hc, mul_zero, zero_add]
    ring
  · simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff (n + 1)) (bernoulliPowerSeries A * (exp A - 1)) = (coeff (n + 1)) X

Tactic:
simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
    coeff_one, coeff_exp, map_sub, factorial, if_pos, cast_succ, cast_mul,
    sub_zero, add_eq_zero, if_false, one_ne_zero, and_false, ← map_mul, ← map_sum]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (algebraMap ℚ A) (bernoulli (n + 1) / ((↑n + 1) * ↑n !)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal n, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if n + 1 = 1 then 1 else 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ↑(π n) * log ↑n

Tactic:
← primesLE_card_eq_primeCounting,

Goal state after:
n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ↑(#n.primesLE) * log ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ ↑p ^ Nat.log p n ≤ ↑n

Tactic:
exact_mod_cast pow_log_le_self p hn

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝³ : k₁ ≤ N
a✝² : p₁ ≠ 0
a✝¹ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
⊢ ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
k₂

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝³ : k₁ ≤ N
a✝² : p₁ ≠ 0
a✝¹ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ : ℕ
⊢ ∀ (b : ℕ), k₂ ≠ 0 → k₂ ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = b ^ k₂ → k₁ = k₂ ∧ p₁ = b
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : 0 < k
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
have hfilter : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) = ∑ v ∈ range p, (v : ℚ) ^ (2 * k) := by
    cases p <;> simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]
  rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,
    show 2 * k + 1 - 2 * k = 1 by lia]
  push_cast
  field_simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x ≤ log 4 * x + 2 * √x * log x

Tactic:
calc
  _ = ψ x - θ x + θ x := by ring
  _ ≤ 2 * x.sqrt * x.log + log 4 * x := by
    gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)
  _ = _ := by ring

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : ∀ (a : F[X]), (algebraMap F[X] K) a = 0 → a = 0
p : F[X]
hp : ↑((algebraMap F[X] ↥(ringOfIntegers F K)) p) = 0
⊢ p = 0

Tactic:
exact hinj p hp

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

Goal state before:
pp: case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1

Tactic:
apply lt_of_le_of_lt (Padic.nonarchimedean _ _)

Goal state after:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ 1 = (log ↑n)⁻¹ * a n

Tactic:
have : log n ≠ 0 := log_ne_zero_of_pos_of_ne_one (mod_cast h.pos) (mod_cast h.ne_one)

Goal state after:
case pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
this : log ↑n ≠ 0
⊢ 1 = (log ↑n)⁻¹ * a n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: | (fun x ↦ √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
arg 2; ext; rw [← mul_one_div, mul_comm]

Goal state after:
x✝ : ℝ
| 1 / log 2 ^ 2 * √x✝
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y

Tactic:
rintro rfl _
    rfl

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

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'

Tactic:
rintro rfl _
    rfl

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

Goal state before:
pp: d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im

Tactic:
by
  obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
  rw [mul_comm] at Hre Him
  refine ⟨⟨re, im⟩, ?_, ?_⟩
  · rw [smul_val, ← Hre, ← Him]
  · rw [Int.isCoprime_iff_gcd_eq_one, H1]

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

Goal state before:
pp: case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

pp: case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0

Tactic:
· exact ha

Goal state after:
case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := ↑x - ↑z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg

Tactic:
Int.subNatNat_eq_coe

Goal state after:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := ↑x - ↑z, im := ↑w - ↑y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(y + 1) }
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Tactic:
have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)

Goal state after:
case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 (n + 1) % xn a1 n)

Tactic:
lem2 (n + 1) (Nat.lt_succ_self _) j2n,

Goal state after:
case refl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (n + 1)))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inl
ξ : ℚ
hq₀ : 0 < ↑ξ.den
h : |ξ * ↑ξ.den - ↑ξ.num| < 1 / ↑ξ.den
⊢ ξ.den ≤ ξ.den

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.ExpLog

Goal state before:
pp: α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ Summable fun n ↦ log (1 - f n)

Tactic:
have hg : DifferentiableAt ℂ (fun z ↦ log (1 - z)) 0 := by
    have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane
    fun_prop
  have : (fun z ↦ log (1 - z)) =O[𝓝 0] id := by
    simpa only [sub_zero, log_one] using! hg.isBigO_sub
  exact this.comp_summable hsum

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹

Tactic:
obtain ⟨Hv, Hv'⟩ := aux₀ (zero_lt_two.trans_le hv)

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹

Tactic:
refine prod_congr rfl fun p hp ↦ ?_

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : p ∈ {p ∈ s | Nat.Prime p}
⊢ ∑' (n : ℕ), f (p ^ n) = (1 - f p)⁻¹
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: case isTrue
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : k = 0
⊢ 0 ≤ 0

Tactic:
exact le_rfl

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₂ : IsOpen S := isOpen_lt continuous_const continuous_re

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
⊢ (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ r

Tactic:
have := (P.hg_top (-(r + P.k))).comp_tendsto tendsto_inv_nhdsGT_zero

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
this : ((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) =O[𝓝[>] 0] ((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹)
⊢ (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ Integrable (fun t ↦ ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Tactic:
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc]

Goal state after:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
indicator_of_mem (mem_Ioo.mpr ⟨div_pos one_pos hx, this⟩),

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f (1 / x) - (P.ε * ↑((1 / x) ^ (-P.k))) • P.g₀ = (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
ofReal_mul,

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / (↑π * ↑(q i)) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))

Tactic:
mul_assoc (3 * π)

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * (↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖) ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))