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

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

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

Tactic:
·

Goal state after:
case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ hs.fract x = hs.base
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
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i

Tactic:
·

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
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
·

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet
    (⋃ i ∈ {i | ↑i ∉ hs.periods},
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z})
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
this : NoMaxOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite

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
hS : (↑S).Finite
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
by
  rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
  refine
    ⟨fun h =>
      ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
          completeTheory.isMaximal L[[α]] h.some⟩,
        (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
      ?_⟩
  rintro ⟨p, hp⟩
  exact p.isMaximal.1.mono (union_subset p.subset hp)

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
⊢ ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)

Tactic:
intro f ho hd

Goal state after:
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)
⊢ Dense (⋂ n, f n)
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
⊢ t₁ ∈ range T.typesWith → ∀ 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₂ ∈ range T.typesWith, ∀ 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}

pp: case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsMaximal {φ | T.typesWith φ ∈ F}

pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ?refine_1, isMaximal' := ?refine_2 } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ?refine_1, isMaximal' := ?refine_2 }

Tactic:
·

Goal state after:
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}
Module: Mathlib.ModelTheory.Topology.Types

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

pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ?refine_2 } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ?refine_2 }

Tactic:
·

Goal state after:
case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsMaximal {φ | T.typesWith φ ∈ F}
Module: Mathlib.ModelTheory.Topology.Types

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

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:
·

Goal state after:
case refine_2.refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsFinitelySatisfiable {φ | T.typesWith φ ∈ F}
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:
·

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} ∨ Formula.not φ ∈ {φ | T.typesWith φ ∈ F}
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
·

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
·

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr

pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Tactic:
·

Goal state after:
case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: case mp
n : ℕ
⊢ IsAlmostPrime 1 n → Prime n

pp: case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ IsAlmostPrime 1 n → Prime n
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Tactic:
·

Goal state after:
case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «0»
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

pp: case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}

Tactic:
·

Goal state after:
case «0»
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

pp: case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}

Tactic:
·

Goal state after:
case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1».«0»
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

pp: case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

pp: case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
·

Goal state after:
case «1».«1».«0»
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

pp: case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
·

Goal state after:
case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
·

Goal state after:
case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
a : (ZMod 0)ˣ
⊢ a ^ λ 0 = 1

pp: case succ
n✝ : ℕ
a : (ZMod (n✝ + 1))ˣ
⊢ a ^ λ (n✝ + 1) = 1

Tactic:
·

Goal state after:
case zero
a : (ZMod 0)ˣ
⊢ a ^ λ 0 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
⊢ λ 0 ∣ φ 0

pp: case succ
n✝ : ℕ
⊢ λ (n✝ + 1) ∣ φ (n✝ + 1)

Tactic:
·

Goal state after:
case zero
⊢ λ 0 ∣ φ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
a : ℕ
h : a ∣ 0
⊢ λ a ∣ λ 0

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

Tactic:
·

Goal state after:
case zero
a : ℕ
h : a ∣ 0
⊢ λ a ∣ λ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ n✝ + 1 ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case pos
a b : ℕ
h₀ : a = 0 ∨ b = 0
⊢ λ (a.lcm b) = (λ a).lcm (λ b)

pp: case neg
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) = (λ a).lcm (λ b)

Tactic:
·

Goal state after:
case pos
a b : ℕ
h₀ : a = 0 ∨ b = 0
⊢ λ (a.lcm b) = (λ a).lcm (λ b)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

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

pp: case a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ a).lcm (λ b) ∣ λ (a.lcm b)

Tactic:
·

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) ∣ (λ a).lcm (λ b)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ a).lcm (λ b) ∣ λ (a.lcm b)

Tactic:
·

Goal state after:
case a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ a).lcm (λ b) ∣ λ (a.lcm b)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
⊢ λ (∅.lcm f) = ∅.lcm (⇑λ ∘ f)

pp: case refine_2
α : Type u_2
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : λ (s.lcm f) = s.lcm (⇑λ ∘ f)
⊢ λ ((insert a s).lcm f) = (insert a s).lcm (⇑λ ∘ f)

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
⊢ λ (∅.lcm f) = ∅.lcm (⇑λ ∘ f)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 2
hn' : n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)

pp: case neg
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : n ≠ 2
hn' : n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k

pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)

pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
·

Goal state after:
case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 0 < n

Tactic:
by lia

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

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
·

Goal state after:
case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)

Tactic:
·

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 0 < n

Tactic:
·

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 0 < n
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2

Tactic:
·

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ (u * x) ^ 1 * ↑(p.choose 1) = ↑p * u * x

pp: case h.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ∑ 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) =
    ↑p * u *
      (v *
        (a * x ^ 2 * ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
          b * x ^ p))

Tactic:
·

Goal state after:
case h.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ (u * x) ^ 1 * ↑(p.choose 1) = ↑p * u * x
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h.e_a.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) =
    ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))

pp: case h.e_a.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ (u * x) ^ p * ↑(p.choose p) = ↑p * u * (v * (b * x ^ p))

Tactic:
·

Goal state after:
case h.e_a.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) =
    ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k

pp: case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b

Tactic:
·

Goal state after:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ k ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b

Tactic:
·

Goal state after:
case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ 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
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ i < p

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : 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
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

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

Tactic:
·

Goal state after:
case inl
𝕜 : 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
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume
Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville

Goal state before:
pp: case pos
m n : ℕ
hm : m = 0
⊢ liouville (m * n) = liouville m * liouville n

pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
·

Goal state after:
case pos
m n : ℕ
hm : m = 0
⊢ liouville (m * n) = liouville m * liouville n
Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville

Goal state before:
pp: case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ liouville (m * n) = liouville m * liouville n

pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
·

Goal state after:
case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ liouville (m * n) = liouville m * liouville n
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inl
𝕜 : 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

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:
·

Goal state after:
case inl.inl
𝕜 : 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
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑n.minFac

pp: case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑n.minFac
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case inl
⊢ Λ 1 ≠ 0 ↔ IsPrimePow 1

pp: case inr
n : ℕ
hn : n ≠ 1
⊢ Λ n ≠ 0 ↔ IsPrimePow n

Tactic:
·

Goal state after:
case inl
⊢ Λ 1 ≠ 0 ↔ IsPrimePow 1