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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
Measurebound : ∀ (n : ℕ), ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ 1 - ε
accumulation : Tendsto (fun a ↦ ↑(μlim (⋃ i, ⋃ (_ : i ≤ a), U i))) atTop (𝓝 ↑1)
⊢ 1 - ε / 2 < 1

Tactic:
by simp only [sub_lt_self_iff, Nat.ofNat_pos, div_pos_iff_of_pos_right]; positivity

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
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
c : 𝕜
hc : c ≠ 0
⊢ ‖c‖₊ • μ.variation = ‖c‖₊ • (c⁻¹ • c • μ).variation

Tactic:
simp [smul_smul, inv_mul_cancel₀ hc]

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

Goal state before:
pp: case hd
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‖ₑ
⊢ (↑({x ∈ P | 0 ≤ μ x})).PairwiseDisjoint fun x ↦ x

Tactic:
apply P_disj.subset (by grind)

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

Goal state before:
pp: case hd
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)‖ₑ
⊢ (↑({x ∈ P | μ x < 0})).PairwiseDisjoint fun x ↦ x

Tactic:
apply P_disj.subset (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)‖ₑ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ

Tactic:
have J : (∑ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), ‖μ p‖ₑ) =
      ‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ := by
    simp only [not_le, enorm_eq_nnnorm, ← ENNReal.ofNNReal_finsetSum,
      ENNReal.coe_inj, ← NNReal.coe_inj, NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs]
    have A : ∑ x ∈ P with μ x < 0, |μ x| = - μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := calc
      ∑ x ∈ P with μ x < 0, |μ x|
      _ = ∑ x ∈ P with μ x < 0, -μ x := by
        refine Finset.sum_congr rfl (fun p hp ↦ ?_)
        simp only [Finset.mem_filter] at hp
        simp [hp.2.le]
      _ = -μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := by
        rw [of_biUnion_finset]
        · simp
        · apply P_disj.subset (by grind)
        · grind
    rw [A, abs_of_nonpos]
    rw [← neg_nonneg, ← A]
    exact Finset.sum_nonneg (fun p hp ↦ by positivity)

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)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
X : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : VectorMeasure X F
f : X → E
s t : Set X
hs : MeasurableSet s
hts : t ⊆ s
h : μ.IntegrableOn f s
ht : ¬MeasurableSet t
⊢ μ.IntegrableOn f t

Tactic:
simp [VectorMeasure.IntegrableOn, restrict_not_measurable _ ht]

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

Goal state before:
pp: case insert.hst
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ Disjoint (s a✝) (⋃ x ∈ s✝, s x)

Tactic:
simp only [disjoint_iUnion_right]
      exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1

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
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:
calc
    ∫ᵛ x, indicator s f x ∂[B; μ]
    _ = ∫ᵛ x in s, indicator s f x ∂[B; μ] + ∫ᵛ x in sᶜ, indicator s f x ∂[B; μ] :=
      (setIntegral_add_compl hs (hfi.integrable_indicator hs)).symm
    _ = ∫ᵛ x in s, f x ∂[B; μ] + ∫ᵛ x in sᶜ, 0 ∂[B; μ] := by
      apply congr_arg₂ (· + ·) (integral_congr_ae ?_) (integral_congr_ae ?_)
      · rw [variation_restrict hs]
        exact indicator_ae_eq_restrict hs
      · rw [variation_restrict hs.compl]
        exact indicator_ae_eq_restrict_compl hs
    _ = ∫ᵛ x in s, f x ∂[B; μ] := by simp

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

Goal state before:
pp: 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)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
rw [← hx h''x]

Goal state after:
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)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ f x = 0 x
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 : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ s ∩ s ≤ᵐ[μ] s ∩ ⋃₀ D

Tactic:
exact ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs)

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

Goal state before:
pp: 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
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f : X → H
C : H →L[ℝ] E
hf : Integrable f μ.variation
⊢ ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]

Tactic:
by
  by_cases hG : CompleteSpace G; swap
  · simp [integral_of_not_completeSpace hG]
  apply hf.induction (P := fun f ↦ ∫ᵛ y, C (f y) ∂[B; μ] = ∫ᵛ y, f y ∂[B ∘L C; μ])
  · intro c s hs hc
    have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩
    rw [integral_indicator_const _ hs]
    have : (fun y ↦ C (s.indicator (fun x ↦ c) y)) = s.indicator (fun x ↦ C c) := by
      ext; simp only [indicator]; grind
    simp_rw [this]
    rw [integral_indicator_const _ hs]
    rfl
  · intro f g _ f_int g_int hf hg
    simp only [Pi.add_apply, _root_.map_add]
    rw [integral_fun_add (C.integrable_comp f_int) (C.integrable_comp g_int), hf, hg,
      integral_fun_add f_int g_int]
  · apply isClosed_eq
    · have I (f : Lp H 1 μ.variation) : ∫ᵛ x, C (f x) ∂[B; μ] = ∫ᵛ x, (C.compLp f) x ∂[B; μ] :=
        (integral_congr_ae (coeFn_compLp _ _)).symm
      simp_rw [I]
      exact continuous_integral.comp (C.compLpL 1 μ.variation).continuous
    · exact continuous_integral
  · intro f g hfg _ hf
    have : ∀ᵐ x ∂μ.variation, C (f x) = C (g x) := by
      filter_upwards [hfg] with x hx using by simp [hx]
    rw [← integral_congr_ae hfg, ← integral_congr_ae this, hf]

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

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

Tactic:
rw [← biUnion_of_singleton s]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ IsSemilinearSet (⋃ x ∈ s, {x})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
ι : Type u_3
κ : Type u_4
inst✝ : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
⊢ IsSemilinearSet {x | ∃ y, Sum.elim x y ∈ s}

Tactic:
convert! hs.image (LinearMap.funLeft ℕ M Sum.inl)

Goal state after:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst✝ : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
⊢ {x | ∃ y, Sum.elim x y ∈ s} = ⇑(LinearMap.funLeft ℕ M Sum.inl) '' s
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
⊢ ∃ g, eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ ∧ MemLp (⇑g) 1 μ.variation

Tactic:
refine ⟨g, ?_, gmem⟩

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
⊢ eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
G : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
s : Set X
hs : MeasurableSet s
⊢ ∫ᵛ (x : X) in s, f x ∂<•μ.toSignedMeasure = ∫ (x : X) in s, f x ∂μ

Tactic:
by
  rw [← integral_toSignedMeasure, restrict_toSignedMeasure hs]

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

Goal state before:
pp: case hbc
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).toReal ≤ (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal

Tactic:
apply ENNReal.toReal_mono

Goal state after:
case hbc.hb
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 C ∂μ.variation ≠ ∞

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
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
obtain ⟨f, h'⟩ :=
      (Scount.union (Set.countable_singleton h.some)).exists_eq_range
        (singleton_nonempty h.some).inr

Goal state after:
case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m n : ℕ
h : m ≤ n
⊢ ⇑(natLERec f' m n h) = fun a ↦ Nat.leRecOn h (fun k ↦ ⇑(f' k)) a

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  ext x
  induction k with
  | zero => simp [natLERec, Nat.leRecOn_self]
  | succ k ih =>
    rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]

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
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype.toFun ((inclusion ⋯) (f.toEquiv x)) = g.cod.subtype.toFun (g.toEquiv ((inclusion ⋯) x))

Tactic:
rwa [toEquiv_inclusion_apply]

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

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

Tactic:
rw [hs.basis_apply]

Goal state after:
case hb
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ 0 ≤ toRatVec ↑i
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
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
← (subtype_toEquiv_inclusion hfg)

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
f : L.FGEquiv N M
m : M
⊢ ∃ g, m ∈ (↑g).cod ∧ f ≤ g

Tactic:
obtain ⟨g, h1, h2⟩ := h f.symm m

Goal state after:
case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
f : L.FGEquiv N M
m : M
g : L.FGEquiv M N
h1 : m ∈ (↑g).dom
h2 : f.symm ≤ g
⊢ ∃ g, m ∈ (↑g).cod ∧ f ≤ g
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 : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g

Tactic:
obtain ⟨g, h1, h2⟩ := h f.symm m

Goal state after:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
g : L.FGEquiv N M
h1 : m ∈ (↑g).cod
h2 : f.symm ≤ g
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a b : M
ab :
  Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 0) <
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 1)
⊢ ∃ a_1,
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) ∧
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 1)

Tactic:
exact exists_between ab

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑(Set.inclusion ⋯ ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) = ↑(Set.inclusion ⋯ (QM.equivRange (NQ n)))

Tactic:
simp only [Embedding.equivRange_apply, hgn]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n)) = g (PM (NP n))
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
exact admissible_E8

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hs : [p, q, r].SortedLE
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]

Tactic:
exact admissible_of_one_lt_sumInv_aux' hpq hqr H

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

Goal state before:
pp: n : ℕ
⊢ Λ n ≠ 0 ↔ IsPrimePow n

Tactic:
by
  rcases eq_or_ne n 1 with (rfl | hn); · simp [not_isPrimePow_one]
  exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff

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

Goal state before:
pp: n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Tactic:
intro m mn hn

Goal state after:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc (n - 1)) ((d⁄dX R) f) = Polynomial.derivative ((trunc n) f)

Tactic:
cases n <;> simp [trunc_derivative]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case succ
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
h : n.succ • (coeff (n + 1)) f = n.succ • (coeff (n + 1)) (exp A)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)

Tactic:
exact (smul_right_inj (Nat.succ_ne_zero n)).mp h

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i =
    ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) + ((d + 2).choose (d + 1) * (d + 1)) • X ^ (d + 1 - 1)

Tactic:
by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0

Tactic:
by
    rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
    · apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
    · simpa +decide [Nat.factorial] using h 1

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Tactic:
have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]

Goal state after:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (∏ p ∈ n.primesLE, p)

Tactic:
refine Finset.squarefree_prod_of_pairwise_isCoprime (fun _ hp _ hq hpq ↦ ?_)
    fun _ hp ↦ (prime_of_mem_primesLE hp).squarefree

Goal state after:
n x✝¹ : ℕ
hp : x✝¹ ∈ ↑n.primesLE
x✝ : ℕ
hq : x✝ ∈ ↑n.primesLE
hpq : x✝¹ ≠ x✝
⊢ Function.onFun IsRelPrime (fun p ↦ p) x✝¹ x✝