mathlib-initiative/mathlib-tactics huggingface dataset:
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
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}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal) ≤ ε / 3 * 1

Tactic:
div_mul_eq_div_mul_one_div,

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
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}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ε / 3 * (1 / (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal) ≤ ε / 3 * 1
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
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
⊢ s.indicator f =ᵐ[(μ.restrict sᶜ).variation] fun x ↦ 0

Tactic:
rw [variation_restrict hs.compl]

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
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
⊢ s.indicator f =ᵐ[μ.variation.restrict sᶜ] fun x ↦ 0
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
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
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0

Tactic:
simp [setIntegral_eq_zero_of_not_measurableSet ht]

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 : Set X
hs : MeasurableSet s
ℓ : StrongDual ℝ E
ℓ_norm : ‖ℓ‖ ≤ 1
hℓ : ℓ (μ s) = ‖μ s‖
h'ℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ μ.semivariation s

Tactic:
by apply le_biSup _ h'ℓ

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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := ⋯
Mle : M ≤ hα
μ' : Measure α := ⋯
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
⊢ {x |
      (fun x ↦ μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x = (fun x ↦ ∑' (d : ℕ), μ[(f d).indicator 1 | M] x) x)
        x} ∈
    ae μ'

Tactic:
apply ae_eq_trim_of_measurable _ (by fun_prop) (by fun_prop)

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := ⋯
Mle : M ≤ hα
μ' : Measure α := ⋯
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
⊢ μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] =ᵐ[μ] fun x ↦ ∑' (d : ℕ), μ[(f d).indicator 1 | M] x
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_add
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
hG : CompleteSpace G
f g : X → H
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
hg : ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
⊢ ∫ᵛ (y : X), C (f y) + C (g y) ∂[B; μ] = ∫ᵛ (y : X), f y + g y ∂[B ∘SL C; μ]

Tactic:
integral_fun_add (C.integrable_comp f_int) (C.integrable_comp g_int),

Goal state after:
case pos.h_add
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
hG : CompleteSpace G
f g : X → H
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
hg : ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
⊢ ∫ᵛ (x : X), C (f x) ∂[B; μ] + ∫ᵛ (x : X), C (g x) ∂[B; μ] = ∫ᵛ (y : X), f y + g y ∂[B ∘SL C; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂m'.variation ≠ ∞

pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∑' (i : ℕ), ∫ᵛ (a : α), μ[(f i).indicator 1 | M] a ∂•m')

Tactic:
· apply ne_of_lt
        grw [m'_le, hμ']
        have A i : Measurable[M] (fun x ↦ ‖μ[(f i).indicator (1 : α → ℝ) | M] x‖ₑ) := by fun_prop
        simp_rw [lintegral_trim Mle (A _)]
        exact I

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∑' (i : ℕ), ∫ᵛ (a : α), μ[(f i).indicator 1 | M] a ∂•m')
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case a
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
⊢ (μ.transpose B).variation ≤ C • μ.variation

Tactic:
apply (variation_transpose_le _ _).trans
    gcongr
    apply opNNNorm_le_bound _ _ (fun x ↦ opNNNorm_le_bound _ _ (fun y ↦ by simp [hB]))

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

Goal state before:
pp: case inr.mpr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ a_1, a + a_1 * b = x + b) → ∃ a_2, a + a_2 * b = x

Tactic:
rintro ⟨y, heq⟩
          cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
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‖ₑ * ρ ≤ ↑δ
i : E
hi : i ≠ 0
this :
  ∃ P,
    (∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}) ∧
      (↑P).PairwiseDisjoint id ∧
        (∀ t ∈ P, MeasurableSet t) ∧
          ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤ ∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}) ∧
      (↑P).PairwiseDisjoint id ∧
        (∀ t ∈ P, MeasurableSet t) ∧
          ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
            ‖i‖ₑ * (∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)

Tactic:
by
      obtain ⟨P, hP, h'P, h''P, h'''P⟩ := this
      exact ⟨P, hP, h'P, h''P, by gcongr⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ (closure L).toFun t₂ = N₂
⊢ N₁ ⊔ (closure L).toFun t₂ = N₁ ⊔ N₂

Tactic:
ht₂.2

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ (closure L).toFun t₂ = N₂
⊢ N₁ ⊔ N₂ = N₁ ⊔ N₂
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case pos
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : φ.Realize v xs
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
exact ⟨a, fun _ => ha⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ (closure L).toFun t₂ = N₂
⊢ N₁ ⊔ (closure L).toFun t₂ = N₁ ⊔ N₂

Tactic:
ht₂.2

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ (closure L).toFun t₂ = N₂
⊢ N₁ ⊔ N₂ = N₁ ⊔ N₂
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
intro a t ht

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
t : Finset ι
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet s
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 ⟹ f2).toPrenex.Realize v xs✝ ↔ (f1 ⟹ f2).Realize v xs✝

Tactic:
rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ✝¹ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
hφ : P φ✝
⊢ P (∃' φ✝)

Tactic:
| ex _ hφ =>

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.FG
⊢ S.FG

Tactic:
· have h := h.map S.subtype.toHom
    rw [← Hom.range_eq_map, range_subtype] at h
    exact h

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.CG
⊢ S.CG

Tactic:
· have h := h.map S.subtype.toHom
    rw [← Hom.range_eq_map, range_subtype] at h
    exact h

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ M ⊨ T

Tactic:
simp only [model_iff]

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: 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✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
x y : Σˣ f
i : ι
hx : x.fst ≤ i
hy : y.fst ≤ i
⊢ x ≈ y ↔ (f x.fst i hx) x.snd = (f y.fst i hy) y.snd

Tactic:
cases x
  cases y
  refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩
  obtain ⟨j, _, _, h⟩ := xy
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  have h := congr_arg (f j k jk) h
  apply (f i k ik).injective
  rw [DirectedSystem.map_map, DirectedSystem.map_map] at *
  exact h

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: 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✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ RelMap R (unify f x i hi) = RelMap R (unify f x j hj)

Tactic:
rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: 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✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
⊢ (lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range

Tactic:
simp_rw [Hom.range_eq_map]

Goal state after:
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✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
⊢ Substructure.map (lift L ι G f g Hg).toHom ⊤ = ⨆ i, Substructure.map (g i).toHom ⊤
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x ≠ hs.base
⊢ x + ∑ i, (-hs.floor x i).toNat • ↑i = hs.fract x + ∑ i, (hs.floor x i).toNat • ↑i

Tactic:
· exact hs.add_floor_neg_toNat_sum_eq x

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
fg : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨(Substructure.fg_iff_structure_fg _).1 fg, ⟨subtype _⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
⊢ (Quotient.mk' '' L.age M).Countable

Tactic:
refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
⊢ a ≤ b → f a ≤ f b

Tactic:
by
  have h := HomClass.map_rel f leSymb ![a, b]
  simp only [relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Function.comp_apply] at h
  exact h

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 ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
· rw [nhds_generateFrom]
      apply le_iInf₂
      rintro _ ⟨hφ, φ, rfl⟩
      rw [Filter.le_principal_iff]
      exact hφ

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ (coeff n✝) ((d⁄dX R) ↑f) = (coeff n✝) ↑(Polynomial.derivative f)

Tactic:
rw [coeff_derivative, coeff_coe, coeff_coe, Polynomial.coeff_derivative]

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

Goal state before:
pp: case neg.inr.inl.refl
p : ℕ
h0 : ¬2 * p ^ 0 = 0
h1 : ¬2 * p ^ 0 = 1
h4 : ¬2 * p ^ 0 = 4
hn✝ : Even (2 * p ^ 0)
hn : Odd (p ^ 0)
h2 : 0 < 1
⊢ 2 * p ^ 0 = 2

Tactic:
rw [pow_zero, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hab
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a ↑⌊b⌋₊

Tactic:
intervalIntegrable_iff_integrableOn_Icc_of_le aux6

Goal state after:
case inr.hab
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntegrableOn (fun x ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) (Set.Icc a ↑⌊b⌋₊) volume