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

Goal state before:
pp: case refine_1
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)
h : NormalSpace E ∨ Monotone K
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) (𝓝 μ)
⊢ μ.mass ≤ C

Tactic:
simp only [mass, mk_apply, μ]

Goal state after:
case refine_1
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)
h : NormalSpace E ∨ Monotone K
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) (𝓝 μ)
⊢ ((Measure.sum fun n ↦ ↑(ν n)) univ).toNNReal ≤ C
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
⊢ Tendsto μ (↑U) (𝓝 μ₀)

Tactic:
by convert! hμ'; ext; rw [this]

Goal state after:
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)
h : NormalSpace E ∨ Monotone K
⊢ IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Tactic:
have : {μ : FiniteMeasure E | μ.mass = C ∧ ∀ n, μ (K n)ᶜ ≤ u n} =
    {μ | μ.mass ≤ C ∧ ∀ n, μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C} := by ext; grind
  rw [this]
  apply IsCompact.inter_right
    (isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le C hu hK h)
  exact isClosed_eq (by fun_prop) (by fun_prop)

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

Goal state before:
pp: case refine_2.inr
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✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = ∞
⊢ ∃ t ∈ ℬ, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine False.elim <| hμs ?_
        rw [eq_top_iff, ← hs]
        exact μ.restrict_le_self _

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
x : X
v : V
⊢ IsFiniteMeasure (dirac x v).variation

Tactic:
simp only [variation_dirac, enorm_eq_nnnorm, Measure.coe_nnreal_smul]
  infer_instance

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

Goal state before:
pp: case inr.inr
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
bigcalc : ∀ μ ∈ S, ↑μ bigKᶜ ≤ ε
⊢ IsCompact bigK

Tactic:
refine TotallyBounded.isCompact_of_isClosed ?_ ?_

Goal state after:
case inr.inr.refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
bigcalc : ∀ μ ∈ S, ↑μ bigKᶜ ≤ ε
⊢ TotallyBounded bigK

case inr.inr.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
bigcalc : ∀ μ ∈ S, ↑μ bigKᶜ ≤ ε
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] bigK
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case insert
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✝
⊢ ∫ᵛ (x : X) in s a✝, f x ∂[B; μ] + ∫ᵛ (x : X) in ⋃ x ∈ s✝, s x, f x ∂[B; μ] =
    ∫ᵛ (x : X) in s a✝, f x ∂[B; μ] + ∑ x ∈ s✝, ∫ᵛ (x : X) in s x, f x ∂[B; μ]

Tactic:
IH hs.2 h's.1 hf.2

Goal state after:
case insert
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✝
⊢ ∫ᵛ (x : X) in s a✝, f x ∂[B; μ] + ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ] =
    ∫ᵛ (x : X) in s a✝, f x ∂[B; μ] + ∑ x ∈ s✝, ∫ᵛ (x : X) in s x, f x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
a : Finset ℕ
⊢ StronglyMeasurable fun a_1 ↦ ∑ y ∈ a, ν (Prod.mk a_1 ⁻¹' f y)

Tactic:
apply Finset.stronglyMeasurable_fun_sum _ (fun i hi ↦ ?_)

Goal state after:
ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
a : Finset ℕ
i : ℕ
hi : i ∈ a
⊢ StronglyMeasurable fun a ↦ ν (Prod.mk a ⁻¹' f i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
hs : IsLinearSet s
⊢ IsLinearSet (a +ᵥ s)

Tactic:
rcases hs with ⟨b, t, ht, rfl⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
⊢ IsLinearSet (a +ᵥ b +ᵥ ↑(closure t))
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:
vadd_vadd

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
⊢ (a + b) +ᵥ ↑(closure t) = (a + b) +ᵥ ↑(closure t)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.add.inr.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x : M
hx : x ∈ closure (insert a t)
hx✝ : a + x ∈ closure (a +ᵥ ↑(closure t))
y : M
hy : y ∈ closure (insert a t)
hy✝ : a + y ∈ closure (a +ᵥ ↑(closure t))
⊢ a + (a + (x + y)) = a + x + (a + y)

Tactic:
simp_rw [← add_assoc, add_right_comm a a x]

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

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

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
⊢ IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))

Tactic:
induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
   =>  _ 

Goal state after:
case h
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
n : ℕ
ih : ∀ m < n, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
a : M
t : Finset M
hn : t.card = n
⊢ IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
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
f : X → E
c : ℝ
hG : CompleteSpace G
this : (c • μ).variation = ‖c‖₊ • μ.variation
⊢ (setToFun (‖c‖₊ • μ.variation) ⇑((c • μ).transpose B) ⋯ fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x

Tactic:
have : DominatedFinMeasAdditive μ.variation ((c • μ).transpose B) (‖c‖ * ‖B‖) := by
    simp only [transpose_smul, FunLike.coe_smul]
    exact (dominatedFinMeasAdditive_cbmApplyMeasure μ B).smul c

Goal state after:
case pos
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
f : X → E
c : ℝ
hG : CompleteSpace G
this✝ : (c • μ).variation = ‖c‖₊ • μ.variation
this : DominatedFinMeasAdditive μ.variation (⇑((c • μ).transpose B)) (‖c‖ * ‖B‖)
⊢ (setToFun (‖c‖₊ • μ.variation) ⇑((c • μ).transpose B) ⋯ fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ (if i ∈ t' then g i - f i else g i + f i) = g i - f i

Tactic:
by simp [hi]

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

Goal state before:
pp: 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
refine setToFun_add_left'' (by simp [transpose]) hB hB ?_
    (norm_nonneg _) (norm_nonneg _) (norm_nonneg _)
  nth_rw 1 [← add_zero μ.variation]
  gcongr
  exact Measure.zero_le μ.variation

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

Goal state before:
pp: 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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ ENNReal.ofReal (dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ]) ≤
    ‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Goal state after:
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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ (‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        φ.Realize ((Sum.elim a (Fin.cons a_1 finZeroElim) ∘ ⇑e.symm) ∘ Sum.inl)
          ((Sum.elim a (Fin.cons a_1 finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr)}

Tactic:
congr! 4

Goal state after:
case e'_8
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ = (Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
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
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : ¬AEStronglyMeasurable f (Measure.map φ μ.variation)
⊢ ¬AEStronglyMeasurable f (μ.map φ).variation

Tactic:
· rwa [hφ.variation_map]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

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

Tactic:
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✝ : ⊤.FG
h : S.FG
⊢ S.FG

Tactic:
exact h

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

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

Tactic:
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
h : S.CG
⊢ S.CG

Tactic:
exact h

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f fst✝¹ k ⋯) snd✝¹ = (f fst✝ k ⋯) snd✝
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst k ⋯) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst k ⋯) ⟨fst✝, snd✝⟩.snd

Tactic:
exact h

Goal state after:
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) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom), (inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)) →
    f ≤ g

Tactic:
· rintro ⟨dom_le_dom, le_cod, h_eq⟩
    rw [le_def]
    exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; rfl⟩

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
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
⊢ F.cod = ⊤

Tactic:
rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]

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
h : a ≤ b → f a ≤ f b
⊢ a ≤ b → f a ≤ f b

Tactic:
exact h

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
h : f a ≤ f b ↔ a ≤ b
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
exact h

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋃ i ∈ S, i)ᶜ

Tactic:
compl_iUnion

Goal state after:
ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋂ i ∈ S, iᶜ)
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3

Tactic:
by
  contrapose! H
  rw [sumInv_pqr]
  have h3q := H.trans hpq
  have h3r := h3q.trans hqr
  have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
  have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3q)
  have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3r)
  calc
    (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
    _ = 1 := by norm_num

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

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

Tactic:
replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩

Goal state after:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}