mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
⊢ ∀ (h : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
        ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h⟩) =
      { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
        ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x✝, ⋯⟩)

Tactic:
_

Goal state after:
case refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
h✝ : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
      ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h✝⟩) =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
      ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨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:
1,

Goal state after:
ι : 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)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun 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

Tactic:
_

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.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1) =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
1,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun x_1 ↦ (hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1

Tactic:
_

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| (hs.floor x x✝).toNat • toRatVec ↑x✝ - (-hs.floor x x✝).toNat • toRatVec ↑x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun x_1 ↦
    Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1) • toRatVec ↑x_1 +
      ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1

Tactic:
_

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝) • toRatVec ↑x✝ +
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝
Module: Mathlib.ModelTheory.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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ : ι
⊢ ∀ (j : ι) (hij : i✝ ≤ j) (x : G i✝), (U j) ((f i✝ j hij) x) = (U i✝) x

Tactic:
_

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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
⊢ ∀ (hij : i✝ ≤ j✝) (x : G i✝), (U j✝) ((f i✝ j✝ hij) x) = (U 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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
⊢ ∀ (hij : i✝ ≤ j✝) (x : G i✝), (U j✝) ((f i✝ j✝ hij) x) = (U i✝) x

Tactic:
_

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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
hij✝ : i✝ ≤ j✝
⊢ ∀ (x : G i✝), (U j✝) ((f i✝ j✝ hij✝) x) = (U 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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
hij✝ : i✝ ≤ j✝
⊢ ∀ (x : G i✝), (U j✝) ((f i✝ j✝ hij✝) x) = (U i✝) x

Tactic:
_

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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
hij✝ : i✝ ≤ j✝
x✝ : G i✝
⊢ (U j✝) ((f i✝ j✝ hij✝) x✝) = (U i✝) x✝
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
⊢ x ∈ ⊤ → x ∈ S

Tactic:
_

Goal state after:
case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
⊢ x ∈ S
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n
hKU : closure ↑(K 0) ⊆ U
hK_subset : ⋂ n, closure ↑(K n) ⊆ U ∩ ⋂ n, f n
hK_nonempty : (⋂ n, closure ↑(K n)).Nonempty
⊢ (U ∩ ⋂ n, f n).Nonempty

Tactic:
exact hK_nonempty.mono hK_subset

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
⊢ BaireSpace ↑s

Tactic:
have : LocallyCompactSpace (closure s) := isClosed_closure.locallyCompactSpace
  have : BaireSpace (closure s) := .of_t2Space_locallyCompactSpace
  have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
    (hG.preimage continuous_subtype_val).baireSpace_of_dense
    (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])
  have h_homeo : Homeomorph ((↑) ⁻¹' s : Set (closure s)) s := ⟨⟨fun x => ⟨x, x.2⟩,
    fun x => ⟨⟨x, subset_closure x.2⟩, x.2⟩, by grind, by grind⟩, by fun_prop, by fun_prop⟩
  exact h_homeo.baireSpace

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
S : List ℕ+ := ⋯
H : 1 < sumInv ↑S
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ S.length = 3

Tactic:
simp only [S, insert_eq_cons, length_sort, card_cons, card_singleton]

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

Goal state before:
pp: case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ λ a ∣ λ (n✝ + 1)

Tactic:
rw [carmichael_eq_exponent <| ne_zero_of_dvd_ne_zero (by lia) h, carmichael_eq_exponent']

Goal state after:
case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n✝ + 1))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = Fintype.card (ZMod p)ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
ZMod.card_units

Goal state after:
case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = p - 1
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)

Tactic:
exact Ico_filter_coprime_le k n h0

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝ : 3 ≤ n#
q : ℕ := (n# - 1).minFac
this : n < q
⊢ n < n#

Tactic:
grind [Nat.minFac_le]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258

Tactic:
by rwa [mem_sdiff, mem_singleton] at h

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact exists_prime_lt_and_le_two_mul_eventually n h

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
hd : 2 * k - 2 * m ≥ 2
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))

Tactic:
set d := 2 * k - 2 * m with hd_def

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n)), Λ m =
    ∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q

Tactic:
sum_biUnion <| by rw [pairwiseDisjoint_iff]; grind [Prime.pow_inj']

Goal state after:
n : ℕ
⊢ ∑ x ∈ Icc 1 n with Nat.Prime x, ∑ i ∈ image (fun x_1 ↦ x ^ x_1) (Icc 1 (Nat.log x n)), Λ i =
    ∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
⊢ k₁ ≤ N →
    p₁ ≠ 0 →
      ↑p₁ ≤ x →
        Nat.Prime p₁ →
          ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
            ∀ (a b : ℕ),
              a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝ : k₁ ≤ N
⊢ p₁ ≠ 0 →
    ↑p₁ ≤ x →
      Nat.Prime p₁ →
        ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
          ∀ (a b : ℕ),
            a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝ : k₁ ≤ N
⊢ p₁ ≠ 0 →
    ↑p₁ ≤ x →
      Nat.Prime p₁ →
        ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
          ∀ (a b : ℕ),
            a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝¹ : k₁ ≤ N
a✝ : p₁ ≠ 0
⊢ ↑p₁ ≤ x →
    Nat.Prime p₁ →
      ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
        ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝¹ : k₁ ≤ N
a✝ : p₁ ≠ 0
⊢ ↑p₁ ≤ x →
    Nat.Prime p₁ →
      ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
        ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝² : k₁ ≤ N
a✝¹ : p₁ ≠ 0
a✝ : ↑p₁ ≤ x
⊢ Nat.Prime p₁ →
    ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
      ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝² : k₁ ≤ N
a✝¹ : p₁ ≠ 0
a✝ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
⊢ ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
    ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝³ : k₁ ≤ N
a✝² : p₁ ≠ 0
a✝¹ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
⊢ ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝³ : k₁ ≤ N
a✝² : p₁ ≠ 0
a✝¹ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
⊢ k₂ ≤ N → p₂ ≠ 0 → ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁴ : k₁ ≤ N
a✝³ : p₁ ≠ 0
a✝² : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝¹ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝ : k₂ ≤ N
⊢ p₂ ≠ 0 → ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁴ : k₁ ≤ N
a✝³ : p₁ ≠ 0
a✝² : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝¹ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝ : k₂ ≤ N
⊢ p₂ ≠ 0 → ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁵ : k₁ ≤ N
a✝⁴ : p₁ ≠ 0
a✝³ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝² : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝¹ : k₂ ≤ N
a✝ : p₂ ≠ 0
⊢ ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁵ : k₁ ≤ N
a✝⁴ : p₁ ≠ 0
a✝³ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝² : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝¹ : k₂ ≤ N
a✝ : p₂ ≠ 0
⊢ ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁶ : k₁ ≤ N
a✝⁵ : p₁ ≠ 0
a✝⁴ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝³ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝² : k₂ ≤ N
a✝¹ : p₂ ≠ 0
a✝ : ↑p₂ ≤ x
⊢ Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁶ : k₁ ≤ N
a✝⁵ : p₁ ≠ 0
a✝⁴ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝³ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝² : k₂ ≤ N
a✝¹ : p₂ ≠ 0
a✝ : ↑p₂ ≤ x
hp₂ : Nat.Prime p₂
⊢ ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁷ : k₁ ≤ N
a✝⁶ : p₁ ≠ 0
a✝⁵ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝⁴ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝³ : k₂ ≤ N
a✝² : p₂ ≠ 0
a✝¹ : ↑p₂ ≤ x
hp₂ : Nat.Prime p₂
a✝ : ↑p₂ ≤ x ^ (↑k₂)⁻¹
⊢ p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ cardPowDegree (x - z) < a

Tactic:
rwa [← hyz']

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
⊢ cardPowDegree (x - z) < a

Tactic:
by
  have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
  by_cases hxy' : x = y
  · rwa [hxy']
  by_cases hyz' : y = z
  · rwa [← hyz']
  by_cases hxz' : x = z
  · rwa [hxz', sub_self, map_zero]
  rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'
  refine lt_of_le_of_lt ?_ (max_lt hxy hyz)
  rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy',
    cardPowDegree_nonzero _ hyz']
  have : (1 : ℤ) ≤ Fintype.card Fq := mod_cast (@Fintype.one_lt_card Fq _ _).le
  simp only [le_max_iff]
  refine Or.imp (pow_le_pow_right₀ this) (pow_le_pow_right₀ this) ?_
  rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ←
    degree_eq_natDegree hxy', ← degree_eq_natDegree hyz']
  convert! degree_add_le (x - y) (y - z) using 2
  exact (sub_add_sub_cancel _ _ _).symm

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
have : 0 ≤ x ^ ((n : ℝ)⁻¹) := by positivity
  use ⌊log (x ^ (n : ℝ)⁻¹) / log 2⌋₊
  intro N hN
  simp_rw [psi_eq_sum_theta' this hN, one_div, b, cast_mul, mul_inv_rev, mul_comm,
    ← rpow_mul (by positivity)]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
N : ℕ
⊢ ∑ 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

Tactic:
induction N with
  | zero => simp
  | succ N ih =>
    rw [show 1 + 6 * (N + 1) = (1 + 6 * N) + 1 + 1 + 1 + 1 + 1 + 1 by ring,
      show 3 * (N + 1) = 3 * N + 1 + 1 + 1 by ring,
      show 2 * (N + 1) = 2 * N + 1 + 1 by ring]
    simp only [le_add_iff_nonneg_left, _root_.zero_le, sum_Icc_succ_top, ih, c]
    rw [show 6 * (N + 1) - 1 = 6 * N + 5 by lia]
    ring_nf

Goal state after: