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

Goal state before:
pp: case bound_integrable
ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
⊢ Integrable (fun x ↦ ↑ν.bound) μ.variation

pp: case h_lim
ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
⊢ ∀ᵐ (a : X) ∂μ.variation, Tendsto (fun n ↦ ∑ y ∈ n, ν (Prod.mk a ⁻¹' f y)) atTop (𝓝 (ν (⋃ i, Prod.mk a ⁻¹' f i)))

Tactic:
· apply integrable_const

Goal state after:
case h_lim
ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
⊢ ∀ᵐ (a : X) ∂μ.variation, Tendsto (fun n ↦ ∑ y ∈ n, ν (Prod.mk a ⁻¹' f y)) atTop (𝓝 (ν (⋃ i, Prod.mk a ⁻¹' f i)))
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s

Tactic:
apply enorm_setIntegral_le_of_enorm_le_const_ae

Goal state after:
case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hs : MeasurableSet s
⊢ ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ₑ ≤ C
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case refine_1
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
this : ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = ∫ᵛ (x : α), s.indicator 1 x ∂•m'
⊢ ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = m s

Tactic:
rw [this, integral_indicator (measurableSet_generateFrom hs)]

Goal state after:
case refine_1
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
this : ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = ∫ᵛ (x : α), s.indicator 1 x ∂•m'
⊢ ∫ᵛ (x : α) in s, 1 x ∂•m' = m s
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case pos
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : μ.Integrable f
⊢ μ.withDensity f B = μ.withDensity g B

pp: case neg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : ¬μ.Integrable f
⊢ μ.withDensity f B = μ.withDensity g B

Tactic:
· simp only [withDensity, hf, ↓reduceDIte, Integrable.congr hf h, mk.injEq]
    ext s
    apply setIntegral_congr_ae
    filter_upwards [h] with x hx xs using hx

Goal state after:
case neg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : ¬μ.Integrable f
⊢ μ.withDensity f B = μ.withDensity g B
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
⊢ ∑ i ∈ g.range, ∑ p ∈ P i, ‖i‖ₑ * ‖((μ.transpose B).restrict s) p‖ₑ + ↑δ =
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ

Tactic:
rw [Finset.sum_sigma']

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case neg
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : ¬x ≤ max k p
⊢ False

Tactic:
· simp only [not_le, Nat.lt_iff_add_one_le] at h₂
    apply Nat.mul_self_le_mul_self at h₂
    grind

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⋃ i ∈ S, ⇑f ⁻¹' i)

Tactic:
exact .biUnion hS fun s hs => isSemilinearSet_preimage_of_isLinearSet (hS' s hs) f

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
⊢ ∃ P s', P.FG ∧ IsLinearSet s' ∧ a +ᵥ ↑(closure t) = Subtype.val '' s'

Tactic:
refine ⟨_, _, (fg_iff _).2 ⟨insert a t, rfl, ht.insert a⟩,
    ⟨⟨_, mem_closure_of_mem (mem_insert a t)⟩, _, ht.preimage Subtype.val_injective.injOn, rfl⟩, ?_⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) = Subtype.val '' (⟨a, ⋯⟩ +ᵥ ↑(closure (Subtype.val ⁻¹' t)))
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case mk
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)
y : Σˣ f
i : ι
hy : y.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hx : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝, snd✝⟩ ≈ y ↔ (f ⟨fst✝, snd✝⟩.fst i hx) ⟨fst✝, snd✝⟩.snd = (f y.fst i hy) y.snd

Tactic:
cases y

Goal state after:
case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩ ↔
    (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι)) = ⊤

Tactic:
convert! (Pi.basisFun ℚ ι).span_eq

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ ⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι) = range ⇑(Pi.basisFun ℚ ι)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' hs.basisSet) = ⊤

Tactic:
rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]

Goal state after:
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
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
i : ι
hx : x.fst ≤ i
hy : y.fst ≤ i
⊢ (g i) ((f x.fst i hx) x.snd) = (g y.fst) y.snd

Tactic:
← Hg y.1 i hy

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
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
i : ι
hx : x.fst ≤ i
hy : y.fst ≤ i
⊢ (g i) ((f x.fst i hx) x.snd) = (g i) ((f y.fst i hy) y.snd)
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⌋ • toRatVec ↑x_1 ≤ toRatVec x

Tactic:
trans toRatVec x - toRatVec hs.base

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⌋ • toRatVec ↑x_1 ≤ toRatVec x - toRatVec hs.base

ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - toRatVec hs.base ≤ 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
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (lift L ι G f (fun i ↦ F.comp (of L ι G f i)) ⋯) ((of L ι G f i) x)

Tactic:
lift_of

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - toRatVec hs.base =
    ∑ 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:
conv =>
    enter [2, 2, _]
    rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - toRatVec hs.base = ∑ x_1, (hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1 • hs.basis x_1
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: α β : Type w'
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
this✝ : Language.order.Structure α := orderStructure α
this : Language.order.Structure β := orderStructure β
⊢ Nonempty (α ≃o β)

Tactic:
let := StrongHomClass.toOrderIsoClass Language.order α β (α ≃[Language.order] β)

Goal state after:
α β : Type w'
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
this✝¹ : Language.order.Structure α := orderStructure α
this✝ : Language.order.Structure β := orderStructure β
this : OrderIsoClass (α ≃[Language.order] β) α β :=
  StrongHomClass.toOrderIsoClass Language.order α β (α ≃[Language.order] β)
⊢ Nonempty (α ≃o β)
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ False

Tactic:
refine h (p.isMaximal.1.mono ?_)

Goal state after:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ {φ, Formula.not φ} ⊆ ↑p
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:
· simp [hm]

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

Goal state before:
pp: 𝕜 : 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⌋₊
t : ℝ
⊢ (t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.134 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.134 ⌊a⌋₊, c k) →
    t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
ht₁

Goal state after:
𝕜 : 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⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.134 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.134 ⌊a⌋₊, c k
⊢ t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
by
  rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]

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

Goal state before:
pp: a : ℤ
ha : Odd a
n : ℕ
⊢ ¬↑2 ∣ a

Tactic:
rwa [← Int.not_even_iff_odd, even_iff_two_dvd] at ha

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n ∣ n#

Tactic:
have : (∏ p ∈ n.primeFactors, p) ∣ (∏ p ∈ range (n + 1) with p.Prime, p) :=
    Finset.prod_dvd_prod_of_subset _ _ _ (by grind [le_of_dvd])
  rwa [Nat.prod_primeFactors_of_squarefree hn] at this

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-C 1 * X)).coeff i =
    ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i

Tactic:
← C_neg,

Goal state after:
case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (C (-1) * X)).coeff i =
    ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m

Tactic:
rw [choose_symm_add, two_mul, add_right_comm]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n : ℕ
⊢ (bernoulli (n + 1)).comp (1 - X) = (-1) ^ (n + 1) * bernoulli (n + 1)

Tactic:
trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)

Goal state after:
n : ℕ
⊢ (bernoulli (n + 1)).comp (1 - X) = ((bernoulli (n + 1)).comp (1 + X)).comp (-X)

n : ℕ
⊢ ((bernoulli (n + 1)).comp (1 + X)).comp (-X) = (-1) ^ (n + 1) * bernoulli (n + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)!
⊢ ∃ x, ¬(coeff x) ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = (coeff x) 0

Tactic:
use 1

Goal state after:
case h
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)!
⊢ ¬(coeff 1) ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = (coeff 1) 0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h₁.refine_2
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this✝ : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
⊢ (2 * n) ^ {x ∈ S | x ≤ (2 * n).sqrt}.card ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)

Goal state after:
case h₁.refine_2
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this✝ : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
x : ℕ
hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ n.primesLE, p ∣ n.lcmUpto

Tactic:
← primeFactors_lcmUpto

Goal state after:
n : ℕ
⊢ ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto