mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : ¬AEStronglyMeasurable f (Measure.map φ μ.variation)
⊢ ¬AEStronglyMeasurable f (μ.map φ).variation

Tactic:
rwa [hφ.variation_map]

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), φ.Realize v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), ψ.Realize v (Fin.snoc xs a)

Tactic:
exact fun M v xs => forall_congr' fun a => h.realize_bd_iff

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih1 : ∀ {ψ : L.BoundedFormula α (n✝ + 1)}, ψ.IsPrenex → (φ✝.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∀' φ✝).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih1 hψ.liftAt).ex

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs

Tactic:
by
  induction φ with
  | falsum => exact Iff.rfl
  | equal => exact Iff.rfl
  | rel => exact Iff.rfl
  | imp f1 f2 h1 h2 =>
    intros
    rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
  | all _ h =>
    intros
    rw [realize_all, toPrenex, realize_all]
    exact forall_congr' fun a => h

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
g_inj : Function.Injective g
⊢ Countable (M →[L] N)

Tactic:
have : Finite ↑S := (S.finite_coe_iff).2 finite_S

Goal state after:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
g_inj : Function.Injective g
this : Finite ↑S
⊢ Countable (M →[L] N)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs

Tactic:
induction hU with

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ P, (∃ n f, AddMonoidHom.mrange f = P) ∧ s = a +ᵥ ↑P
P : AddSubmonoid M
n : ℕ
f : (Fin n → ℕ) →+ M
hf : AddMonoidHom.mrange f = P
hs : s = a +ᵥ ↑P
⊢ s = a +ᵥ ↑P

Tactic:
hs

Goal state after:
case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ P, (∃ n f, AddMonoidHom.mrange f = P) ∧ s = a +ᵥ ↑P
P : AddSubmonoid M
n : ℕ
f : (Fin n → ℕ) →+ M
hf : AddMonoidHom.mrange f = P
hs : s = a +ᵥ ↑P
⊢ a +ᵥ ↑P = a +ᵥ ↑P
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ ↑(AddMonoidHom.mrange f)
⊢ s = a +ᵥ ↑(AddMonoidHom.mrange f)

Tactic:
hs

Goal state after:
case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ ↑(AddMonoidHom.mrange f)
⊢ a +ᵥ ↑(AddMonoidHom.mrange f) = a +ᵥ ↑(AddMonoidHom.mrange f)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : AddMonoid.FG M
F : Type u_5
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
⊢ IsSemilinearSet (⇑f ⁻¹' s)

Tactic:
by
  rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, g, hg⟩
  rw [AddMonoidHom.mrange_eq_top] at hg
  rw [← image_preimage_eq (f ⁻¹' s) hg]
  apply image
  rw [← preimage_comp, ← AddMonoidHom.coe_coe, ← AddMonoidHom.coe_comp]
  exact Nat.isSemilinearSet_preimage hs _

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) =
    ↑⟨a, ⋯⟩ +ᵥ ↑(AddSubmonoid.map (closure (insert a t)).subtype (closure (⇑(closure (insert a t)).subtype ⁻¹' t)))

Tactic:
AddMonoidHom.map_mclosure

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) = ↑⟨a, ⋯⟩ +ᵥ ↑(closure (⇑(closure (insert a t)).subtype '' ⇑(closure (insert a t)).subtype ⁻¹' t))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
⊢ ∃ P s', P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val '' s'

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩
  choose! P t hP ht ht' using fun s hs => (hS' s hs).exists_fg_eq_subtypeVal
  have : Finite S := hS
  refine ⟨⨆ s : S, P s, ⋃ (s : S), AddSubmonoid.inclusion (le_iSup _ s) '' t s.1,
    .iSup _ fun s => hP s s.2, .iUnion fun s => (ht s s.2).isSemilinearSet.image _, ?_⟩
  simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
this : Fintype ι
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
isLinearSet_iff_exists_matrix

Goal state after:
ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : ∃ v n A, s₁ = {x | ∃ x_1, v + A *ᵥ x_1 = x}
hs₂ : ∃ v n A, s₂ = {x | ∃ x_1, v + A *ᵥ x_1 = x}
this : Fintype ι
⊢ IsSemilinearSet (s₁ ∩ s₂)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
⊢ hs.fundamentalDomain.Finite

Tactic:
apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
⊢ hs.fundamentalDomain ⊆ Iic (hs.base + ∑ i, ↑i)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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 = ⊤
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Tactic:
exact ⟨toEmbeddingOfEqTop isTop,
        by convert! (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) → ⟦N⟧ ∈ Quotient.mk' '' L.age M

pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧

Tactic:
· rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Language.simpleGraphOfStructure V = G

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : p1 < a ∧ p2 < b
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
← cmp_eq_lt_iff,

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ p2 < b
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
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 + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 =
    hs.base + (∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j + (hs.floor x i).toNat • ↑i)

Tactic:
Finset.sum_erase_add _ _ (Finset.mem_univ i),

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 + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.base + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1
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
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.fract (hs.base + z)
⊢ hs.fract x = hs.base

Tactic:
hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz),

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

Tactic:
Finset.sum_erase_add _ _ (Finset.mem_univ i),

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 + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.base + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1
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 : hs.fract x = hs.fract (hs.base + ↑i + y + z)
⊢ hs.fract x = hs.base

Tactic:
hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz),

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 : hs.fract x = hs.fract (hs.base + ↑i + y)
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨S_fg, ⟨subtype _⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
← setOfPred_subset_eq_empty_iff

Goal state after:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
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, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U

Tactic:
rcases U_open.exists_positiveCompacts_closure_subset U_nonempty with ⟨K₀, hK₀⟩

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)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ ¬IsSatisfiable ((L.lhomWithConstants α).onTheory T ∪ ∅) ↔ Set.univ = ∅

Tactic:
← setOfPred_subset_eq_empty_iff

Goal state after:
L : Language
T : L.Theory
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑r

Tactic:
by exact_mod_cast h3r

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

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1)
k : ℕ
hk : k ≤ n - 1
h : exponent (ZMod (2 ^ n))ˣ = 2 ^ k
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)

Tactic:
have := IsCyclic.iff_exponent_eq_card.not.mp <| ZMod.isCyclic_units_two_pow_iff n |>.not.mpr hn'

Goal state after:
case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1)
k : ℕ
hk : k ≤ n - 1
h : exponent (ZMod (2 ^ n))ˣ = 2 ^ k
this : ¬exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑p ^ (n + m) * ↑a + ↑p ^ (n + m + 1) * y = 0

Tactic:
simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]

Goal state after:
case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(p ^ (n + m)) * ↑a = 0
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case zero
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ 1 = constantCoeff (exp A)

Tactic:
constantCoeff_exp

Goal state after:
case zero
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ 1 = 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n x : ℕ
hx : x ≤ n
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Tactic:
choose_symm hx,

Goal state after:
n x : ℕ
hx : x ≤ n
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose x))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.refine_1.e_f
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ (fun i ↦ ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = fun k ↦
    ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

Tactic:
funext x

Goal state after:
case succ.succ.refine_1.e_f
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
x : ℕ
⊢ ↑((n + 2).choose (x + 2)) * bernoulli (x + 2) = ↑(n.succ.succ.choose (x + 1 + 1)) * bernoulli' (x + 1 + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / (↑m ! * ↑(q - m + 1)!) * ↑n ^ (q - m + 1)

Tactic:
tsub_add_eq_add_tsub (le_of_lt_succ h),

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / (↑m ! * ↑(q + 1 - m)!) * ↑n ^ (q + 1 - m)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case refine_2
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) =
    PowerSeries.mk fun p ↦ ∑ x ∈ range (p + 1), ↑n ^ (p + 1 - x) * (bernoulli x * ↑((p + 1).choose x)) / ↑(p + 1)!

Tactic:
simp only [mul_comm, factorial]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
⊢ f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ

Tactic:
f,

Goal state after:
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
⊢ bernoulli 1 * ↑(p.succ.succ.choose 1) * ↑n ^ (p.succ.succ - 1) / ↑p.succ.succ + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x = ∑ n ∈ Icc 0 ⌊x⌋₊, Λ n

Tactic:
rw [psi, ← add_sum_Ioc_eq_sum_Icc] <;> simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
grw [psi_ge' (by linarith)]
  linarith [psi_sub_theta_le hx]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den.Coprime p
hcop_rest : (∑ i ∈ vonStaudtPrimes k with i ≠ p, 1 / ↑i).den.Coprime p
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q).den

Tactic:
have hcop := (Nat.Coprime.of_dvd_left (Rat.add_den_dvd _ _) (hcop_ind.mul_left hcop_rest)).symm

Goal state after:
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den.Coprime p
hcop_rest : (∑ i ∈ vonStaudtPrimes k with i ≠ p, 1 / ↑i).den.Coprime p
hcop :
  p.Coprime (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ i ∈ vonStaudtPrimes k with i ≠ p, 1 / ↑i).den
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q).den
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
⊢ Algebra.IsAlgebraic (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K

Tactic:
by
  exact .tower_top (K := F⟮(X : F⟮X⟯)⟯) _

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ P.det * (P.det * (traceMatrix A b).det) = P.det ^ 2 * discr A b

Tactic:
←
    mul_assoc,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ P.det * P.det * (traceMatrix A b).det = P.det ^ 2 * discr A b