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

Goal state before:
pp: case insert.hft
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
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (⋃ x ∈ s✝, s x)

Tactic:
· apply IntegrableOn.biUnion_finset hs.2 hf.2

Goal state after:
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✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε

Tactic:
let s'' := s' \ t'

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε
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', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
let M : MeasurableSpace α := generateFrom C

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
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
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
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s

Tactic:
have : NeBot (ae (μ.variation.restrict s)) := by simpa using h's
      obtain ⟨x, hx⟩ : ∃ x, ‖f x‖ ≤ C := hC.exists
      have : 0 ≤ C := le_trans (norm_nonneg _) hx
      positivity

Goal state after:
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
c : ℝ
⊢ (c • μ).transpose B = c • μ.transpose B

Tactic:
by
  simp [transpose, mapRange_smul]

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

Goal state before:
pp: case mpr.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : x ∈ closure (insert a t)
⊢ a + x ∈ closure (a +ᵥ ↑(closure t))

Tactic:
· simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx
      rcases hx with ⟨_, ⟨n, rfl⟩, ⟨x, hx, rfl⟩⟩
      rw [add_left_comm]
      refine add_mem (nsmul_mem (mem_closure_of_mem ?_) _)
        (mem_closure_of_mem (vadd_mem_vadd_set hx))
      nth_rw 2 [← add_zero a]
      exact vadd_mem_vadd_set (zero_mem _)

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

Goal state before:
pp: case h
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))
⊢ IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))

Tactic:
by_cases hindep : LinearIndepOn ℕ id (t : Set M)

Goal state after:
case pos
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))
hindep : LinearIndepOn ℕ id ↑t
⊢ IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))

case neg
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))
hindep : ¬LinearIndepOn ℕ id ↑t
⊢ IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
⊢ x ∈ ⋃₀ ↑S ↔ x + S.lcm p ∈ ⋃₀ ↑S

Tactic:
simp only [mem_sUnion, SetLike.mem_coe]

Goal state after:
case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
⊢ (∃ t ∈ S, x ∈ t) ↔ ∃ t ∈ S, x + S.lcm p ∈ t
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : x i + y i = a
hxz : x + z ∈ s
hxzi : x i + z i = a
⊢ a + z i = a

Tactic:
← hxi,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : x i + y i = a
hxz : x + z ∈ s
hxzi : x i + z i = a
⊢ x i + z i = x i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
⊢ IsSemilinearSet s

Tactic:
by
  classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    have := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOfPred_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_ofPred_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective ⇑h
⊢ IsSemilinearSet (⇑h '' ⇑h ⁻¹' {x | a + f x = b + g x})

Tactic:
preimage_ofPred_eq

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective ⇑h
⊢ IsSemilinearSet (⇑h '' {a_1 | a + f (h a_1) = b + g (h a_1)})
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap graphRel.adj xs

Tactic:
refine congr rfl (funext ?_)

Goal state after:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Tactic:
by
  filter_upwards [Ico_ae_eq_Icc] with t h ht
  rw [Nat.floor_eq_on_Ico _ _ (h.mpr ht)]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: ⊢ log * ↑μ = Λ

Tactic:
rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have h_locint {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : n ≤ t₁) (h₂ : t₂ ≤ n + 1)
          (h₃ : a ≤ t₁) (h₄ : t₂ ≤ b) :
          IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂ := by
        rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]
        exact (IntegrableOn.mono_set (hg_int.mul_const _) (Set.Icc_subset_Icc h₃ h₄)).congr
          <| ae_restrict_of_ae_restrict_of_subset (Set.Icc_subset_Icc h₁ h₂)
            <| (ae_restrict_iff' measurableSet_Icc).mpr
              (by filter_upwards [sumlocc c n] with t h ht using by rw [h ht])
      have aux1 : 0 ≤ b := (Nat.pos_of_floor_pos <| (Nat.zero_le _).trans_lt hb).le
      have aux2 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
      have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
      have aux4 : a ≤ ⌊b⌋₊ := le_of_lt (by rwa [← Nat.floor_lt ha])
      -- now break up into 3 subintervals
      rw [← intervalIntegrable_iff_integrableOn_Icc_of_le (aux3.trans aux2)]
      have I1 : IntervalIntegrable _ volume a ↑(⌊a⌋₊ + 1) :=
        h_locint (mod_cast aux3) (Nat.floor_le ha) (mod_cast le_rfl) le_rfl (mod_cast aux2)
      have I2 : IntervalIntegrable _ volume ↑(⌊a⌋₊ + 1) ⌊b⌋₊ :=
        trans_iterate_Ico hb fun k hk ↦ h_locint (mod_cast k.le_succ)
          le_rfl (mod_cast le_rfl) (ineqofmemIco hk).1 (mod_cast (ineqofmemIco hk).2)
      have I3 : IntervalIntegrable _ volume ⌊b⌋₊ b :=
        h_locint (Nat.floor_le aux1) le_rfl (Nat.lt_floor_add_one _).le aux4 le_rfl
      exact (I1.trans I2).trans I3

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

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ (coeff n✝)
      (∑ k ∈ Finset.range n,
        { toFun := fun f ↦ mk fun n ↦ ↑k ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          (exp A)) =
    (coeff n✝) (mk fun p ↦ ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹)

Tactic:
simp only [one_div, coeff_mk, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_exp, map_sum]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
rwa [Nat.cast_zero]

Goal state after:
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 := fun i j ↦ (A i).coeff ↑j
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀

Tactic:
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
    simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)

Goal state after:
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 := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)

Tactic:
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
    simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ n.lcmUpto.factorization p = log p n

Tactic:
by
  rw [lcmUpto, Finset.factorization_lcm (fun _ _ ↦ by grind)]
  have := hp.one_lt
  refine le_antisymm ?_ ?_
  · simp only [Finset.sup_le_iff, mem_Icc, and_imp]
    exact fun m _ h ↦ le_log_of_pow_le this (le_of_dvd (by grind) (ordProj_dvd m p) |>.trans h)
  rcases le_or_gt p n with _ | h
  · have := pow_log_le_self p (x := n) (by linarith)
    grw [← le_sup (b := p ^ p.log n) (by grind)]
    simp [hp]
  simp [log_of_lt h]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ ∑ n ∈ Icc 1 (1 + 6 * N + 1 + 1 + 1 + 1 + 1 + 1), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N + 1 + 1 + 1), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N + 1 + 1), b x (3 * n) +
      ∑ n ∈ Icc 1 (N + 1), c x n

Tactic:
simp only [le_add_iff_nonneg_left, _root_.zero_le, sum_Icc_succ_top, ih, c]

Goal state after:
case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) +
                  ∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * (N + 1) - 1) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ↑(π ⌊x⌋₊) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
simp only [primeCounting, primeCounting', count_eq_card_filter_range]

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
have int_deriv (f : ℝ → ℝ) :
        ∫ u in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u =
        ∫ u in 2..x, f u * -(u * log u ^ 2)⁻¹ :=
      intervalIntegral.integral_congr fun u _ ↦ by simp [field]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
int_deriv :
  ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u = ∫ (u : ℝ) in 2..x, f u * -(u * log u ^ 2)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
simp only [primeCounting, primeCounting', count_eq_card_filter_range]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Nat.cast)

Tactic:
rw [Metric.mem_closure_range_iff]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Tactic:
ext i j : 2

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
i j : ι
⊢ traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
⊢ limNthHom f_compat 0 = 0

Tactic:
simp [limNthHom]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
⊢ ofIntSeq 0 ⋯ = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
n : ℤ√d
⊢ ↑n.norm = n * star n

Tactic:
ext <;> simp [norm, star, mul_comm, sub_eq_add_neg]

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a

Tactic:
have t := (b - a).nonneg_total

Goal state after:
d : ℕ
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case neg
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : ¬p ^ (k + 1) = 2
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
· exact discr_prime_pow_ne_two hζ hirr hk

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a

Tactic:
have t := (b - a).nonneg_total

Goal state after:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|

Tactic:
obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)

Goal state after:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])

Tactic:
rw [← hx, ← hy]

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ u v s t b,
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])