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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ENNReal.ofReal (ε / 2 + ε / 2) = ENNReal.ofReal ε

Tactic:
add_halves

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ENNReal.ofReal ε = ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
h : ∀ (δ : ℝ), 0 < δ → ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
⊢ ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
choose f hf₀ hf₁ using h
  intro H
  obtain ⟨ε, -, hε', hε₀⟩ := exists_seq_strictAnti_tendsto_nhdsWithin (0 : ℝ)
  refine not_eventually.2
    (Frequently.of_forall fun _ ↦ lt_irrefl <| ENNReal.ofReal <| 4⁻¹ ^ Fintype.card ι)
    ((Filter.Tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds ?_).mono fun n ↦
      lt_of_le_of_lt ?_)
  on_goal 2 =>
    calc
      ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)
        = volume (closedBall (f (ε n) (hε' n)) (ε n / 4)) / volume (closedBall x (ε n)) := ?_
      _ ≤ volume (closure s ∩ closedBall x (ε n)) / volume (closedBall x (ε n)) := by
        gcongr
        exact subset_inter ((hf₁ _ <| hε' n).trans interior_subset_closure) <| hf₀ _ <| hε' n
    have := hε' n
    rw [Real.volume_pi_closedBall, Real.volume_pi_closedBall, ← ENNReal.ofReal_div_of_pos,
      ← div_pow, mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div]
  all_goals positivity

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

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
m.extend_eq hC hf_mem

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (f x).fst) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ

Tactic:
simp_rw [← WithLp.ofLp_fst, ← WithLp.ofLp_snd, ← memLp_prod_iff]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (f x).ofLp) p μ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
E : Set X
hE : MeasurableSet E
hE' : ¬⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
simp only [variation_apply, preVariation, ennrealToMeasure_apply hE, ennrealPreVariation_apply]

Goal state after:
case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
E : Set X
hE : MeasurableSet E
hE' : ¬⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ preVariationFun (fun x ↦ ‖μ x‖ₑ) E
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
E : Set X
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
by_cases hE : MeasurableSet E
  swap; · simp [hE]
  by_cases hE' : (⟨E, hE⟩ : Subtype MeasurableSet) = ⊥
  · simp_all
  simp only [variation_apply, preVariation, ennrealToMeasure_apply hE, ennrealPreVariation_apply]
  calc
    ‖μ E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖μ p‖ₑ := by simp
    _ ≤ preVariationFun (‖μ ·‖ₑ) E := by apply preVariation.sum_le

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

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup V
μ ν : VectorMeasure X V
inst✝ : Finite X
⊢ μ.variation Set.univ < ∞

Tactic:
classical
    let : Fintype X := Fintype.ofFinite X
    simp only [variation_apply, preVariation_apply, MeasurableSet.univ, ennrealToMeasure_apply,
      ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
    exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])

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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
hs : s ∈ C'
⊢ s ∈ {s | ‖m₁ s‖ₑ ≤ μ ↑s}

Tactic:
simp only [Set.mem_ofPred_eq]

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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
hs : s ∈ C'
⊢ ‖m₁ s‖ₑ ≤ μ ↑s
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
heqa : h.choose = a
A : ⋯.choose {a} = 0
⊢ Function.rightLim f ⋯.choose - f ⋯.choose = Function.rightLim f a - Function.leftLim f a

Tactic:
simpa only [heqa, sub_right_inj] using (leftLim_eq_of_isBot ha).symm

Goal state after:
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
t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
ht : MeasurableSet t
hf : AEStronglyMeasurable f (μ.variation.restrict t)
this : ∫ᵛ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂[B; μ] = 0
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0

Tactic:
rw [← this]

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
t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
ht : MeasurableSet t
hf : AEStronglyMeasurable f (μ.variation.restrict t)
this : ∫ᵛ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂[B; μ] = 0
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂[B; μ]
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✝¹ : 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α
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ AEStronglyMeasurable ((f i).indicator 1) μ

Tactic:
exact AEStronglyMeasurable.indicator (by fun_prop) (f_meas i)

Goal state after:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ ‖B‖₊ ^ (ENNReal.toReal 1)⁻¹ • eLpNorm (f - ⇑g) 1 μ.variation ≤ ↑δ

Tactic:
grw [h'g.le]

Goal state after:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ ‖B‖₊ ^ (ENNReal.toReal 1)⁻¹ • ↑ρ ≤ ↑δ
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ μ.variation ≤ μ.variation + μ.variation

Tactic:
← add_zero μ.variation

Goal state after:
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ μ.variation + 0 ≤ μ.variation + μ.variation
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
hfg : f ≤ g
⊢ f.symm ≤ g.symm

Tactic:
rw [le_iff]
  refine ⟨cod_le_cod hfg, dom_le_dom hfg, ?_⟩
  intro x
  apply g.toEquiv.injective
  change g.toEquiv (inclusion _ (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm _)
  rw [g.toEquiv.apply_symm_apply, (Equiv.apply_symm_apply f.toEquiv x).symm,
    f.toEquiv.symm_apply_apply]
  exact toEquiv_inclusion_apply hfg _

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
a₁✝ a₂✝ : M ↪[L] N
x✝ : M
w✝ : ((fun f ↦ f.toPartialEquiv) a₁✝).dom = ((fun f ↦ f.toPartialEquiv) a₂✝).dom
H :
  ∀ (x : M) (h : x ∈ ((fun f ↦ f.toPartialEquiv) a₁✝).dom),
    ((fun f ↦ f.toPartialEquiv) a₁✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
      ((fun f ↦ f.toPartialEquiv) a₂✝).cod.subtype (((fun f ↦ f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
exact H _ (Substructure.mem_top _)

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 : ι → ℕ
f : ↑hs.basisSet → ℕ
⊢ toRatVec hs.base +
      ∑ i, Int.fract ((hs.basis.repr (toRatVec (x + ∑ i, f i • ↑i) - toRatVec hs.base)) i) • toRatVec ↑i =
    toRatVec (hs.fract x)

Tactic:
hs.toRatVec_fract_eq

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ toRatVec (hs.fract x) = toRatVec x

Tactic:
hs.toRatVec_fract_eq

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

Tactic:
rw [mem_closure_singleton] at hy

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : ∃ n, n • ↑i = y
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + ↑i + y + z' = hs.base + z
⊢ hs.floor x i < 0
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 α
x y : β
hxy : x < y
⊢ Nonempty (α ↪o β)

Tactic:
obtain ⟨a, ha⟩ := exists_between 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
a : β
ha : x < a ∧ a < y
⊢ Nonempty (α ↪o β)
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
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i

Tactic:
rw [mem_closure_singleton] at hy

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : ∃ n, n • ↑i = y
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
⊢ L.IsExtensionPair M N

Tactic:
intro ⟨f, f_FG⟩

Goal state after:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∀ (m : M), ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: this : Language.empty.Structure (ULift.{w, 0} ℕ)
⊢ IsFraisse {S | Finite ↑S}

Tactic:
exact (isFraisseLimit_of_countable_infinite (ULift ℕ)).isFraisse

Goal state after:
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ IsAlmostPrime 2 (p ^ 2)

Tactic:
by
  simpa [pow_two] using hp.mul_isAlmostPrime_two hp

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

Goal state before:
pp: h : Monoid.exponent (ZMod 8)ˣ ∣ 2
h' : Monoid.exponent (ZMod 8)ˣ = 4
⊢ False

Tactic:
simp [h'] at h

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

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 0 < n

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 0 < n
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1)) (pderivFun i g)) +
      MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) g * (trunc R (n + single i 1)) (pderivFun i f))

Tactic:
trunc_pderivFun,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    MvPolynomial.coeff n
        ((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
      MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) g * (trunc R (n + single i 1)) (pderivFun i f))
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    MvPolynomial.coeff n
        ((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
      MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) g * (trunc R (n + single i 1)) (pderivFun i f))

Tactic:
trunc_pderivFun,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    MvPolynomial.coeff n
        ((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
      MvPolynomial.coeff n
        ((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f))