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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ✝ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ✝)
n : ℕ
h : Monotone K
this✝¹ : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
⊢ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass ≤ u n

Tactic:
have : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n) := by
      rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]
      · exact (disjoint_disjointed K).set_pairwise _
      · exact MeasurableSet.disjointed (fun i ↦ (hK i).measurableSet)

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ✝ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ✝)
n : ℕ
h : Monotone K
this✝² : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝¹ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this✝ :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass ≤ u n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mpr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
⊢ μ univ = 1 → ∃ s, μ s = 1

Tactic:
· intro h
    exact ⟨univ, h⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
⊢ ∃ x₀, ⋂ n, B n = {x₀}

Tactic:
simp_rw [eq_singleton_iff_unique_mem]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
⊢ ∃ x₀ ∈ ⋂ n, B n, ∀ x ∈ ⋂ n, B n, x = x₀
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case ac
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 := ⋯
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)
⊢ μ (s \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)

Tactic:
measure_sdiff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),

Goal state after:
case ac
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)
⊢ μ s - μ (s ∩ T N) < ENNReal.ofReal (ε / 2)
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: 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
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
rcases exists_countable_dense E with ⟨u, countable_u, dense_u⟩

Goal state after:
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
⊢ SeparableSpace ↥(Lp E p μ)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case succ.a
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ MeasurableSet (⋃ x ∈ Finset.range n, f x)

pp: case succ.a
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ Disjoint (f n) (⋃ x ∈ Finset.range n, f x)

Tactic:
· exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)

Goal state after:
case succ.a
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ Disjoint (f n) (⋃ x ∈ Finset.range n, f x)
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : ¬μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
· rw [integral_undef hfi, integral_undef]
    rw [integrable_indicator_iff hs]
    simpa [transpose_restrict, variation_restrict hs] using hfi

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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case h_ind
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedAddCommGroup H
μ : VectorMeasure X F
f : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f μ.variation
⊢ ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      μ.variation s < ∞ →
        C ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B; μ] =
          ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
intro c s hs hc
    have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩
    simp [integral_indicator_const _ hs]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddMonoidWithOne M
n : ℕ
⊢ Term.realize v ↑n = ↑n

Tactic:
induction n with simp [*]

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

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

Tactic:
intro hx

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

Goal state before:
pp: case mp
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 : ℕ
⊢ x ∈ s → x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x

Tactic:
intro hx

Goal state after:
case mp
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
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
⊢ IsSlice {x | x ∈ s ∧ x i = a}

Tactic:
by
  intro x ⟨hx, hxi⟩ y z ⟨hxy, hxyi⟩ ⟨hxz, hxzi⟩
  refine ⟨hs _ hx _ _ hxy hxz, ?_⟩
  simp only [Pi.add_apply] at *
  rw [hxyi, ← hxi, hxzi, hxi]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f1 f2 : L.BoundedFormula α n✝
h1 : ∀ {xs : Fin n✝ → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs
h2 : ∀ {xs : Fin n✝ → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs
xs✝ : Fin n✝ → M
⊢ f1.Realize v xs✝ → f2.toPrenex.Realize v xs✝ ↔ f1.Realize v xs✝ → f2.Realize v xs✝

Tactic:
h2

Goal state after:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f1 f2 : L.BoundedFormula α n✝
h1 : ∀ {xs : Fin n✝ → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs
h2 : ∀ {xs : Fin n✝ → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs
xs✝ : Fin n✝ → M
⊢ f1.Realize v xs✝ → f2.Realize v xs✝ ↔ f1.Realize v xs✝ → f2.Realize v xs✝
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ t
h' : x ∈ ↑((closure L).toFun t)
⊢ x ∈ range ⇑f

Tactic:
h2

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ t
h' : x ∈ ↑(Substructure.map f.toHom s)
⊢ x ∈ range ⇑f
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : 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}
y : ι → ℕ
⊢ y ∈ s ↔ y ∈ {y | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y | y ∈ s ∧ y i = j}

Tactic:
simp only [Finset.mem_range, mem_union, mem_ofPred_eq, mem_iUnion, Pi.le_def]

Goal state after:
ι : 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}
y : ι → ℕ
⊢ y ∈ s ↔ (y ∈ s ∧ ∀ (i : ι), x i ≤ y i) ∨ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 < x i), y ∈ s ∧ y i = i_1
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
h : (fun f ↦ f.toPartialEquiv) a₁✝ = (fun f ↦ f.toPartialEquiv) a₂✝
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
rw [PartialEquiv.ext_iff] at h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h :
  ∃ (h_dom : ((fun f ↦ f.toPartialEquiv) a₁✝).dom = ((fun f ↦ f.toPartialEquiv) a₂✝).dom),
    ∀ (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, ⋯⟩)
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ Countable (L.FGEquiv M M)

Tactic:
by
  let g : L.FGEquiv M M →
      Σ U : { S : L.Substructure M // S.FG }, U.val →[L] M :=
    fun f ↦ ⟨⟨f.val.dom, f.prop⟩, (subtype _).toHom.comp f.val.toEquiv.toHom⟩
  have g_inj : Function.Injective g := by
    intro f f' h
    ext
    let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f
    cases congr_arg (·.1) h
    apply PartialEquiv.ext (by rfl)
    simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h
    exact fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩
  have : ∀ U : { S : L.Substructure M // S.FG }, Structure.FG L U.val :=
    fun U ↦ (U.val.fg_iff_structure_fg.1 U.prop)
  exact Function.Embedding.countable ⟨g, g_inj⟩

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

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ hs.fract x ≠ hs.base →
    ∃ i ∈ hs.fundamentalDomain \ {hs.base}, ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = i + y

Tactic:
intro hx

Goal state after:
case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x ≠ hs.base
⊢ ∃ i ∈ hs.fundamentalDomain \ {hs.base}, ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = i + y
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case h
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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) := ⋯
m : M
hm : m ∈ ⨆ i, S i
a : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
h✝ : (liftInclusion S).toHom a = m
⊢ F a = ⟨m, hm⟩

Tactic:
simpa only [F, Embedding.codRestrict_apply', Subtype.mk.injEq]

Goal state after:
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
        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:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p q : T.CompleteType α
h : (fun p ↦ ↑p) p = (fun p ↦ ↑p) q
⊢ p = q

Tactic:
by
    cases p
    cases q
    congr

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

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ↑F ≤
    ⨅ s ∈ {s | { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ s ∧ s ∈ range T.typesWith},
      Filter.principal s

Tactic:
apply le_iInf₂

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ∀ i ∈ {s | { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ s ∧ s ∈ range T.typesWith},
    ↑F ≤ Filter.principal i
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:
change r ∈ ({3, 4, 5} : Multiset ℕ+)

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: case succ
n : ℕ
hn : n + 1 ≠ 0
⊢ λ (n + 1) = exponent (ZMod (n + 1))ˣ

Tactic:
change Nat.find _ = _

Goal state after:
case succ
n : ℕ
hn : n + 1 ≠ 0
⊢ Nat.find ⋯ = exponent (ZMod (n + 1))ˣ
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.188 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.188 n, c k
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k

Tactic:
h (h_inc₁ h')

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∑ k ∈ Icc 0 n, c k
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 n, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, Λ i = Real.log ↑(p ^ k)

Tactic:
sum_divisors_prime_pow hp,

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ x ∈ range (k + 1), Λ (p ^ x) = Real.log ↑(p ^ k)
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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
⊢ a < ↑⌊b⌋₊

Tactic:
← Nat.floor_lt ha

Goal state after:
𝕜 : 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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
⊢ ⌊a⌋₊ < ⌊b⌋₊
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
⊢ ¬IsCyclic (ZMod (m * n))ˣ

Tactic:
have _ : NeZero m := ⟨Nat.ne_of_odd_add hm⟩

Goal state after:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝ : NeZero m
⊢ ¬IsCyclic (ZMod (m * n))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
h2

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