mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : w = 0
⊢ w + u ∈ f a

pp: case neg
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
⊢ w + u ∈ f a

Tactic:
· simpa [hw₁]

Goal state after:
case neg
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
⊢ w + u ∈ f a
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → N.FG

Tactic:
by
    rintro ⟨t', h, rfl⟩
    rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
    exact ⟨t, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

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

Tactic:
rcases h with h | h

Goal state after:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ N.CG ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
rw [cg_def]
  constructor
  · 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
  · intro h
    rcases h with h | h
    · refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩
      rw [← SetLike.coe_subset_coe, h]
      exact empty_subset _
    · obtain ⟨f, rfl⟩ := h
      exact ⟨range f, countable_range _, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
  · obtain ⟨⟨f', hf'⟩, mf', ff'1, ff'2⟩ := h ⟨⟨S, _, f.equivRange⟩, S_FG⟩ m
    refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
    · simp only [sup_le_iff, ff'1, closure_le, singleton_subset_iff, SetLike.mem_coe, mf',
        and_self]
    · ext ⟨x, hx⟩
      rw [Embedding.subtype_equivRange] at ff'2
      simp only [← ff'2, Embedding.comp_apply, Substructure.coe_inclusion,
        Equiv.coe_toEmbedding, coe_subtype, PartialEquiv.toEmbedding_apply]
  · obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m
    refine ⟨⟨⟨closure L {m} ⊔ f.dom, f'.toHom.range, f'.equivRange⟩,
      (fg_closure_singleton _).sup f_FG⟩,
      subset_closure.trans (le_sup_left : (closure L) {m} ≤ _) (mem_singleton m),
      ⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩
    rw [PartialEquiv.toEmbedding] at eq_f'
    simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
      Embedding.equivRange_apply, eq_f']

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

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + (↑i + ((-hs.floor x i).toNat - 1) • ↑i) + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
← succ_nsmul',

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + ((-hs.floor x i).toNat - 1 + 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + (↑i + n • ↑i)) i = 0
⊢ hs.floor x i < 0

Tactic:
← succ_nsmul',

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + (n + 1) • ↑i) i = 0
⊢ hs.floor x i < 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet
    (⋃ i,
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z})

Tactic:
· refine .iUnion fun i => .proj' ?_
    rw [ofPred_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite (finite_singleton _)) (LinearMap.funLeft ℕ ℕ Sum.inr)
    apply IsSemilinearSet.proj'
    rw [ofPred_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.sdiff) (LinearMap.funLeft ℕ ℕ Sum.inr)
    apply IsSemilinearSet.proj'
    rw [ofPred_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.sdiff) (LinearMap.funLeft ℕ ℕ Sum.inr)
    have := Fintype.ofFinite ι
    convert!
      Nat.isSemilinearSet_setOfPred_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) i.1 hs.base
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 1) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 0) 1) 0) using 4
      <;> simp [add_comm _ i.1, add_assoc, fromCols_mulVec]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) →
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
rintro ⟨M, h1, h2, rfl⟩

Goal state after:
case mp
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
h1 : Countable ↑M
⊢ (L.age ↑M).Nonempty ∧
    (∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)) ∧
      (Quotient.mk' '' L.age ↑M).Countable ∧
        (∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1) ∧ Hereditary (L.age ↑M) ∧ JointEmbedding (L.age ↑M)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + (↑i + ((hs.floor x i).toNat - 1) • ↑i) + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
← succ_nsmul',

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ((hs.floor x i).toNat - 1 + 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + (↑i + n • ↑i)) i
⊢ 0 < hs.floor x i

Tactic:
← succ_nsmul',

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + (n + 1) • ↑i) i
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Order

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

Tactic:
have := NoTopOrder.to_noMaxOrder N

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

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)
h : ∀ φ ∈ S, {p | φ ∈ p} = Set.univ
φ : L[[α]].Sentence
h1 : φ ∈ S
⊢ (fun φ ↦ {p | φ ∈ p}) φ = Set.univ

Tactic:
exact h _ h1

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

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
⊢ t₂ ∈ range T.typesWith → ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range T.typesWith, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
⟨ψ, ht₂⟩

Goal state after:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
⊢ ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range T.typesWith, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ (L.lhomWithConstants α).onTheory T ⊆ {φ | T.typesWith φ ∈ F}

Tactic:
intro φ x

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
x : φ ∈ (L.lhomWithConstants α).onTheory T
⊢ φ ∈ {φ | T.typesWith φ ∈ F}
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ GCDMonoid.lcm (exponent (ZMod a)ˣ) (exponent (ZMod b)ˣ)

Tactic:
← exponent_prod,

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ exponent ((ZMod a)ˣ × (ZMod b)ˣ)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)

Tactic:
obtain ⟨a, ha⟩ := hvu

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hpuv : ↑p * u * v ∣ u ^ p
x a : R
ha : u = v * a
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)

Tactic:
let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p * ↑a) = p ^ n

Tactic:
convert! orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n using 1
  · rw [pow_one]
  · have := hp.two_le; lia

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

Goal state before:
pp: case succ
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale ↑k) (exp A)
⊢ exp A ^ (k + 1) = (rescale ↑(k + 1)) (exp A)

Tactic:
simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}
⊢ p ∣ (m + n).choose m

Tactic:
rw [mem_filter, mem_Ico] at hp
          exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
              (Nat.lt_succ_iff.1 hp.1.2)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p ∈ antidiagonal (n + 1),
      (coeff p.1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (coeff p.2) (exp A - 1) =
    (coeff (n + 1)) (X * exp A)

Tactic:
mul_comm X,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p ∈ antidiagonal (n + 1),
      (coeff p.1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (coeff p.2) (exp A - 1) =
    (coeff (n + 1)) (exp A * X)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm]

Goal state after:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
⊢ ∑ 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: case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H : ∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Tactic:
rw [sum_eq_add_sum_sdiff_singleton_of_mem h₁] at H ⊢

Goal state after:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
⊢ ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 =
    0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ), Prime p → n < p → 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n

Tactic:
bertrand_main_inequality n_large

Goal state after:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ), Prime p → n < p → 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ 4 ^ n ≤ 4 ^ n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x ≤ 1
⊢ x < 2

Tactic:
by linarith

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
⊢ 0 < normBound abv bS

Tactic:
by
  obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 := by
    by_contra! h
    obtain ⟨i⟩ := bS.index_nonempty
    apply bS.ne_zero i
    apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
    ext j k
    simp [h]
  simp only [normBound, Algebra.smul_def, eq_natCast]
  apply mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _))
  refine pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) ?_) _
  refine lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ ?_)
  exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
this : 1 < p
h✝ : p ≤ n
⊢ n ≠ 0

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
left✝¹ : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left✝ : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ n ≠ 0

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x

Tactic:
gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : x < 1
⊢ x < 2

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < 1 / 2

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ ↑1 = bernoulli (2 * 0) + ∑ p ∈ range (2 * 0 + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * 0, 1 / ↑p

Tactic:
decide +kernel

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹)

Tactic:
rcases le_total x 0 with hx | hx
  · grind [theta_eq_zero_iff, psi_eq_zero_iff, psi_nonneg]
  · exact (psi_sub_theta_bounds hx).1

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ ∀ (x : R), ¬(x ∈ finsetApprox bS adm ∧ x = 0)

Tactic:
rintro x ⟨hx, rfl⟩

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
hx : 0 ∈ finsetApprox bS adm
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < 2

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 0 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2) =o[atTop] fun x ↦ x ^ (1 / 2)

Tactic:
apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2) =O[atTop] fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
apply IsBigO.of_bound'

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖ ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ 2 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ 2 ≤ x

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ 0 ≤ t

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ g (h ↑↑ζ) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)

Tactic:
toFun_spec,

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ g ↑(↑ζ ^ (χ₀ n h).val) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)