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_9
inst✝ : MeasurableSpace β
φ : X → β
⊢ ((μ.transpose B).map φ).variation ≤ Measure.map φ (μ.transpose B).variation

Tactic:
variation_map_le

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
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
⊢ Measure.map φ (μ.transpose B).variation ≤ Measure.map φ (μ.transpose B).variation
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case equal
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
this : Fintype α
n✝ : ℕ
t₁ t₂ : presburger[[↑A]].Term (α ⊕ Fin n✝)
k₁ : ℕ
u₁ : α ⊕ Fin n✝ → ℕ
ht₁ : ∀ (v : α ⊕ Fin n✝ → ℕ), Term.realize v t₁ = k₁ + u₁ ⬝ᵥ v
⊢ IsSemilinearSet
    {v |
      Term.realize (Sum.elim (v ∘ Sum.inl) (v ∘ Sum.inr)) t₁ = Term.realize (Sum.elim (v ∘ Sum.inl) (v ∘ Sum.inr)) t₂}

Tactic:
rcases term_realize_eq_add_dotProduct t₂ with ⟨k₂, u₂, ht₂⟩

Goal state after:
case equal
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
this : Fintype α
n✝ : ℕ
t₁ t₂ : presburger[[↑A]].Term (α ⊕ Fin n✝)
k₁ : ℕ
u₁ : α ⊕ Fin n✝ → ℕ
ht₁ : ∀ (v : α ⊕ Fin n✝ → ℕ), Term.realize v t₁ = k₁ + u₁ ⬝ᵥ v
k₂ : ℕ
u₂ : α ⊕ Fin n✝ → ℕ
ht₂ : ∀ (v : α ⊕ Fin n✝ → ℕ), Term.realize v t₂ = k₂ + u₂ ⬝ᵥ v
⊢ IsSemilinearSet
    {v |
      Term.realize (Sum.elim (v ∘ Sum.inl) (v ∘ Sum.inr)) t₁ = Term.realize (Sum.elim (v ∘ Sum.inl) (v ∘ Sum.inr)) t₂}
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
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_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ¬μ.Integrable fun x ↦ f (φ x)

pp: case neg
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_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ¬(μ.map φ).Integrable f

Tactic:
· exact h'fm

Goal state after:
case neg
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_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ¬(μ.map φ).Integrable f
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) → ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

pp: case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N) → ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
· rintro ⟨S, Scount, hS⟩
    rcases eq_empty_or_nonempty (N : Set M) with h | h
    · exact Or.intro_left _ h
    obtain ⟨f, h'⟩ :=
      (Scount.union (Set.countable_singleton h.some)).exists_eq_range
        (singleton_nonempty h.some).inr
    refine Or.intro_right _ ⟨f, ?_⟩
    rw [← h', closure_union, hS, sup_eq_left, closure_le]
    exact singleton_subset_iff.2 h.some_mem

Goal state after:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N) → ∃ S, S.Countable ∧ (closure L).toFun S = N
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (of L ι G f j) ((f i j hij) x) = (of L ι G f i) x

Tactic:
of_apply,

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ ⟦Structure.Sigma.mk f j ((f i j hij) x)⟧ = (of L ι G f i) x
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ ⟦Structure.Sigma.mk f j ((f i j hij) x)⟧ = (of L ι G f i) x

Tactic:
of_apply,

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ ⟦Structure.Sigma.mk f j ((f i j hij) x)⟧ = ⟦Structure.Sigma.mk f i x⟧
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ x ∈ Iic (hs.base + ∑ i, ↑i)

Tactic:
rw [mem_Iic, ← toRatVec_mono, map_add, map_sum, ← add_sub_cancel (toRatVec hs.base) (toRatVec x),
    add_le_add_iff_left, ← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ ∑ i, (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ ∑ x, 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
a₁✝ a₂✝ : M ↪[L] N
h :
  ∃ (h_dom : ((fun f ↦ f.toPartialEquiv) a₁✝).dom = ((fun f ↦ f.toPartialEquiv) a₂✝).dom),
    ∀ (x : M) (h : x ∈ ((fun f ↦ f.toPartialEquiv) a₁✝).dom),
      ((fun f ↦ f.toPartialEquiv) a₁✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
        ((fun f ↦ f.toPartialEquiv) a₂✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
rcases h with ⟨_, H⟩

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
x✝ : M
w✝ : ((fun f ↦ f.toPartialEquiv) a₁✝).dom = ((fun f ↦ f.toPartialEquiv) a₂✝).dom
H :
  ∀ (x : M) (h : x ∈ ((fun f ↦ f.toPartialEquiv) a₁✝).dom),
    ((fun f ↦ f.toPartialEquiv) a₁✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
      ((fun f ↦ f.toPartialEquiv) a₂✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
⊢ a₁✝ x✝ = a₂✝ x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1,
      (⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
        (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1) ≤
    toRatVec x

Tactic:
enter [1, 2, _]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ StrictMono fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
    if hxS : x ∈ S
    then if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
    else
      obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
      if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Tactic:
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]
  refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
  intro h a
  exact exists_not_ge a

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

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
⊢ ∃ U, IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
cases mem_or_not_mem p φ with
  | inl h =>
    refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
  | inr h =>
    refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]

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

Goal state before:
pp: case refine_2.refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ φ ∈ {φ | T.typesWith φ ∈ F} ∨ Formula.not φ ∈ {φ | T.typesWith φ ∈ F}

Tactic:
simp only [mem_ofPred_eq, typesWith_not]

Goal state after:
case refine_2.refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ T.typesWith φ ∈ F ∨ (T.typesWith φ)ᶜ ∈ F
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:

Tactic:
(2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
    _ = 1 := by norm_num

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

Goal state before:
pp: ⊢ ¬Monoid.exponent (ZMod 8)ˣ = Fintype.card (ZMod 8)ˣ

Tactic:
card_units_eq_totient

Goal state after:
⊢ ¬Monoid.exponent (ZMod 8)ˣ = φ 8
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (2 ^ n))ˣ ↔ n ≤ 2

Tactic:
by
  match n with
  | 0 => simp [isCyclic_units_one]
  | 1 => simp [isCyclic_units_prime Nat.prime_two]
  | 2 => simp [isCyclic_units_four]
  | n + 3 =>
    simp only [Nat.reduceLeDiff, iff_false]
    intro H
    apply not_isCyclic_units_eight
    have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by lia)
    exact isCyclic_of_surjective _ (unitsMap_surjective h)

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ π' n = 0 ↔ n ≤ 2

Tactic:
by
  rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
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.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) =
    (algebraMap ℚ A) ↑(n + 1) * t ^ n

Tactic:
← aeval_monomial,

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.Bernoulli

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1

Tactic:
rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑(x.1 + x.2)! =
    ↑(x.1 + x.2)! / ↑(x.1! * x.2!) / (↑x.2 + 1) * bernoulli x.1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto ∣ n !

Tactic:
simp +contextual [lcmUpto, dvd_factorial, Order.one_le_iff_pos]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
cast_sub

Goal state after:
case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ log x / log 2

case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
    rw [norm_sub_rev] at hr
    calc
      _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
      _ ≤ _ := Padic.nonarchimedean _ _
      _ ≤ _ := max_le (le_of_lt hr) x.2

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1
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)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Tactic:
rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: case e_a
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
⊢ 1 = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2

Tactic:
have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]

Goal state after:
case e_a
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
hunit : IsUnit r
⊢ 1 = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
have : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional {n} ℚ K)

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) ↔ x = y

Tactic:
by
  constructor
  · intro h
    rw [← lift_self x, ← lift_self y]
    simp +unfoldPartialApp [lift, limNthHom, nthHom, h]
  · rintro rfl _
    rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = pellZd a1 (m + 1)

Tactic:
show b = b * ⟨a, -1⟩ * ⟨a, 1⟩ by rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b * { re := ↑a, im := -1 } * { re := ↑a, im := 1 } = pellZd a1 (m + 1)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp [norm, star, mul_comm, sub_eq_add_neg]

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

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

Tactic:
simp [norm, star, mul_comm, sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0 : n = 0
⊢ yn a1 n ∣ t

Tactic:
n0

Goal state after:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : 0 ∣ t
n0 : n = 0
⊢ yn a1 0 ∣ t
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = 1

Tactic:
convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _

Goal state after:
case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i

case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i) = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 2 * n ≤ 2 * n

Tactic:
Nat.succ_mul

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 1 * n + n ≤ 1 * n + n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ↑(↑j / ↑k).den ≤ k

Tactic:
convert! le_of_dvd hk₀ (Rat.den_dvd j k)

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ↑j / ↑k = Rat.divInt j k
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ∈ factoredNumbers s
⊢ m.primeFactors ⊆ s

Tactic:
rw [mem_factoredNumbers] at hm
  exact fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1

Tactic:
Nat.succ_mul

Goal state after:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < z * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1