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

Goal state before:
pp: case refine_1
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
f : (n : ℕ) × (Fin n → ↑u) × (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun nds ↦ key nds.fst nds.snd.1 nds.snd.2
this✝¹ : Countable ↑𝒜₀
this✝ : Countable ↑u
this : D ⊆ range f
⊢ D.Countable

Tactic:
exact (countable_range f).mono this

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

Goal state before:
pp: 𝓧 : 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
⊢ ∑' (m : ℕ),
      (1 -
        ↑μ
          (⋃ i,
            ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))) ≤
    ∑' (m : ℕ), ε * 2 ^ (-(↑m + 1))

Tactic:
by
      refine ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_
      replace hbound := (hbound (m + 1) μ hs).le
      simp_all only [neg_add_rev, Int.reduceNeg, tsub_le_iff_right, Nat.cast_add, Nat.cast_one,
          ← coe_ofNat, ← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
      grw [hbound]
      gcongr with i hi
      grw [← subset_closure (s := ball (D i) (u m)), ball_subset_ball]
      exact hu_anti.antitone (by grind)

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ∑ p ∈ P, ‖μ p‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
A : ∑ x ∈ P with μ x < 0, |μ x| = -μ (⋃ x ∈ {x ∈ P | μ x < 0}, x)
⊢ μ (⋃ p ∈ {x ∈ P | μ x < 0}, p) ≤ 0

Tactic:
rw [← neg_nonneg, ← A]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ∑ p ∈ P, ‖μ p‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
A : ∑ x ∈ P with μ x < 0, |μ x| = -μ (⋃ x ∈ {x ∈ P | μ x < 0}, x)
⊢ 0 ≤ ∑ x ∈ P with μ x < 0, |μ x|
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 b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0

Tactic:
simp only [hx, ↓reduceDIte]

Goal state after:
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 b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ (VectorMeasure.dirac ⋯.choose (Function.rightLim f ⋯.choose - f ⋯.choose)) (Ioc a b) = 0
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 : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 * (1 + ‖μ s‖ₑ) ≤ 2 * ‖μ t‖ₑ

Tactic:
rw [mul_add, add_comm, mul_one]

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 * ‖μ s‖ₑ + 2 ≤ 2 * ‖μ t‖ₑ
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
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
u : ℕ → Set X := fun n ↦ s n \ s (n + 1)
hu : ∀ (n : ℕ), 1 ≤ ‖μ (u n)‖ₑ
⊢ False

Tactic:
have s_anti : Antitone s := by
    apply antitone_nat_of_succ_le (fun n ↦ ?_)
    simp only [Function.iterate_succ', Function.comp_apply, s]
    apply t_subs _ (hs n).1 (hs n).2

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
u : ℕ → Set X := fun n ↦ s n \ s (n + 1)
hu : ∀ (n : ℕ), 1 ≤ ‖μ (u n)‖ₑ
s_anti : Antitone s
⊢ False
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
⊢ (μ.prod ν B) univ = ρ univ

Tactic:
← univ_prod_univ,

Goal state after:
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
⊢ (μ.prod ν B) (univ ×ˢ univ) = ρ (univ ×ˢ univ)
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
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSingletonClass X
inst✝ : CompleteSpace G
a : X
v : F
this : IsFiniteMeasure ((dirac a v).transpose B).variation
⊢ ∫ᵛ (x : X), f x ∂[B; dirac a v] = ∫ᵛ (x : X), f a ∂[B; dirac a v]

Tactic:
apply integral_congr_ae
      simp only [variation_dirac]
      exact Measure.ae_smul_measure (ae_eq_dirac f) _

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

Goal state before:
pp: case _1
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s

pp: case _2
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k ≤ k + (x - k) % p

pp: case _3
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p < k + p

pp: case _4
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p + (x - k) / p * p = x

Tactic:
· rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx
          generalize (x - k) / p = m at hx
          induction m with grind

Goal state after:
case _2
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k ≤ k + (x - k) % p

case _3
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p < k + p

case _4
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p + (x - k) / p * p = x
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case hbc.h
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
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation ≤ ∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation

Tactic:
apply lintegral_mono_ae

Goal state after:
case hbc.h
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
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.variation, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal C
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
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
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
hμ : ¬μ.variation = 0
this : (ae μ.variation).NeBot
hC : 0 ≤ C
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal = ‖B‖ * (C * μ.variation.real univ)

Tactic:
simp [ENNReal.toReal_ofReal hC, Measure.real]

Goal state after:
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 ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}

Tactic:
refine ⟨a, ha.1, ?_⟩

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
⊢ IsSemilinearSet {y | y ∈ s ∧ a ≤ y}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        ∃ x ∈ {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)},
          x = (LinearEquiv.funCongrLeft ℕ ℕ e).symm (Sum.elim a (Fin.cons a_1 finZeroElim))}

Tactic:
LinearEquiv.funCongrLeft_symm,

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        ∃ x ∈ {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)},
          x = (LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim))}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: 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

Tactic:
simp only [LinearEquiv.funUnique_apply, Function.eval, Fin.default_eq_zero, ofPred_mem_eq]

Goal state after:
A s : Set ℕ
⊢ IsSemilinearSet ((fun a ↦ a 0) '' (fun x ↦ x 0) ⁻¹' s) ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ N ≤ (closure L).toFun ∅

Tactic:
rw [← SetLike.coe_subset_coe, h]

Goal state after:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∅ ⊆ ↑((closure L).toFun ∅)
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

pp: case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
· refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩
      rw [← SetLike.coe_subset_coe, h]
      exact empty_subset _

Goal state after:
case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_1
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₂')
⊢ Subtype.val '' s₁' = (fun x ↦ ↑((AddSubmonoid.inclusion ⋯) x)) '' s₁'

Tactic:
AddSubmonoid.coe_inclusion

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

Goal state before:
pp: case refine_2
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₂')
⊢ Subtype.val '' s₂' = (fun x ↦ ↑((AddSubmonoid.inclusion ⋯) x)) '' s₂'

Tactic:
AddSubmonoid.coe_inclusion

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
j : ι → ℕ
hj : j ∈ t
| f j • toRatVec j

Tactic:
rw [← (f j).toNat_sub_toNat_neg]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
j : ι → ℕ
hj : j ∈ t
| (↑(f j).toNat - ↑(-f j).toNat) • toRatVec j
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ (Std.Irrefl fun x y ↦ RelMap adj ![x, y]) ∧ Std.Symm fun x y ↦ RelMap adj ![x, y]

Tactic:
exact ⟨G.loopless, G.symm⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ x ∈ ↑(DirectLimit.of L ι G f i).toHom.range

Tactic:
refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (DirectLimit.of L ι G f i).toHom ((f (out x).fst i ⋯) (out x).snd) = x
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑(Finset.image ⇑(Equiv.prodComm β α).symm ↑f) ⊆ ↑↑f'

Tactic:
Finset.coe_subset

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ Finset.image ⇑(Equiv.prodComm β α).symm ↑f ⊆ ↑f'
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝² : L.IsOrdered
inst✝¹ : L.Structure M
h : M ⊨ L.linearOrderTheory
inst✝ : DecidableRel fun a b ↦ RelMap leSymb ![a, b]
⊢ leSymb.total ∈ L.linearOrderTheory

Tactic:
by simp [linearOrderTheory]

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
    ext
    simp [subset_def]
  simp_rw [h, sInter_eq_univ, ← setOfPred_mem_eq_univ_iff]
  refine ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩
  rintro h _ ⟨φ, h1, rfl⟩
  exact h _ h1

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case inr
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ ∃ U, IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]

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

Goal state before:
pp: case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ liouville (m * n) = liouville m * liouville n

pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
· simp [hn]

Goal state after:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ liouville (m * n) = liouville m * liouville n