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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
hs : IsSemilinearSet s
⊢ IsSemilinearSet (a +ᵥ s)

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a : M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (a +ᵥ ⋃₀ S)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

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

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f '' ⋃₀ S)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
⊢ IsSemilinearSet ↑(closure s)

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet ↑(closure (⋃₀ S))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsProperSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
⊢ IsSemilinearSet (⋃₀ S)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)

Tactic:
← sUnion_union

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ (S₁ ∪ S₂))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
s : Set M
inst✝ : IsCancelAdd M
hs : IsSemilinearSet s
⊢ IsProperSemilinearSet s

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsProperSemilinearSet (⋃₀ S)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id ↑t
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ ↑(closure ↑t) ↔ x + p ∈ a +ᵥ ↑(closure ↑t)

Tactic:
have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank

Goal state after:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id ↑t
hcard : t.card ≤ 1
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ ↑(closure ↑t) ↔ x + p ∈ a +ᵥ ↑(closure ↑t)
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: 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
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

Tactic:
by
  by_cases hf : μ.Integrable f
  · rw [integral_eq_setToFun_transpose hf]
    apply (enorm_setToFun_le _ (by simp)).trans (by simp)
  · simp [integral_undef hf]

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

Goal state before:
pp: case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ setToFun (variation μ.toSignedMeasure) ⇑(transpose μ.toSignedMeasure (lsmul ℝ ℝ).flip) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ f

Tactic:
simp only [Measure.variation_toSignedMeasure]

Goal state after:
case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ setToFun μ ⇑(transpose μ.toSignedMeasure (lsmul ℝ ℝ).flip) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : z ∈ f x
hz₂ : ¬z = 0
⊢ ∃ y_1 z_1, (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = y' + z

Tactic:
hf _ hx

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ ∃ y_1 z_1, (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = y' + z
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ f (a + x)

Tactic:
hf _ hx

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ a + x + y ∈ s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: 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
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
by
  by_cases hfm : AEStronglyMeasurable f (μ.variation.map φ)
  · by_cases h'fm : μ.Integrable (f ∘ φ)
    · apply integral_map hφ.measurable hfm h'fm
    · rw [integral_undef, integral_undef]
      · exact h'fm
      · rwa [hφ.integrable_map_vectorMeasure]
  · rw [integral_non_aestronglyMeasurable, integral_non_aestronglyMeasurable]
    · rwa [hφ.aestronglyMeasurable_map_iff] at hfm
    · rwa [hφ.variation_map]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isAtomic
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsAtomic
⊢ False

pp: case imp
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' ∼φ).IsQF
h₂✝ : ⊥.IsQF
⊢ False

Tactic:
· exact φ.not_ex_isAtomic con

Goal state after:
case imp
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' ∼φ).IsQF
h₂✝ : ⊥.IsQF
⊢ False
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ ↑S = ↑S'

Tactic:
rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ (closure L).toFun ↑(Exists.choose ⋯) = (closure L).toFun ↑(Exists.choose ⋯)
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
s : Set M
hs : IsSemilinearSet s
f : F
⊢ IsSemilinearSet (⇑f ⁻¹' s)

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Goal state after:
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 (⇑f ⁻¹' ⋃₀ S)
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⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ ∃ P s', P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val '' s'
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₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
⊢ ∃ P s₁'_1 s₂',
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧ Subtype.val '' s₁' = Subtype.val '' s₁'_1 ∧ IsSemilinearSet s₂' ∧ s₂ = Subtype.val '' s₂'

Tactic:
rcases hs₂.exists_fg_eq_subtypeVal with ⟨P₂, s₂', hP₂, hs₂', rfl⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ ∃ P s₁'_1 s₂'_1,
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val '' s₁' = Subtype.val '' s₁'_1 ∧ IsSemilinearSet s₂'_1 ∧ Subtype.val '' s₂' = Subtype.val '' s₂'_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddMonoid.FG M
inst✝ : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ IsSemilinearSet (⋂ i, s i)

Tactic:
rw [← sInter_range]
  apply sInter (finite_range s)
  simpa

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 ι
α : Type u_1
inst✝ : Finite α
x y : α → Σˣ f
xy : x ≈ y
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Sigma.fst ∘ x) a) ∩ upperBounds (range fun a ↦ (Sigma.fst ∘ y) a)
⊢ ∃ i,
    ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy

Tactic:
exact ⟨i, hi.1, hi.2, funext fun a => (equiv_iff G f _ _).1 (xy a)⟩

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

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

Tactic:
apply (span_mono (image_mono subset_union_right)).trans'

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

Goal state before:
pp: case hb
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ 0 ≤ hs.basis i

Tactic:
rw [hs.basis_apply]
    exact toRatVec_nonneg _

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

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract (x + y') = hs.fract (u + y)
⊢ hs.fract x ≠ hs.base

Tactic:
hs.fract_add_of_mem_closure hy',

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract x = hs.fract (u + y)
⊢ hs.fract x ≠ hs.base
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_2
ι : 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
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa [Subtype.val_inj] using hj

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

Goal state before:
pp: case mp.refine_3
ι : 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
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa [Subtype.val_inj] using hj

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

Goal state before:
pp: case mp.refine_2
ι : 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
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa [Subtype.val_inj] using hj

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

Goal state before:
pp: case mp.refine_3
ι : 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
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa [Subtype.val_inj] using hj

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M

Tactic:
simp only [denselyOrderedSentence, Sentence.Realize, Formula.Realize,
    BoundedFormula.realize_imp, BoundedFormula.realize_all, Term.realize_lt,
    BoundedFormula.realize_ex, BoundedFormula.realize_inf]

Goal state after:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ (∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)) ↔
    DenselyOrdered M
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: case h
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 : ↥(insert m hS.toFinset) ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
g' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr ↑((Substructure.closure Language.order).toFun {m} ⊔ S) ↑(insert m hS.toFinset)
        ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ x ∈ hS.toFinset

Tactic:
simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]

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
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_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n
hKU : closure ↑(K 0) ⊆ U
x : X
hx : x ∈ ⋂ n, closure ↑(K n)
⊢ x ∈ U ∩ ⋂ n, f n

Tactic:
by
    simp only [mem_iInter, mem_inter_iff] at hx ⊢
    exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩

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
hG : IsGδ s
this✝ : LocallyCompactSpace ↑(closure s)
this : BaireSpace ↑(closure s)
⊢ Dense (Subtype.val ⁻¹' s)

Tactic:
simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure]

Goal state after:
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
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
⊢ IsSatisfiable ↑x

Tactic:
have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ

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
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
this : ∀ φ ∈ x, T.typesWith φ ∈ ↑F
⊢ IsSatisfiable ↑x
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 : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.134 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.134 ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ orderOf (1 + ↑p) = p ^ n

Tactic:
by
  convert! orderOf_one_add_mul_prime hp hp2 1 _ n
  · simp
  · intro H
    apply hp.ne_one
    simpa using Int.eq_one_of_dvd_one (Int.natCast_nonneg p) H

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

Goal state before:
pp: n : ℕ
⊢ orderOf 5 = 2 ^ n

Tactic:
convert! orderOf_one_add_four_mul 1 (by simp) n

Goal state after:
n : ℕ
⊢ 5 = 1 + 4 * ↑1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
exact Nat.not_odd_zero hn

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

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ 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:
rw [h0]; simp [isCyclic_units_zero]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ derivative (bernoulli 0) = ↑0 * bernoulli (0 - 1)

Tactic:
rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow

Tactic:
by
  rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range n,
      (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) =
    0

Tactic:
refine sum_eq_zero ?_

Goal state after:
n : ℕ
⊢ ∀ x ∈ range n,
    (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _), sum_cons, ← Icc_add_one_left_eq_Ioc,
      Icc_eq_cons_Ioc (by lia), sum_cons]

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 + (f ↑(0 + 1) * c (0 + 1) + ∑ x ∈ Ioc (0 + 1) ⌊b⌋₊, f ↑x * c x) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.e_a
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)

Tactic:
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast

Goal state after:
case succ.e_a
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn✝ : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
· calc
        (n + 1)# = n# := primorial_succ hn ho
        _ < 4 ^ n := ihn n n.lt_succ_self (by grind)
        _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ

Goal state after: