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 : NormalSpace E
this✝ : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this : Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑ρ) (↑f) (𝓝 (∫ (x : E), g x ∂↑μ))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
⊢ ∫ (x : E), (K n)ᶜ.indicator 1 x ∂↑ρ = ↑(ρ (K n)ᶜ)

Tactic:
simp [integral_indicator (hK n).measurableSet.compl]

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)

Tactic:
· let t := {x | f x ≤ g x}
    have ht : MeasurableSet t := measurableSet_le hf hg
    rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
      ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]
    have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
      simp only [restrict_eq_zero]
      rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
      refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
      simpa [tsub_eq_zero_iff_le]
    rw [h_zero, zero_add]
    suffices (μ.withDensity (f - g)).restrict tᶜ ≤
      (μ.withDensity f - μ.withDensity g).restrict tᶜ from this.trans (Measure.le_add_left le_rfl)
    rw [restrict_sub_eq_restrict_sub_restrict ht.compl]
    simp_rw [restrict_withDensity ht.compl]
    have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
      rw [← restrict_withDensity ht.compl]
      infer_instance
    rw [withDensity_sub_of_le hg]
    refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_
    simp only [Set.mem_compl_iff, Set.mem_ofPred_eq, not_le, t] at hx
    exact hx.le

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
h's : (↑t).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, μ.IntegrableOn f (s i)
⊢ ∫ᵛ (x : X) in ⋃ i ∈ t, s i, f x ∂[B; μ] = ∑ i ∈ t, ∫ᵛ (x : X) in s i, f x ∂[B; μ]

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ hat IH =>
    simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢
    rw [setIntegral_union]
    · rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
    · simp only [disjoint_iUnion_right]
      exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1
    · exact hs.1
    · exact Finset.measurableSet_biUnion _ hs.2
    · exact hf.1
    · apply IntegrableOn.biUnion_finset hs.2 hf.2

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
hU : ∀ x ∈ t, f x = 0
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0

Tactic:
exact setIntegral_eq_zero_of_forall_eq_zero hU

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

Goal state before:

Tactic:
μ ((s'' ∪ t') ∆ (s ∪ t))
      _ ≤ μ (s'' ∆ s ∪ t' ∆ t) := measure_mono (Set.union_symmDiff_union_subset ..)
      _ ≤ μ (s'' ∆ s) + μ (t' ∆ t) := measure_union_le _ _
      _ < 3 * δ + δ := by gcongr
      _ = 4 * δ := by ring

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

Goal state before:
pp: case h₁
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s

Tactic:
apply le_biSup _ hℓ

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

Goal state before:
pp: case h₂
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation t ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
apply le_biSup _ hℓ

Goal state after:
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 t : Set X
hst : s ⊆ t
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation t ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
apply le_biSup _ hℓ

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

Goal state before:
pp: case inl
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‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation t = ∞
this : 1 + ‖μ s‖ₑ ≤ ‖μ (s \ t)‖ₑ + ‖μ s‖ₑ
⊢ 1 ≤ ‖μ (s \ t)‖ₑ

Tactic:
rwa [ENNReal.add_le_add_iff_right (by simp)] at this

Goal state after:
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
⊢ μ.semivariation univ < ∞

Tactic:
apply Ne.lt_top (fun h ↦ ?_)
  have A (s : Set X) (hs : MeasurableSet s) (h's : μ.semivariation s = ∞) :
      ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ :=
    exists_one_le_enorm_apply_of_semivariation_eq_top hs h's
  choose! t t_meas t_subs t_var ht using A
  let s n := t^[n] univ
  have hs n : MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞ := by
    induction n with
    | zero => simp [s, h]
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, s]
      exact ⟨t_meas _ ih.1 ih.2, t_var _ ih.1 ih.2⟩
  let u n := s n \ s (n + 1)
  have hu n : 1 ≤ ‖μ (u n)‖ₑ := by
    simp only [Function.iterate_succ', Function.comp_apply, u, s]
    exact ht _ (hs n).1 (hs n).2
  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
  have u_disj : Pairwise (Disjoint on u) := by
    apply (pairwise_disjoint_on _).2 (fun m n hmn ↦ ?_)
    have : Disjoint (u m) (s (m + 1)) := by simp [u, disjoint_sdiff_left]
    apply this.mono_right
    simp only [sdiff_le_iff, sup_eq_union, u]
    exact Subset.trans (s_anti (by grind)) subset_union_right
  have : HasSum (fun i => μ (u i)) (μ (⋃ i, u i)) :=
    hasSum_of_disjoint_iUnion (fun n ↦ (hs n).1.diff (hs (n + 1)).1) u_disj
  have : Tendsto (fun x ↦ ‖μ (u x)‖ₑ) atTop (𝓝 0) :=
    tendsto_zero_iff_enorm_tendsto_zero.1 this.summable.tendsto_atTop_zero
  obtain ⟨n, hn⟩ : ∃ n, ‖μ (u n)‖ₑ < 1 := ((tendsto_order.1 this).2 _ zero_lt_one).exists
  order [hu n]

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
⊢ ‖B‖ₑ * ∫⁻ (x : X) in ⋃ i, s i, ‖f x‖ₑ ∂μ.variation < ∞

Tactic:
simp only [VectorMeasure.IntegrableOn, VectorMeasure.Integrable,
        variation_restrict (MeasurableSet.iUnion hm)] at hfi
      exact ENNReal.mul_lt_top (by simp) hfi.2

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

Tactic:
← add_tsub_cancel_of_le hx',

Goal state after:
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 : k + (x - k) ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s
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
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
hxz : x + z ∈ s
hxzi : (x + z) i = a
⊢ x + y + z ∈ {x | x ∈ s ∧ x i = a}

Tactic:
refine ⟨hs _ hx _ _ hxy hxz, ?_⟩

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
hxz : x + z ∈ s
hxzi : (x + z) i = a
⊢ (x + y + z) i = a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
⊢ A.Definable presburger {x | x 0 ∈ {x | ∃ x_1, x_1 * x_1 = x}}

Tactic:
convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]

Goal state after:
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
⊢ {x | x 0 ∈ {x | ∃ x_1, x_1 * x_1 = x}} = (fun g ↦ g ∘ ![0]) '' (fun g ↦ g ∘ ![0, 1, 1]) ⁻¹' {v | v 0 = v 1 * v 2}
Module: Mathlib.ModelTheory.Equivalence

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

Tactic:
simp only [realize_iff, realize_sup, realize_not, realize_top, or_not]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
by
    have := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)

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

Goal state before:
pp: ι : Type u_3
x y : ι → ℕ
⊢ ∀ (a : ι), toRatVec x a ≤ toRatVec y a ↔ x a ≤ y a

Tactic:
simp [toRatVec]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' hs.basisSet) = ⊤

Tactic:
rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ ⊤ ≤ span ℚ (⇑toRatVec '' (hs.periods ∪ range ⇑(Pi.basisFun ℕ ι)))
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case h
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 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
i : (_ : E) × Set X
hi : i ∈ g.range.sigma P
⊢ ‖∫ᵛ (x : X) in i.snd, g x - f x ∂[B; μ.restrict s] + ∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤
    ‖∫ᵛ (x : X) in i.snd, g x - f x ∂[B; μ.restrict s]‖ₑ + ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ

Tactic:
apply enorm_add_le

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

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : x + y' = u + y
⊢ hs.fract x ≠ hs.base

Tactic:
apply congr_arg hs.fract at heq

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract (x + y') = hs.fract (u + y)
⊢ hs.fract x ≠ hs.base
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
n : ℕ
⊢ ∀ (a b : Language.graph.Relations n), a = b

Tactic:
rintro ⟨⟩ ⟨⟩

Goal state after:
V : Type u
⊢ graphRel.adj = graphRel.adj
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
rcases lt_or_gt_of_ne this with hl | hr

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hl : p1 < a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

case h.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : a < p1
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : 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.fract x = hs.base

Tactic:
apply congr_arg hs.fract at heq

Goal state after:
case mpr.refine_1
ι : 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 : hs.fract (x + ↑i + y + z') = hs.fract (hs.base + z)
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
⊢ ∀ (a b : Language.order.Relations n), a = b

Tactic:
rintro ⟨⟩ ⟨⟩

Goal state after:
L : Language
α : Type w
M : Type w'
⊢ orderRel.le = orderRel.le
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : 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
⊢ hs.fract x = hs.base

Tactic:
apply congr_arg hs.fract at heq

Goal state after:
case mpr.refine_1
ι : 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 : hs.fract (x + z') = hs.fract (hs.base + ↑i + y + z)
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Tactic:
nonempty_iff_univ_nonempty,

Goal state after:
L : Language
T : L.Theory
α : Type w
⊢ Set.univ.Nonempty ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)

Tactic:
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]

Goal state after:
case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

Tactic:
exact admissible_D' r

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

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf 5 ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
show (5 : ZMod (2 ^ n)) = five by rfl,

Goal state after:
case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf ↑five ∣ exponent (ZMod (2 ^ n))ˣ
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

Tactic:
rw [coeff_pderiv, coeff_trunc, if_neg ((add_lt_add_iff_right _).not.mpr h), zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
⊢ (coeff n) ((d⁄dX R) (subst g f)) = (coeff n) (subst g ((d⁄dX R) f) * (d⁄dX R) g)

Tactic:
rw [coeff_derivative, this, ← coeff_derivative, derivative_subst_coe _ hg, coeff_mul, coeff_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
⊢ ∑ p ∈ Finset.antidiagonal n, (coeff p.1) (subst g ((d⁄dX R) ↑((trunc (m + 1)) f))) * (coeff p.2) ((d⁄dX R) g) =
    ∑ p ∈ Finset.antidiagonal n, (coeff p.1) (subst g ((d⁄dX R) f)) * (coeff p.2) ((d⁄dX R) g)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
rw [← Nat.cast_succ]

Goal state after:
n p : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑p.succ
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h₁
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := ⋯
f : ℕ → ℕ := ⋯
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
    · exact pow_factorization_choose_le (mul_pos two_pos n_pos)
    have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
    rw [Finset.prod_const]
    refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)
    obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
    exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < |b| • ε

Tactic:
Algebra.smul_def

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < (algebraMap ℤ ℝ) |b| * ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
x : ℝ
hy : 2 ≤ x
this : 0 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}

Tactic:
simpa using ⟨(le_floor_iff this).2 hy, prime_two⟩

Goal state after: