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

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ {x | ((∑ i, ‖x i‖ ^ p) ^ (1 / p)) ^ p < r ^ p} = {a | ∑ i, ‖a i‖ ^ p < r ^ p}

Tactic:
← rpow_mul (h₁ _),

Goal state after:
case e'_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p * p) < r ^ p} = {a | ∑ i, ‖a i‖ ^ p < r ^ p}
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
⊢ ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ range ⇑φ

Tactic:
intros

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
a✝² : ↑I
a✝¹ : a✝² ∈ Ioo 0 1
b✝ : ↑I
a✝ : b✝ ∈ Ioo 0 1
⊢ φ (a✝², b✝) ∈ range ⇑φ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
⊢ μ = ν

Tactic:
let e : (Z × T) ≃ᵐ ((Unit → Z) × (Unit → T)) :=
    .symm <| .prodCongr (.funUnique ..) (.funUnique ..)
  rw [← e.map_measurableEquiv_injective.eq_iff]
  refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map_equiv, integral_map_equiv]
  simpa [e] using! h (f ()) (g ())

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
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
⊢ (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤ μ.withDensity f - μ.withDensity g

Tactic:
← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
⊢ (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
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)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ i, ⋃ (_ : i ≤ n), U i)
this : ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ liminf (fun i ↦ ↑((μ (sub i)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop
⊢ ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ liminf (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop

Tactic:
← ofNNReal_liminf

Goal state after:
𝓧 : 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)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ i, ⋃ (_ : i ≤ n), U i)
this : ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ ↑(liminf (fun i ↦ (μ (sub i)) (⋃ i, ⋃ (_ : i ≤ n), U i)) atTop)
⊢ ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ liminf (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop

𝓧 : 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)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ i, ⋃ (_ : i ≤ n), U i)
this : ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ liminf (fun i ↦ ↑((μ (sub i)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun i ↦ (μ (sub i)) (⋃ i, ⋃ (_ : i ≤ n), U i)
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 - ε
⊢ Tendsto (fun n ↦ μlim (accumulate U n)) atTop (𝓝 (μlim (⋃ i, U i)))

Tactic:
ProbabilityMeasure.tendsto_measure_iUnion_accumulate

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

Goal state before:
pp: case inl
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hempty : IsEmpty 𝓧
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ε

Tactic:
← univ_eq_empty_iff

Goal state after:
case inl
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hempty : univ = ∅
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case refine_2.refine_2.refine_1
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → ↑u
sf : Fin nf → ↑𝒜₀
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → ↑u
sg : Fin ng → ↑𝒜₀
bg_eq : bg = key ng dg sg
d : Fin (nf + ng) → ↑u := fun i ↦ if h : ↑i < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : Fin (nf + ng) → ↑𝒜₀ := fun i ↦ if h : ↑i < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
⊢ bf + bg = key (nf + ng) d s

Tactic:
simp [key, d, s, Fin.sum_univ_add, bf_eq, bg_eq]

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 : 𝕜
⊢ (c • μ).variation = ‖c‖₊ • μ.variation

Tactic:
by
  apply le_antisymm variation_smul_le ?_
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  calc ‖c‖₊ • μ.variation
  _ = ‖c‖₊ • (c⁻¹ • (c • μ)).variation := by simp [smul_smul, inv_mul_cancel₀ hc]
  _ ≤ ‖c‖₊ • ‖c⁻¹‖₊ • (c • μ).variation := by
    gcongr
    exact variation_smul_le
  _ = (c • μ).variation := by
    simp [smul_smul, mul_inv_cancel₀ (nnnorm_ne_zero_iff.mpr hc)]

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

Goal state before:
pp: case pos
X : Type u_1
mX : MeasurableSpace X
μ : VectorMeasure X ℝ≥0∞
s : Set X
h : MeasurableSet s
⊢ preVariationFun (⇑μ) s = μ s

Tactic:
rw [preVariationFun_apply]

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
μ : VectorMeasure X ℝ≥0∞
s : Set X
h : MeasurableSet s
⊢ ⨆ P, ∑ p ∈ P.parts, μ ↑p = μ s

case pos.h
X : Type u_1
mX : MeasurableSpace X
μ : VectorMeasure X ℝ≥0∞
s : Set X
h : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case e'_5
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a}))
this✝ : Tendsto u atTop (𝓝[<] a)
this : (𝓝[<] a).NeBot
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a

Tactic:
exact (leftLim_rightLim (hf.tendsto_leftLim _)).symm

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 : X) in t, f x ∂[B; μ] ≠ 0
ht : MeasurableSet t
⊢ ∃ᵐ (x : X) ∂μ.variation.restrict t, f x ≠ 0

Tactic:
← variation_restrict ht

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
hU : ∫ᵛ (x : X) in t, f x ∂[B; μ] ≠ 0
ht : MeasurableSet t
⊢ ∃ᵐ (x : X) ∂(μ.restrict t).variation, f x ≠ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
ℓ : StrongDual ℝ E
ℓ_norm : ‖ℓ‖ ≤ 1
hℓ : ℓ (μ s) = ‖μ s‖
h'ℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ ‖μ s‖ₑ = ‖(μ.mapRange ↑ℓ ⋯) s‖ₑ

Tactic:
by simp [← ofReal_norm, hℓ]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
⊢ a +ᵥ b +ᵥ ↑(closure t) = (a + b) +ᵥ ↑(closure t)

Tactic:
rw [vadd_vadd]

Goal state after:
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)
  ext x
  constructor
  · intro ⟨y, hy⟩
    exact ⟨Sum.elim x y, hy, rfl⟩
  · rintro ⟨y, hy, rfl⟩
    refine ⟨y ∘ Sum.inr, ?_⟩
    simpa [LinearMap.funLeft]

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

Goal state before:
pp: case pos
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
s : Set X
hf : μ.Integrable f
hs : MeasurableSet s
⊢ (μ.withDensity f B).restrict s = (μ.restrict s).withDensity f B

Tactic:
· ext t ht
    simp only [hs, ht, restrict_apply]
    rw [withDensity_apply hf, withDensity_apply hf.restrict, restrict_restrict _ ht hs]

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : x ∈ f a
y : M
hxy : x + y ∈ f a
⊢ y ∈ f a

Tactic:
hf _ ha.1

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : x + y ∈ f a
⊢ y ∈ f a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
⊢ a + u ∈ s

Tactic:
hf _ ha.1

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : a + u ∈ s
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
⊢ a + u ∈ 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:
intros

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 ⟹ f2).toPrenex.Realize v xs✝ ↔ (f1 ⟹ f2).Realize v xs✝
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
h : ∀ {xs : Fin (n✝ + 1) → M}, f✝.toPrenex.Realize v xs ↔ f✝.Realize v xs
⊢ ∀ {xs : Fin n✝ → M}, (∀' f✝).toPrenex.Realize v xs ↔ (∀' f✝).Realize v xs

Tactic:
intros

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
h : ∀ {xs : Fin (n✝ + 1) → M}, f✝.toPrenex.Realize v xs ↔ f✝.Realize v xs
xs✝ : Fin n✝ → M
⊢ (∀' f✝).toPrenex.Realize v xs✝ ↔ (∀' f✝).Realize v xs✝
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
induction hA with

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
⊢ Function.Injective g

Tactic:
intro S

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S : { S // S.FG }
⊢ ∀ ⦃a₂ : { S // S.FG }⦄, g S = g a₂ → S = a₂
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isAtomic
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ✝ : L.BoundedFormula α n
hA : φ✝.IsAtomic
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ✝.Realize v xs

Tactic:
induction hA with

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 ι
α : Type u_1
inst✝ : Finite α
x y : α → Σˣ f
xy : x ≈ y
i : ι
hi : i ∈ upperBounds (range fun a ↦ (x a).fst) ∩ upperBounds (range fun a ↦ (y a).fst)
⊢ ∃ i,
    ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy

Tactic:
← Function.comp_apply (f := Sigma.fst)

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 ι
α : Type u_1
inst✝ : Finite α
x y : α → Σˣ f
xy : x ≈ y
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Sigma.fst ∘ x) a) ∩ upperBounds (range fun a ↦ (Sigma.fst ∘ y) a)
⊢ ∃ i,
    ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ f ≤ g

Tactic:
le_def

Goal state after:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ ∃ (h : f.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g

Tactic:
le_def

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding