mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
⊢ μ (s ∩ t) = 1

Tactic:
rcases μ.zero_one s with (_ | hμs)

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
⊢ μ (s ∩ t) = 1

case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs✝ : μ s = 1
hμt : μ t = 1
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
⊢ μ (s ∩ t) = 1
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ 0 < ↑(u n)

Tactic:
norm_cast; exact u_pos n

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ ⋃ i, s ∩ f i ∈ C

Tactic:
← inter_iUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ s ∩ ⋃ i, f i ∈ C
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
i : ℕ
⊢ f i \ s = ⋃₀ ↑(A i)

Tactic:
simp [A, IsSetSemiring.sUnion_disjointOfDiff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ b ≤ 1 - ε

Tactic:
apply le_trans (h c le_rfl)

Goal state after:
case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ ↑((μ (sub c)) (⋃ i, ⋃ (_ : i ≤ sub c), U i)) ≤ 1 - ε
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
⊢ (μ.restrict s).variation ≤ μ.variation.restrict s

Tactic:
by_cases hs : MeasurableSet s
  · simp [variation_restrict hs]
  · simp [restrict_not_measurable _ hs, Measure.zero_le]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case e_a
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ∑' (i : ℕ), 2 ^ (-1 - ↑i) = 1

Tactic:
exact tsum_two_zpow_neg_add_one

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε

Tactic:
have It : ‖m t' - m₁ t‖ₑ < δ := by
      have : m₁ ⟨t', hCmeas _ t'C⟩ = m t' :=
        C'_dense.extend_eq lip.continuous ⟨⟨t', hCmeas _ t'C⟩, ⟨t', t'C, rfl⟩⟩
      rw [← this, ← edist_eq_enorm_sub]
      apply (m₁_lip _ _).trans_lt
      simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul]
      exact ht'

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: 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
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : MeasurableSingletonClass X
a : X
inst✝ : CompleteSpace G
⊢ ∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})

Tactic:
simp only [restrict_singleton, integral_dirac]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation (s ∪ t) ≤
    (⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s) + ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
apply (measure_union_le _ _).trans

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s + (μ.mapRange ↑ℓ ⋯).variation t ≤
    (⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s) + ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
⊢ VectorMeasure.Integrable 0 f

Tactic:
simp [VectorMeasure.Integrable]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: 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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
i : ι
⊢ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.restrict (s i)).variation ≤ (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) i

Tactic:
dsimp

Goal state after:
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
i : ι
⊢ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.restrict (s i)).variation ≤ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ∀' liftAt 1 n φ).Realize v xs

Tactic:
realize_iff,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ (∀' liftAt 1 n φ).Realize v xs
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ φ.toPrenex).Realize v xs

Tactic:
realize_iff,

Goal state after:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ φ.toPrenex.Realize v xs
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
h : CG L M
f : M →[L] N
hs : Function.Surjective ⇑f
⊢ CG L N

Tactic:
by
  rw [← Hom.range_eq_top] at hs
  rw [cg_def, ← hs]
  exact h.range f

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ Countable ↥⊤ ↔ Countable M

Tactic:
topEquiv.toEquiv.countable_iff

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ Countable M ↔ Countable M
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
⊢ IsSemilinearSet ({x | ∃ x_1, u + A *ᵥ x_1 = x} ∩ {x | ∃ x_1, v + B *ᵥ x_1 = x})

Tactic:
← ofPred_and,

Goal state after:
ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
⊢ IsSemilinearSet {a | (∃ x, u + A *ᵥ x = a) ∧ ∃ x, v + B *ᵥ x = a}
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.toEquiv ((inclusion ⋯) x) = (inclusion ⋯) (f.toEquiv x)

Tactic:
by
  apply (subtype _).injective
  change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _
  rw [subtype_toEquiv_inclusion h]
  simp

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

Goal state before:
pp: case mem
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y✝ : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
y : ι → ℕ
hy : y ∈ t
⊢ (hs.basis.repr (toRatVec y)) i = 0

Tactic:
| mem y hy =>

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

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

Tactic:
simp only [fract]
  rw [← map_tsub_of_le _ _ _ (hs.floor_toNat_sum_le x)]
  simp only [map_add, map_sum, map_nsmul]
  rw [← sub_add_eq_add_sub, sub_add, ← Finset.sum_sub_distrib]
  conv =>
    enter [1, 2, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]
  rw [sub_eq_iff_eq_add, add_assoc, ← sub_eq_iff_eq_add', ← Finset.sum_add_distrib]
  simp only [floor]
  conv =>
    enter [2, 2, _]
    rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]
  rw [hs.basis.sum_repr]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
⊢ IsSemilinearSet
    {a |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
convert!
      Nat.isSemilinearSet_setOfPred_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) i.1 hs.base
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 1) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 0) 1) 0) using 4

Goal state after:
case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x✝ ∘ Sum.inr =
    ↑i + ((fromCols 1 1).fromCols 0).fromCols 1 *ᵥ x✝

case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + (x✝ ∘ Sum.inl) ∘ Sum.inr = hs.base + ((fromCols 0 0).fromCols 1).fromCols 0 *ᵥ x✝
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
⊢ Nonempty (α ↪o β)

Tactic:
rcases exists_pair_lt β with ⟨x, y, hxy⟩

Goal state after:
case intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
x y : β
hxy : x < y
⊢ Nonempty (α ↪o β)
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.base + ((hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j)

Tactic:
Finset.add_sum_erase _ (fun j => (hs.floor x j).toNat • j.1) (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 + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j = hs.base + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1
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:
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
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)
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k

Tactic:
have h_inc₂ : Set.uIcc t₁ t₂ ⊆ Set.Icc a b := Set.uIcc_of_le h ▸ Set.Icc_subset_Icc h₃ h₄

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 = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k
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 (p ^ 0))ˣ

pp: case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
· rw [pow_zero]; infer_instance

Goal state after:
case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
by_cases h2 : n = 2

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

case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Function.Surjective π

Tactic:
by
  suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
  convert! surjective_primeCounting'
  ext
  exact primeCounting_sub_one _

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ bernoulli' n = 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k

Tactic:
by
  rw [bernoulli']

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0

Tactic:
rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h

Goal state after:
case inl
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0

case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
coeff_add,

Goal state after:
case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i =
    (-1) ^ (n + 1) • ((bernoulli (n + 1)).coeff i + ((n + 1) • X ^ (n + 1 - 1)).coeff i)
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)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
PowerSeries.ext_iff

Goal state after:
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)!
this :
  ∀ (n_1 : ℕ),
    (coeff n_1) (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff n_1)
        (PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε

Tactic:
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x = 0 ↔ x < 2

Tactic:
refine ⟨fun h₀ ↦ ?_, psi_eq_zero_of_lt_two⟩
  by_contra! contra
  replace contra : 2 ∈ Ioc 0 ⌊x⌋₊ := by rw [mem_Ioc, le_floor_iff (by grind)]; grind
  have : Λ 2 ≤ ψ x := single_le_sum (fun n _ ↦ vonMangoldt_nonneg (n := n)) contra
  have := vonMangoldt_pos_iff.mpr prime_two.isPrimePow
  linarith

Goal state after: