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

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
ρ : VectorMeasure (X × Y) G
hρ : ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)
this : μ.HasProd ν B
⊢ ∀ s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}, (μ.prod ν B) s = ρ s

Tactic:
rintro - ⟨s, hs, t, ht, rfl⟩
    rw [prod_apply, hρ _ _ hs ht]

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : 0 ≤[i] μ
hjm : MeasurableSet j
this : 0 ≤ μ (i ∩ j)
⊢ ↑(NNReal.mk (μ (i ∩ j)) ⋯) = ENNReal.ofReal (μ (i ∩ j))

Tactic:
ENNReal.ofReal_eq_coe_nnreal

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : 0 ≤[i] μ
hjm : MeasurableSet j
this : 0 ≤ μ (i ∩ j)
⊢ ↑(NNReal.mk (μ (i ∩ j)) ⋯) = ↑(NNReal.mk (μ (i ∩ j)) ?m.69)

X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : 0 ≤[i] μ
hjm : MeasurableSet j
this : 0 ≤ μ (i ∩ j)
⊢ 0 ≤ μ (i ∩ j)
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : μ ≤[i] 0
hjm : MeasurableSet j
this : μ (i ∩ j) ≤ 0
⊢ ↑(NNReal.mk (-μ (i ∩ j)) ⋯) = ENNReal.ofReal (-μ (i ∩ j))

Tactic:
ENNReal.ofReal_eq_coe_nnreal

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : μ ≤[i] 0
hjm : MeasurableSet j
this : μ (i ∩ j) ≤ 0
⊢ ↑(NNReal.mk (-μ (i ∩ j)) ⋯) = ↑(NNReal.mk (-μ (i ∩ j)) ?m.80)

X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : μ ≤[i] 0
hjm : MeasurableSet j
this : μ (i ∩ j) ≤ 0
⊢ 0 ≤ -μ (i ∩ j)
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
⊢ m'' s = m s

pp: case refine_2
α : 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 α
⊢ ‖m'' s‖ₑ ≤ μ s

Tactic:
· simp only [coe_mk, h'C s hs, ↓reduceIte, m'']
    have : ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = ∫ᵛ (x : α), s.indicator 1 x ∂•m' := by
      apply integral_congr_ae
      filter_upwards with x
      rw [condExp_of_stronglyMeasurable Mle]
      · exact StronglyMeasurable.indicator stronglyMeasurable_const
          (measurableSet_generateFrom hs)
      · exact (integrable_const 1).indicator (h'C s hs)
    rw [this, integral_indicator (measurableSet_generateFrom hs)]
    have : IsFiniteMeasure m'.variation :=
      isFiniteMeasure_of_le _ m'_le
    simp only [Pi.one_apply, setIntegral_const]
    simp [m'C s hs]

Goal state after:
case refine_2
α : 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 α
⊢ ‖m'' s‖ₑ ≤ μ s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)

Tactic:
conv =>

Goal state after:
α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| (List.map (fun i ↦ Term.realize v (f i)) s.toList).sum
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.add
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x y : M
hx✝ : x ∈ closure (a +ᵥ ↑(closure t))
hy✝ : y ∈ closure (a +ᵥ ↑(closure t))
ih₁ : x = 0 ∨ ∃ y ∈ closure (insert a t), a + y = x
ih₂ : y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = y
⊢ x + y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = x + y

Tactic:
rcases ih₁ with rfl | ⟨x, hx, rfl⟩

Goal state after:
case mp.add.inl
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x y : M
hy✝ : y ∈ closure (a +ᵥ ↑(closure t))
ih₂ : y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = y
hx✝ : 0 ∈ closure (a +ᵥ ↑(closure t))
⊢ 0 + y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = 0 + y

case mp.add.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ y : M
hy✝ : y ∈ closure (a +ᵥ ↑(closure t))
ih₂ : y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = y
x : M
hx : x ∈ closure (insert a t)
hx✝ : a + x ∈ closure (a +ᵥ ↑(closure t))
⊢ a + x + y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = a + x + y
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
hpt : p t ∣ S.lcm p
⊢ x ∈ t ↔ x + S.lcm p ∈ t

Tactic:
dvd_iff_exists_eq_mul_left

Goal state after:
case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
hpt : ∃ c, S.lcm p = c * p t
⊢ x ∈ t ↔ x + S.lcm p ∈ t
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl.add
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 2 → presburger[[↑A]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap presburgerFunc.add fun i ↦ Term.realize v (ts i)) = k 0 + k 1 + (u 0 + u 1) ⬝ᵥ v

Tactic:
add_dotProduct,

Goal state after:
case func.inl.add
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 2 → presburger[[↑A]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap presburgerFunc.add fun i ↦ Term.realize v (ts i)) = k 0 + k 1 + (u 0 ⬝ᵥ v + u 1 ⬝ᵥ v)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A s : Set ℕ
⊢ IsSemilinearSet (⇑(LinearEquiv.funUnique (Fin 1) ℕ ℕ) '' {x | x 0 ∈ s}) ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
← preimage_ofPred_eq

Goal state after:
A s : Set ℕ
⊢ IsSemilinearSet (⇑(LinearEquiv.funUnique (Fin 1) ℕ ℕ) '' (fun x ↦ x 0) ⁻¹' {a | a ∈ s}) ↔
    ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Module: Mathlib.ModelTheory.Equivalence

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

Tactic:
by
  rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
  exact h M v xs

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
⊢ (φ.toPrenexImpRight ψ).IsPrenex

Tactic:
by
  induction hψ with
  | of_isQF hψ => rw [hψ.toPrenexImpRight]; exact (hφ.imp hψ).isPrenex
  | all _ ih1 => exact (ih1 hφ.liftAt).all
  | ex _ ih2 => exact (ih2 hφ.liftAt).ex

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∃ a, (φ✝.toPrenexImp (liftAt 1 n✝ ψ)).Realize v (snoc xs a)) ↔ (∀' φ✝ ⟹ ψ).Realize v xs

Tactic:
refine _root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∃ a, (φ✝ ⟹ liftAt 1 n✝ ψ).Realize v (snoc xs a)) ↔ (∀' φ✝ ⟹ ψ).Realize v xs
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
⊢ ∀ {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ

Tactic:
φ

Goal state after:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ✝ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
⊢ φ.IsPrenex → P φ
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case a.inr
ι : Type u_1
inst✝ : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)}, IsSlice s → ∀ (a : ι → ℕ), (∀ x ∈ s, ∀ i ∉ t_1, x i = a i) → IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
⊢ IsSemilinearSet ({y | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y | y ∈ s ∧ y i = j})

Tactic:
refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]

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

Goal state before:
pp: ι : Type u_3
x y : ι → ℕ
⊢ toRatVec x = toRatVec y ↔ x = y

Tactic:
refine ⟨fun h => ?_, congr_arg toRatVec⟩

Goal state after:
ι : Type u_3
x y : ι → ℕ
h : toRatVec x = toRatVec y
⊢ x = y
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 ι
i j : ι
hij : i ≤ j
x : G i
⊢ (of L ι G f j) ((f i j hij) x) = (of L ι G f i) x

Tactic:
by
  rw [of_apply, of_apply, Quotient.eq]
  refine Setoid.symm ⟨j, hij, refl j, ?_⟩
  simp only [DirectedSystem.map_self]

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 : ι → ℕ
i : ↑hs.basisSet
n : ℕ
⊢ hs.floor (x + n • ↑i) i = hs.floor x i + ↑n

Tactic:
by
  simp only [floor]
  rw [map_add, ← sub_add_eq_add_sub]
  simp [-nsmul_eq_mul, ← hs.basis_apply]

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 : ι → ℕ
| ∑ x_1,
      (⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
        (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1) ≤
    toRatVec x

Tactic:
conv =>

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝
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 - toRatVec hs.base

Tactic:
conv =>

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ i, (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
conv =>

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| hs.floor x x✝ • toRatVec ↑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 =>

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| (hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝ • hs.basis x✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝¹ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange },
                    ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝

Tactic:
simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
      Embedding.equivRange_apply, eq_f']

Goal state after:
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 = ⊤
⊢ ↑g ≤ (toEmbeddingOfEqTop isTop).toPartialEquiv

Tactic:
convert! (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding

Goal state after:
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 + ↑i + ((-hs.floor x i).toNat - 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
add_assoc x,

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 + (↑i + ((-hs.floor x i).toNat - 1) • ↑i) + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
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 + (-hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
add_assoc x,

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 + ((-hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j) =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + ↑i + n • ↑i) i = 0
⊢ hs.floor x i < 0

Tactic:
add_assoc x,

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + (↑i + n • ↑i)) i = 0
⊢ hs.floor x i < 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ hs.setOfFloorNeg =
    ⋃ i,
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z}

pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet
    (⋃ i,
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z})

Tactic:
· ext x
    simp only [setOfFloorNeg, mem_iUnion, mem_ofPred_eq]
    constructor
    · intro ⟨hx, i, hi⟩
      refine ⟨i, ((- hs.floor x i).toNat - 1) • i.1, ?_,
        ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
        ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.1, ?_, ?_⟩
      · exact nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · rw [add_assoc x, ← succ_nsmul',
          tsub_add_cancel_of_le
            ((Int.le_toNat (neg_pos.2 hi).le).2 (le_neg.1 (Int.cast_le_neg_one_of_neg hi))),
          add_assoc x,
          Finset.add_sum_erase _ (fun j => (-hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 hi.le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x
    · intro ⟨i, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, ?_⟩
      · apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz), hs.fract_base] at heq
      · rw [mem_closure_singleton] at hy
        rcases hy with ⟨n, rfl⟩
        apply congr_arg (hs.floor · i) at heq
        rw [hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz,
          hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',
          hs.floor_base, add_assoc x, ← succ_nsmul', hs.floor_add_nsmul_self,
          ← eq_neg_iff_add_eq_zero] at heq
        simpa [heq] using neg_one_lt_zero.trans_le (Nat.cast_nonneg _)

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet
    (⋃ i,
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₁' \ ⇑f ⁻¹' s₂')

Tactic:
apply Nat.isSemilinearSet_sdiff <;> apply Nat.isSemilinearSet_preimage <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3

Tactic:
conv =>

Goal state after:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ {1, 2}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4

Tactic:
conv =>

Goal state after:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ {2, 3}
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6

Tactic:
conv =>

Goal state after:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ {3, 4, 5}
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: a b : ℕ
h : a ∣ b
⊢ λ a ∣ λ b

Tactic:
cases b

Goal state after:
case zero
a : ℕ
h : a ∣ 0
⊢ λ a ∣ λ 0

case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ λ a ∣ λ (n✝ + 1)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case hfin
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)
⊢ (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1

Tactic:
obtain ⟨y, hy⟩ := this (n + 1)
        rw [hy, ← pow_add, ← Nat.cast_pow]
        simp

Goal state after: