mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x + ∑ x_1, (-hs.floor x x_1).toNat • toRatVec ↑x_1 - ∑ x_1, (hs.floor x x_1).toNat • toRatVec ↑x_1 =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
← sub_add_eq_add_sub,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - ∑ x_1, (hs.floor x x_1).toNat • toRatVec ↑x_1 + ∑ x_1, (-hs.floor x x_1).toNat • toRatVec ↑x_1 =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝) • toRatVec ↑x✝ +
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝

Tactic:
rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| (hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝ • hs.basis x✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
this : Order.sequenceOfCofinals g D (Encodable.encode ⟨x, hx⟩ + 1) ∈ D ⟨x, hx⟩
⊢ x ∈ ↑F.dom

Tactic:
exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (⟨x, hx⟩ : X) + 1)) this

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ CG L (DirectLimit G f)

Tactic:
by
  refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩
  · exact Set.countable_iUnion fun i => Set.Countable.image (Classical.choose_spec (h i).out).1 _
  · rw [eq_top_iff, Substructure.closure_iUnion]
    simp_rw [← Embedding.coe_toHom, Substructure.closure_image]
    rw [le_iSup_iff]
    intro S hS x _
    let out := Quotient.out (s := DirectLimit.setoid G f)
    refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩
    · rw [(Classical.choose_spec (h (out x).1).out).2]
      trivial
    · simp only [out, Embedding.coe_toHom, DirectLimit.of_apply, Sigma.eta, Quotient.out_eq]

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ ⇑(Equiv.prodComm α β) '' ↑f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm p ∈ f

Tactic:
Equiv.image_eq_preimage_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ ⇑(Equiv.prodComm α β).symm ⁻¹' ↑f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm p ∈ f
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ ⇑(Equiv.prodComm α β) '' ↑f
⊢ (Equiv.prodComm α β).symm q ∈ f

Tactic:
Equiv.image_eq_preimage_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ ⇑(Equiv.prodComm α β).symm ⁻¹' ↑f
⊢ (Equiv.prodComm α β).symm q ∈ f
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ ⇑(Equiv.prodComm β α) '' ↑↑f'

Tactic:
Equiv.image_eq_preimage_symm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ ⇑(Equiv.prodComm β α).symm ⁻¹' ↑↑f'
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι t₁ t₂ → deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k = deriv f x * ∑ k ∈ Icc 0 n, c k

Tactic:
filter_upwards [sumlocc c n] with t h h'

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.188 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.188 n, c k
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ i ∈ a.divisors, Λ i = Real.log ↑a
hb : ∑ i ∈ b.divisors, Λ i = Real.log ↑b
⊢ ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢

Goal state after:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑(a * b)
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
have aux2 : b ≤ ⌊b⌋₊ + 1 := (Nat.lt_floor_add_one _).le

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ pderivFun i (↑f * ↑g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
← coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ pderivFun i ↑(f * g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + g * (pderiv i) f) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
← coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + g * (pderiv i) f) = ↑(f * (pderiv i) g) + ↑g * ↑((pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + g * (pderiv i) f) = ↑(f * (pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
← coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + g * (pderiv i) f) = ↑(f * (pderiv i) g) + ↑(g * (pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
⊢ f = g

Tactic:
ext n
  by_cases h : n = 0
  · rw [h, coeff_zero_eq_constantCoeff, hc]
  obtain ⟨i, hi : n i ≠ 0⟩ := ne_iff.mp h
  have : single i 1 ≤ n := fun j ↦ by
    by_cases hj : j = i <;> grind [single_eq_same, single_eq_of_ne]
  have e := congr(coeff (n - single i 1) $(hD i))
  rwa [coeff_pderiv, coeff_pderiv, tsub_add_cancel_of_le this, coe_tsub, Pi.sub_apply,
    single_eq_same, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hi), Nat.cast_one, sub_add_cancel,
    mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul, smul_right_inj hi] at e

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ f.coeff (n✝ + 1) * (↑n✝ + 1) = (Polynomial.derivative f).coeff n✝

Tactic:
Polynomial.coeff_derivative

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ f.coeff (n✝ + 1) * (↑n✝ + 1) = f.coeff (n✝ + 1) * (↑n✝ + 1)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_iff_of_odd hn, or_iff_left]
    · congr! with p m
      rw [and_iff_right_of_imp]
      rintro rfl
      contrapose! h1
      cases Nat.lt_one_iff.mp h1
      apply pow_zero
    · rintro ⟨p, m, -, -, -, rfl⟩
      simp [← Nat.not_even_iff_odd] at hn

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n m : ℕ
a✝ : n ≤ m
p : ℕ
⊢ p ∈ n.primesLE → p ∈ m.primesLE

Tactic:
simp [mem_primesLE]

Goal state after:
n m : ℕ
a✝ : n ≤ m
p : ℕ
⊢ p ≤ n → Prime p → p ≤ m ∧ Prime p
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H : ∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Tactic:
sum_eq_add_sum_sdiff_singleton_of_mem h₁

Goal state after:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
⊢ ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 =
    0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ x * (2 * x) ^ √(2 * x) / 4 ^ (x * (1 / 3)) ≤ 1

Tactic:
mul_one_div,

Goal state after:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3) ≤ 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! * (1 / ↑(q - m + 1)!) * ↑n ^ (q - m + 1)

Tactic:
mul_one_div,

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! / ↑(q - m + 1)! * ↑n ^ (q - m + 1)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
⊢ 0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (h.card ε ^ 0).succ → Fin 0 → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin 0), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
_hε

Goal state after:
case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
⊢ ∀ {b : R},
    b ≠ 0 →
      ∀ (A : Fin (h.card ε ^ 0).succ → Fin 0 → R),
        ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin 0), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (n + 1)), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
intro ε hε b hb A

Goal state after:
case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (n + 1)), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j

pp: case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₁)

Tactic:
· simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h

Goal state after:
case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₁)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
⊢ Summable fun n ↦ f ↑n * c n

Tactic:
refine Summable.congr_atTop (summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1
    h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_) hg₁ hg₂) ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖if k = 0 then 0 else c k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖if k = 0 then 0 else c k‖ -
      ∫ (t : ℝ) in Set.Ioc ↑1 ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖if k = 0 then 0 else c k‖

case refine_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
⊢ (fun n ↦ f ↑n * if n = 0 then 0 else c n) =ᶠ[atTop] fun n ↦ f ↑n * c n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p

Tactic:
by
  rw [theta, sum_filter, sum_filter, ← add_sum_Ioc_eq_sum_Icc] <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
⊢ ∃ i j k, (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0

Tactic:
by
    by_contra! h
    obtain ⟨i⟩ := bS.index_nonempty
    apply bS.ne_zero i
    apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
    ext j k
    simp [h]

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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊ ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)

Tactic:
grw [← Nat.le_ceil]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den.Coprime p
hcop_rest : (∑ i ∈ vonStaudtPrimes k with i ≠ p, 1 / ↑i).den.Coprime p
hcop :
  p.Coprime (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ i ∈ vonStaudtPrimes k with i ≠ p, 1 / ↑i).den
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q).den

Tactic:
exact (Nat.Prime.coprime_iff_not_dvd Fact.out).1 hcop

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ x.zmodRepr ≠ 0

Tactic:
ne_eq,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ ¬x.zmodRepr = 0