mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ ↑‖μ s‖₊ ≤ ↑μ.bound

Tactic:
← enorm_eq_nnnorm

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ ‖μ s‖ₑ ≤ ↑μ.bound
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖(B x) (μ s)‖ₑ ≤ ↑‖B‖₊ * μ.variation s * ‖x‖ₑ

Tactic:
le_opENorm,

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖B x‖ₑ * ‖μ s‖ₑ ≤ ↑‖B‖₊ * μ.variation s * ‖x‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖B x‖ₑ * ‖μ s‖ₑ ≤ ↑‖B‖₊ * μ.variation s * ‖x‖ₑ

Tactic:
le_opENorm,

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖B‖ₑ * ‖x‖ₑ * ‖μ s‖ₑ ≤ ↑‖B‖₊ * μ.variation s * ‖x‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖B‖ₑ * ‖x‖ₑ * μ.variation s ≤ ↑‖B‖₊ * μ.variation s * ‖x‖ₑ

Tactic:
← enorm_eq_nnnorm

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
x : E
⊢ ‖B‖ₑ * ‖x‖ₑ * μ.variation s ≤ ‖B‖ₑ * μ.variation s * ‖x‖ₑ
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mpr
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
⊢ (x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x) → x ∈ s

Tactic:
rintro (⟨hx, hx'⟩ | ⟨x, ⟨⟨hx, hx'⟩, _⟩, m, rfl⟩)

Goal state after:
case mpr.inl
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s

case mpr.inr
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
right✝ : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
m : ℕ
⊢ x + m * p ∈ s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
l : ℕ
ts : Fin l → presburger[[↑A]].Term α
ih : ∀ (a : Fin l), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : presburger.Functions l
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inl f) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
| inl f =>

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs

Tactic:
induction φ with
  | falsum => exact Iff.rfl
  | equal => exact Iff.rfl
  | rel => exact Iff.rfl
  | imp f1 f2 h1 h2 =>
    intros
    rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
  | all _ h =>
    intros
    rw [realize_all, toPrenex, realize_all]
    exact forall_congr' fun a => h

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndepOn ℚ (⇑toRatVec) s

Tactic:
LinearIndepOn,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndependent ℚ fun (x : ↑s) ↦ toRatVec ↑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
⊢ L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

Tactic:
refine Iff.intro ?_ ?_ <;>
  · intro h f m
    obtain ⟨g, h1, h2⟩ := h f.symm m
    exact ⟨g.symm, h1, monotone_symm h2⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

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

Tactic:
classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : Language.order.Structure M
inst✝⁴ : LE M
inst✝³ : Language.order.OrderedStructure M
N : Type u_1
inst✝² : Language.order.Structure N
inst✝¹ : LE N
inst✝ : Language.order.OrderedStructure N
F : Type u_2
⊢ ∀ (φ : M ↪o N) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M), RelMap r (⇑φ ∘ x) ↔ RelMap r x

Tactic:
simp only [order.forall_relations, order.relation_eq_leSymb, relMap_leSymb, Fin.isValue,
    Function.comp_apply, RelEmbedding.map_rel_iff, implies_true]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this : LinearOrder M := Language.order.linearOrderOfModels M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
let := Language.order.linearOrderOfModels N

Goal state after:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝ : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder N := Language.order.linearOrderOfModels N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this : LinearOrder M := Language.order.linearOrderOfModels M
⊢ Nonempty (↑N ↪[Language.order] M)

Tactic:
let := Language.order.linearOrderOfModels N

Goal state after:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this✝ : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder ↑N := Language.order.linearOrderOfModels ↑N
⊢ Nonempty (↑N ↪[Language.order] M)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: ⊢ Language.order.dlo.ModelType

Tactic:
by
      letI : Language.order.Structure ℚ := orderStructure ℚ
      exact Theory.ModelType.of _ ℚ

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv (E' 3)

Tactic:
E',

Goal state after:
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv {2, 3, 3}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv (E' 4)

Tactic:
E',

Goal state after:
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv {2, 3, 4}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv (E' 5)

Tactic:
E',

Goal state after:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv {2, 3, 5}
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case e'_2.a.h₁
n i : ℕ
h : i ≤ n
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ n - x✝ = i ↔ n - i = x✝

Tactic:
grind [choose_symm]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case e'_3
n i : ℕ
h : i ≤ n
⊢ n.choose i = n.choose (n - i)

Tactic:
grind [choose_symm]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n ∣ n#

Tactic:
have : (∏ p ∈ n.primeFactors, p) ∣ (∏ p ∈ range (n + 1) with p.Prime, p) :=
    Finset.prod_dvd_prod_of_subset _ _ _ (by grind [le_of_dvd])

Goal state after:
n : ℕ
hn : Squarefree n
this : ∏ p ∈ n.primeFactors, p ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli k = if n + 1 = 1 then 1 else 0

Tactic:
cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
by_cases! hb : b < 2

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

case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n p : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ (p + 1) =
    ∑ i ∈ range (p + 1 + 1), bernoulli' i * ↑((p + 1 + 1).choose i) * ↑n ^ (p + 1 + 1 - i) / ↑(p + 1).succ

Tactic:
let f i := bernoulli i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ

Goal state after:
case succ
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ (p + 1) =
    ∑ i ∈ range (p + 1 + 1), bernoulli' i * ↑((p + 1 + 1).choose i) * ↑n ^ (p + 1 + 1 - i) / ↑(p + 1).succ
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := ⋯
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ j < d

Tactic:
exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ((Icc 1 n).lcm id).factorization p = log p n

Tactic:
Finset.factorization_lcm (fun _ _ ↦ by grind)

Goal state after:
n p : ℕ
hp : Prime p
⊢ ((Icc 1 n).sup fun a ↦ (id a).factorization p) = log p n
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
⊢ ↑(A i₁ % b - A i₀ % b).natDegree < ↑?m.556

Tactic:
convert! deg_lt
    rw [degree_eq_natDegree h']; rfl

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.inl
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
hi_eq : i + 2 = 2 * m
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
simp only [hi_eq]

Goal state after:
case succ.succ.inl
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
hi_eq : i + 2 = 2 * m
⊢ (Rat.padicValuation p) (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1)) ≤ 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
obtain ⟨t', ht'⟩ := ih (Fin.tail A)

Goal state after:
case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
⊢ 1 ≤ x

Tactic:
have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
this : 1 ≤ x ^ (↑k)⁻¹
⊢ 1 ≤ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑(⌊log x / log 2⌋₊ - 1) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)

Tactic:
gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n * log 2 ≤ log (↑n + 1) + ψ ↑n

Tactic:
psi_eq_log_lcmUpto,

Goal state after:
n : ℕ
⊢ ↑n * log 2 ≤ log (↑n + 1) + log ↑n.lcmUpto
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ FunctionField F K ↔ FiniteDimensional Ft K

Tactic:
by
  let e := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
  have : ∀ (c) (x : K), e c • x = c • x := by
    intro c x
    rw [Algebra.smul_def, Algebra.smul_def]
    congr
    refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c
    refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
      simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
  constructor <;> intro h
  · let b := Module.finBasis F⟮X⟯ K
    exact (b.mapCoeffs e this).finiteDimensional_of_finite
  · let b := Module.finBasis Ft K
    refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite
    intro c x; convert! (this (e.symm c) x).symm; simp only [e.apply_symm_apply]

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

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr (m + (k + 1)) - x.appr m

Tactic:
rw [← add_assoc]
    dsimp [appr]
    split_ifs with h
    · exact ih
    rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
    apply dvd_add _ ih
    apply dvd_mul_of_dvd_left
    apply pow_dvd_pow _ (Nat.le_add_right m k)

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,

Goal state after:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (embeddingsMatrixReindex K E (⇑pb.basis) e).det ^ 2 = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(x.appr n) = 0

Tactic:
zmod_congr_of_sub_mem_span n x _ 0 _ h,

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑0 = 0

p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,
    embeddingsMatrixReindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow]
  congr; ext i
  rw [← prod_pow]

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

Goal state before:
pp: case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist x ↑(x.appr n) < ε

Tactic:
dist_eq_norm

Goal state after:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ < ε