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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - toRatVec hs.base

Tactic:
;

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - toRatVec hs.base
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
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (F.comp (of L ι G f 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
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (F.comp (of L ι G f i)) x
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case e'_4
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
isTop : F.dom = ⊤
⊢ (toEmbeddingOfEqTop isTop).toPartialEquiv = partialEquivLimit S

Tactic:
;

Goal state after:
case e'_4
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
isTop : F.dom = ⊤
⊢ (toEmbeddingOfEqTop isTop).toPartialEquiv = partialEquivLimit S
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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
⊢ ∃ y, (liftInclusion S) y = (liftInclusion S) 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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
⊢ ∃ y, (liftInclusion S) y = (liftInclusion S) 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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) :=
  Embedding.codRestrict (⨆ i, S i) (liftInclusion S) liftInclusion_in_sup
m : M
hm : m ∈ ⨆ i, S i
a : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
h✝ : (liftInclusion S).toHom a = m
⊢ ∃ a, F a = ⟨m, hm⟩

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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) :=
  Embedding.codRestrict (⨆ i, S i) (liftInclusion S) liftInclusion_in_sup
m : M
hm : m ∈ ⨆ i, S i
a : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
h✝ : (liftInclusion S).toHom a = m
⊢ ∃ a, F a = ⟨m, hm⟩
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ ((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x =
    (of L ι (fun x ↦ ↥(S x)) (fun x x_1 h ↦ Substructure.inclusion ⋯) i) x

Tactic:
;

Goal state after:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ ((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x =
    (of L ι (fun x ↦ ↥(S x)) (fun x x_1 h ↦ Substructure.inclusion ⋯) i) x
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
⊢ graphRel.adj = graphRel.adj

Tactic:
;

Goal state after:
V : Type u
⊢ graphRel.adj = graphRel.adj
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2.zero
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
e : ↑(F 0).out ≃[L] ↑N
⊢ ↑(F 0).out ↪[L] ↑(F 0).out

Tactic:
;

Goal state after:
case refine_2.zero
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
e : ↑(F 0).out ≃[L] ↑N
⊢ ↑(F 0).out ↪[L] ↑(F 0).out
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2.succ
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
n : ℕ
e : ↑(F (n + 1)).out ≃[L] ↑N
⊢ ↑(F (n + 1)).out ↪[L] ↑(P (Nat.rec ⟨(F 0).out, ⋯⟩ (fun n N ↦ ⟨P N n, ⋯⟩) n) n)

Tactic:
;

Goal state after:
case refine_2.succ
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
n : ℕ
e : ↑(F (n + 1)).out ≃[L] ↑N
⊢ ↑(F (n + 1)).out ↪[L] ↑(P (Nat.rec ⟨(F 0).out, ⋯⟩ (fun n N ↦ ⟨P N n, ⋯⟩) n) n)
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
q : α × β
qf : q ∈ ↑f
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

Tactic:
rw [cmp_eq_cmp_symm]
      exact a_b _ qf

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
⊢ orderRel.le = orderRel.le

Tactic:
;

Goal state after:
L : Language
α : Type w
M : Type w'
⊢ orderRel.le = orderRel.le
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith ∼φ)

Tactic:
;

Goal state after:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith ∼φ)
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
φ : L[[α]].Sentence
hφ : φ ∈ x
⊢ T.typesWith φ ∈ ↑F

Tactic:
;

Goal state after:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
φ : L[[α]].Sentence
hφ : φ ∈ x
⊢ T.typesWith φ ∈ ↑F
Module: Mathlib.NumberTheory.AlmostPrime

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

Tactic:
exact fun h ↦ ArithmeticFunction.cardFactors_eq_one_iff_prime.mp h.2

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

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

Tactic:
rw [← H, A', sumInv_pqr, add_assoc]
    simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
    apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Tactic:
;

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

Goal state before:
pp: case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Tactic:
;

Goal state after:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
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, ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * 1 ^ (p - m) * ↑(p.choose m) = 1 + ↑p * u * (x + v * y)

Tactic:
rw [← Finset.add_sum_erase (a := 0) _ _ (by simp)]

Goal state after:
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,
    (u * x) ^ 0 * 1 ^ (p - 0) * ↑(p.choose 0) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * 1 ^ (p - x_1) * ↑(p.choose x_1) =
      1 + ↑p * u * (x + v * y)
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 = ↑p * u * x

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 = ↑p * u * x
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
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (↑p * ↑(p.choose i / p)) =
    u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p)

Tactic:
;

Goal state after:
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
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (↑p * ↑(p.choose i / p)) =
    u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p)
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
⊢ (v * a) ^ 2 * x ^ 2 * (v * a * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * (v * a) * (v * (a * x ^ 2 * ((v * a * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
;

Goal state after:
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
⊢ (v * a) ^ 2 * x ^ 2 * (v * a * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * (v * a) * (v * (a * x ^ 2 * ((v * a * x) ^ (i - 2) * ↑(p.choose i / p))))
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

case inr
n : ℕ
hn : n ≠ 1
⊢ Λ n ≠ 0 ↔ IsPrimePow n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ (Λ * ↑ζ) n = log n

Tactic:
;

Goal state after:
n : ℕ
⊢ (Λ * ↑ζ) n = log n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ Real.log ↑n = log n

Tactic:
;

Goal state after:
n : ℕ
⊢ Real.log ↑n = log n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
;

Goal state after:
⊢ Λ * ↑ζ = log
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
;

Goal state after:
⊢ log * ↑μ = Λ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
;

Goal state after:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + 0 * ↑a) = p ^ 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
this : 2 ≤ p
⊢ 1 + 2 ≤ p * 1

Tactic:
;

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
this : 2 ≤ p
⊢ 1 + 2 ≤ p * 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case zero
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod 1)ˣ

Tactic:
;

Goal state after:
case zero
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod 1)ˣ
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n

Tactic:
exact sum_congr rfl fun k hk ↦ (integralmulsum c hf_diff hf_int _ _ _ (mod_cast k.le_succ)
      le_rfl (mod_cast le_rfl) (ineqofmemIco' hk).1 <| mod_cast (ineqofmemIco' hk).2)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ (pderiv R i) (X i) = Pi.single i 1 i

Tactic:
;

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ (pderiv R i) (X i) = Pi.single i 1 i
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: hn : Odd 0
⊢ False

Tactic:
;

Goal state after:
hn : Odd 0
⊢ False
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
exact hnp ▸ iff_of_true (isCyclic_units_of_prime_pow p hp (odd.ne_two_of_dvd_nat dvd_rfl) _)
      ⟨p, _, hp, odd, rfl⟩

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

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod 0)ˣ ↔ 0 = 0 ∨ 0 = 1 ∨ 0 = 2 ∨ 0 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (0 = p ^ m ∨ 0 = 2 * p ^ m)

Tactic:
;

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod 0)ˣ ↔ 0 = 0 ∨ 0 = 1 ∨ 0 = 2 ∨ 0 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (0 = p ^ m ∨ 0 = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod 1)ˣ ↔ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (1 = p ^ m ∨ 1 = 2 * p ^ m)

Tactic:
;

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod 1)ˣ ↔ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (1 = p ^ m ∨ 1 = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
⊢ IsCyclic (ZMod 2)ˣ ↔ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (2 = p ^ m ∨ 2 = 2 * p ^ m)

Tactic:
;

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
⊢ IsCyclic (ZMod 2)ˣ ↔ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (2 = p ^ m ∨ 2 = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod 4)ˣ ↔ 4 = 0 ∨ 4 = 1 ∨ 4 = 2 ∨ 4 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (4 = p ^ m ∨ 4 = 2 * p ^ m)

Tactic:
;

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod 4)ˣ ↔ 4 = 0 ∨ 4 = 1 ∨ 4 = 2 ∨ 4 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (4 = p ^ m ∨ 4 = 2 * p ^ m)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, ‖f x‖ₑ.toReal • ‖f x‖⁻¹ • f x ∂μ

pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ.restrict s)

pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ₑ < ∞

Tactic:
;

Goal state after:
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, ‖f x‖ₑ.toReal • ‖f x‖⁻¹ • f x ∂μ

X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ.restrict s)

X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ₑ < ∞