mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_8
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
hF : Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)

Tactic:
exact hF

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F✝ : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
s : Set X
hF : Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)

Tactic:
exact hF

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A s : Set ℕ
⊢ A.Definable₁ presburger s ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
rw [Definable₁, definable_iff_isSemilinearSet,
    ← isSemilinearSet_image_iff (LinearEquiv.funUnique (Fin 1) ℕ ℕ), ← preimage_ofPred_eq]
  simp only [LinearEquiv.funUnique_apply, Function.eval, Fin.default_eq_zero, ofPred_mem_eq]
  rw [image_preimage_eq s fun x => ⟨![x], rfl⟩, Nat.isSemilinearSet_iff_ultimately_periodic]

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ T ⊨ᵇ ∀' φ ⇔ ∀' ψ

Tactic:
ModelsBoundedFormula,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (∀' φ ⇔ ∀' ψ).Realize v xs
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ T ⊨ᵇ ∃' φ ⇔ ∃' ψ

Tactic:
ModelsBoundedFormula,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (∃' φ ⇔ ∃' ψ).Realize v xs
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ T ⊨ᵇ ∼φ ⇔ ∼ψ

Tactic:
ModelsBoundedFormula,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (∼φ ⇔ ∼ψ).Realize v xs
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ T ⊨ᵇ φ ⟹ φ' ⇔ ψ ⟹ ψ'

Tactic:
ModelsBoundedFormula,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (φ ⟹ φ' ⇔ ψ ⟹ ψ').Realize v xs
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀' φ✝).Realize (⇑f ∘ v) (⇑f ∘ xs) → (∀' φ✝).Realize v xs

Tactic:
simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)

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 : ι → ℕ
| toRatVec x - toRatVec hs.base =
    ∑ x_1,
      (Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1) • toRatVec ↑x_1 +
        ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1)

Tactic:
enter [2, 2, _]

Goal state after:
ι : 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✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝¹ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange },
                    ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝

Tactic:
PartialEquiv.toEmbedding

Goal state after:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝¹ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange },
                    ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
⊢ (Quotient.mk' '' L.age M).Countable

Tactic:
classical
  refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : L.IsOrdered
⊢ ∀ ⦃φ : L.Sentence⦄, φ ∈ L.preorderTheory → BoundedFormula.IsUniversal φ

Tactic:
simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq]
  exact ⟨leSymb.isUniversal_reflexive, leSymb.isUniversal_transitive⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn :
  ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding) ((PM.comp NP).equivRange n) =
    (g.toEmbedding.comp (PM.comp NP).toHom.range.subtype) ((PM.comp NP).equivRange n)
⊢ ↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) =
    ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)

Tactic:
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply,
    Substructure.coe_subtype, Embedding.equivRange_apply] at hgn

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) =
    ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) =
    ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)

Tactic:
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑((Substructure.inclusion ⋯) ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) =
    ↑((Substructure.inclusion ⋯) (QM.equivRange (NQ n)))
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
    ext
    simp [subset_def]

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ Set.univ ≠ ∅ ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Tactic:
Ne,

Goal state after:
L : Language
T : L.Theory
α : Type w
⊢ ¬Set.univ = ∅ ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:

Tactic:
(p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
    _ = 1 := by norm_num

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case hf
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖⁻¹ • f x) (μ.withDensity fun x ↦ ‖f x‖ₑ)

Tactic:
apply AEStronglyMeasurable.mono_ac (withDensity_absolutelyContinuous _ _)
      exact hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable

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

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n.choose x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)

Tactic:
div_eq_iff,

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n.choose x) = 1 / (↑x ! * ↑(n - x)!) * ↑n !

case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! ≠ 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) • bernoulli k = (monomial n) (↑n + 1)

Tactic:
simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm,
    Finset.sum_Ico_eq_sum_range]
  simp only [add_tsub_cancel_left, zero_add, map_add]
  simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
  conv_lhs =>
    apply_congr
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
  simp_rw [← sum_smul, Nat.sub_zero]
  rw [sum_range_succ_comm]
  simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left,
    choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
    map_add, range_one, mul_one]
  refine sum_eq_zero ?_
  intro x hx
  have hx1 : n + 1 - x ≠ 1 := by grind
  simp [_root_.sum_bernoulli, hx1]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ (∏ p ∈ n.primesLE, p).primeFactors = n.primesLE

Tactic:
exact primeFactors_prod fun _ hp ↦ prime_of_mem_primesLE hp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (aeval t) ((monomial n) ↑(n + 1))

Tactic:
cast_add,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (aeval t) ((monomial n) (↑n + ↑1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = log (∏ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, ↑i)

Tactic:
log_prod (fun p hp ↦ mod_cast (mem_filter.mp hp).2.pos.ne')

Goal state after:
x : ℝ
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ∑ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, log ↑i
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
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log (↑(Fintype.card Fq) ^ (A i₁ % b - A i₀ % b).natDegree) < log (↑(Fintype.card Fq) ^ b.natDegree * ε)

Tactic:
log_mul (pow_ne_zero _ q_pos'.ne') hε.ne',

Goal state after:
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
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log (↑(Fintype.card Fq) ^ (A i₁ % b - A i₀ % b).natDegree) < log (↑(Fintype.card Fq) ^ b.natDegree) + log ε
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mpr
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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ (distinctElems bS adm) i - (distinctElems bS adm) j ≠ 0

Tactic:
Ne,

Goal state after:
case mpr
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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i - (distinctElems bS adm) j = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
⊢ ∃ M, ∀ N ≥ M, ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
use ⌊log (x ^ (n : ℝ)⁻¹) / log 2⌋₊

Goal state after:
case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
⊢ ∀ N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊, ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
psi_eq_sum_theta' this hN,

Goal state after:
case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ∑ n_1 ∈ Icc 1 N, θ ((x ^ (↑n)⁻¹) ^ (1 / ↑n_1)) = ∑ k ∈ Icc 1 N, b x (n * k)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_2.refine_2
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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A (Classical.choose ⋯).succ % b)) < cardPowDegree b • ε
⊢ False

Tactic:
Ne,

Goal state after:
case refine_2.refine_2
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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : ¬j₀.succ = j₁.succ
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A (Classical.choose ⋯).succ % b)) < cardPowDegree b • ε
⊢ False
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁸ : EuclideanDomain R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁸ : IsScalarTower R K L
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
⊢ Ideal.span {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁸ : EuclideanDomain R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁸ : IsScalarTower R K L
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
⊢ ¬Ideal.span {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
div_le_iff₀ (log_pos (mod_cast h)),

Goal state after:
case inr.inr
n : ℕ
h : 1 < n
⊢ ↑n * log 2 - log (↑n + 1) ≤ ↑(π n) * log ↑n
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ↑p ^ (-↑(k + 1)) ≤ ↑p ^ (-↑k)

Tactic:
by gcongr <;> simp [‹Fact p.Prime›.1.one_le]

Goal state after: