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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
A : ∀ (i : ℕ), Measurable fun x ↦ ‖μ[(f i).indicator 1 | M] x‖ₑ
⊢ ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ.trim Mle < ∞

Tactic:
lintegral_trim Mle (A _)

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
A : ∀ (i : ℕ), Measurable fun x ↦ ‖μ[(f i).indicator 1 | M] x‖ₑ
⊢ ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: case a
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ (VectorMeasure.variation μ) r ≤ μ.totalVariation r

Tactic:
apply VectorMeasure.variation_le_of_forall_enorm_le

Goal state after:
case a
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ ∀ (E : Set X), MeasurableSet E → ‖μ E‖ₑ ≤ μ.totalVariation E
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case a
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
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
⊢ (μ.transpose B).variation ≤ C • μ.variation

pp: case a
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
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
⊢ C • μ.variation ≤ (μ.transpose B).variation

Tactic:
· apply (variation_transpose_le _ _).trans
    gcongr
    apply opNNNorm_le_bound _ _ (fun x ↦ opNNNorm_le_bound _ _ (fun y ↦ by simp [hB]))

Goal state after:
case a
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
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
⊢ C • μ.variation ≤ (μ.transpose B).variation
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case refine_2
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
⊢ ‖m'' s‖ₑ ≤ μ s

Tactic:
by_cases hs : MeasurableSet s; swap
    · simp [not_measurable _ hs]
    simp only [coe_mk, hs, ↓reduceIte, m'']
    grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul,
      lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop),
      lintegral_enorm_condExp_indicator Mle hs]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
x : M
⊢ x ∈ a +ᵥ ↑(closure ↑t) ↔ x ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))

Tactic:
simp only [mem_vadd_set, SetLike.mem_coe]

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
x : M
⊢ (∃ y ∈ closure ↑t, a +ᵥ y = x) ↔ x ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case inl
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑∅
x : ℕ
hx : x ≥ a + 1
⊢ x ∈ a +ᵥ ↑(closure ↑∅) ↔ x + 1 ∈ a +ᵥ ↑(closure ↑∅)

Tactic:
simp [(by grind : x ≠ a), (by grind : x + 1 ≠ a)]

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:
by
  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_ex]
  exact fun M v xs => exists_congr fun a => h.realize_bd_iff

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hs : s.Finite
⊢ (closure L).toFun ↑hs.toFinset = (closure L).toFun s

Tactic:
hs.coe_toFinset

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hs : s.Finite
⊢ (closure L).toFun s = (closure L).toFun s
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
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)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd) ≈ Quotient.out x

Tactic:
DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),

Goal state after:
case mp
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)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (f (Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd)).fst
        (Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd)).fst ⋯)
      (Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd)).snd =
    (f (Quotient.out x).fst (Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd)).fst ⋯) (Quotient.out x).snd
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)

Tactic:
cases nonempty_encodable α
  rcases exists_pair_lt β with ⟨x, y, hxy⟩
  obtain ⟨a, ha⟩ := exists_between hxy
  have : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
  let our_ideal : Ideal (PartialIso α _) :=
    idealOfCofinals default (definedAtLeft (Set.Ioo x y))
  let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ _ a)
  refine
    ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
        (OrderEmbedding.subtype _)⟩
  rcases (F a₁).prop with ⟨f, hf, ha₁⟩
  rcases (F a₂).prop with ⟨g, hg, ha₂⟩
  rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
  exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
classical
  rw [age]
  ext N
  refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
  let := Language.order.linearOrderOfModels M
  let := Language.order.linearOrderOfModels N
  exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case inl
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ φ ∉ q

Tactic:
← hφ,

Goal state after:
case inl
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ ¬φ ∉ p
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case inr
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ ¬φ ∉ q

Tactic:
← hφ,

Goal state after:
case inr
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ ¬¬φ ∉ p
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : 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
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : j = i
⊢ (single i 1) j ≤ n j

Tactic:
grind [single_eq_same, single_eq_of_ne]

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

Goal state before:
pp: case neg
σ : 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
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : ¬j = i
⊢ (single i 1) j ≤ n j

Tactic:
grind [single_eq_same, single_eq_of_ne]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : constantCoeff f = 0
this : f⁻¹ = 0
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f

Tactic:
rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by
  by_cases h0 : n = 0
  · rw [h0]; simp [isCyclic_units_zero]
  by_cases h1 : n = 1
  · rw [h1]; simp [isCyclic_units_one]
  by_cases h2 : n = 2
  · rw [h2]; simp [isCyclic_units_two]
  by_cases h4 : n = 4
  · rw [h4]; simp [isCyclic_units_four]
  simp only [h0, h1, h2, h4, false_or, and_or_left, exists_or]
  rcases (n.even_or_odd).symm with hn | hn
  · 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
  obtain ⟨n, rfl⟩ := hn.two_dvd
  rcases (n.even_or_odd).symm with hn | hn
  · rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]
    · congr! with p m
      rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]
      rintro rfl
      contrapose! h2
      cases Nat.lt_one_iff.mp h2
      rw [pow_zero, mul_one]
    · rintro ⟨p, m, -, odd, -, eq⟩
      have := eq ▸ odd.pow
      simp [← Nat.not_even_iff_odd] at this
  obtain ⟨n, rfl⟩ := hn.two_dvd
  apply iff_of_false
  · rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]
    lia
  grind

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n x : ℕ
hx : x ∈ range (n + 1)
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Tactic:
rw [mem_range_succ_iff] at hx

Goal state after:
n x : ℕ
hx : x ≤ n
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 0 n)

Tactic:
ext p
  simp [primesLE_eq_filter_range]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1

Tactic:
by
  refine ((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans ?_).trans (bernoulli'_spec n)
  refine sum_congr rfl fun x hx => ?_
  simp only [add_tsub_cancel_of_le, mem_range_succ_iff.mp hx, cast_sub]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
if_neg (succ_ne_zero _)

Goal state after:
case succ
n : ℕ
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
hrw : ↑p ^ N / ↑M = ↑p ^ (N - e) / ↑M'
hM'_eq : ↑p ^ (N - e) / ↑M' = Rat.divInt (↑p ^ (N - e)) ↑M'
⊢ (↑p ^ (N - e) / ↑M').den ∣ M'

Tactic:
by
      rw [hM'_eq]; exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = ∑ n ∈ Ioc 0 ⌊↑⌊x⌋₊⌋₊, Λ n

Tactic:
rw [floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
rw [floor_natCast]

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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv ((Algebra.norm R) (∑ i, (bS.repr a) i • bS i)) ≤ normBound abv bS * y ^ Fintype.card ι

Tactic:
Algebra.norm_apply,

Goal state after:
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv (LinearMap.det ((Algebra.lmul R S) (∑ i, (bS.repr a) i • bS i))) ≤ normBound abv bS * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x - θ x = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n

Tactic:
rw [psi, theta, sum_filter, sum_filter, ← sum_sub_distrib]
  refine sum_congr rfl fun n hn ↦ ?_
  split_ifs with h
  · simp [h, vonMangoldt_apply_prime]
  · simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
obtain ⟨N₂, h2⟩ := psi_pow_eq_sum_b x 2 hx

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x.zmodRepr).zmodRepr = x.zmodRepr

Tactic:
by
  apply zmodRepr_unique _ _ (zmodRepr_lt_p _)
  simp

Goal state after:
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:
rw [Ne, Fin.succ_inj] at j_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₀ = j₁
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A (Classical.choose ⋯).succ % b)) < cardPowDegree b • ε
⊢ False
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)

Tactic:
calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_
      · apply add_lt_add_of_lt_of_le (ih _)
        apply Nat.mul_le_mul_left
        apply le_pred_of_lt
        apply ZMod.val_lt
      · rw [mul_tsub, mul_one, ← _root_.pow_succ]
        apply add_tsub_cancel_of_le (le_of_lt hp)

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ ((LinearMap.BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Tactic:
← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero

Goal state after:
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ (traceForm K L).Nondegenerate
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = (ZMod.ringEquivCongr hn) ((ZMod.ringEquivCongr ⋯) c)

Tactic:
← ZMod.ringEquivCongr_symm hn,

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = (ZMod.ringEquivCongr hn) ((ZMod.ringEquivCongr hn).symm c)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (b'.toMatrix ⇑b).det

Tactic:
← LinearMap.toMatrix_id_eq_basis_toMatrix b b'

Goal state after:
case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit ((LinearMap.toMatrix b b') LinearMap.id).det
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } ∈ unitary (ℤ√d)

Tactic:
Unitary.mem_iff,

Goal state after:
d x y : ℤ
⊢ IsPell { re := x, im := y } ↔
    star { re := x, im := y } * { re := x, im := y } = 1 ∧ { re := x, im := y } * star { re := x, im := y } = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
⊢ d * (y + w) * (y + w) < c * (x + z) * (x + z)

Tactic:
simp only [mul_add, mul_comm, mul_left_comm, add_assoc]

Goal state after:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n

Tactic:
exact dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

Goal state after: