mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case h_bound.hd
ι : 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 ℕ
x : X
⊢ (↑a).PairwiseDisjoint fun y ↦ Prod.mk x ⁻¹' f y

Tactic:
exact fun i hi j hj hij ↦ (f_disj hij).preimage _

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝² : CompleteSpace G
inst✝¹ : IsFiniteMeasure μ.variation
inst✝ : SFinite ν.variation
⊢ (μ.prod ν B).variation ≤ ‖B‖ₑ • μ.variation.prod ν.variation

Tactic:
apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

Goal state after:
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝² : CompleteSpace G
inst✝¹ : IsFiniteMeasure μ.variation
inst✝ : SFinite ν.variation
s : Set (X × Y)
hs : MeasurableSet s
⊢ ‖(μ.prod ν B) s‖ₑ ≤ (‖B‖ₑ • μ.variation.prod ν.variation) s
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
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s

Tactic:
by
  rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
  · simp
  by_cases hs : MeasurableSet s; swap
  · simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero]
    have : 0 ≤ C := le_trans (norm_nonneg _) (hC x hx)
    positivity
  apply norm_setIntegral_le_of_norm_le_const_ae
  filter_upwards [ae_restrict_mem hs] with x hx using hC x hx

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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂((μ.restrict s).transpose B).variation ≤ ∫⁻ (x : X) in s, ‖f x‖ₑ ∂(μ.transpose B).variation

Tactic:
transpose_restrict,

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
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂((μ.transpose B).restrict s).variation ≤ ∫⁻ (x : X) in s, ‖f x‖ₑ ∂(μ.transpose B).variation
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (μ.transpose B).variation ≤ ‖B‖₊ • μ.variation

Tactic:
apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
⊢ ‖(μ.transpose B) s‖ₑ ≤ (‖B‖₊ • μ.variation) s
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
μ : 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‖₊
hC : C ≠ 0
this : μ.variation ≤ C⁻¹ • (μ.transpose B).variation
⊢ C • μ.variation ≤ (μ.transpose B).variation

Tactic:
grw [this, smul_smul, mul_inv_cancel₀ hC, one_smul]

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

Goal state before:
pp: case a.inr
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‖₊
hC : C ≠ 0
⊢ μ.variation ≤ C⁻¹ • (μ.transpose B).variation

Tactic:
apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

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
μ : 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‖₊
hC : C ≠ 0
s : Set X
hs : MeasurableSet s
⊢ ‖μ s‖ₑ ≤ (C⁻¹ • (μ.transpose B).variation) s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
μ : VectorMeasure X F
⊢ ∀ (x : ℝ) (y : F), ‖((lsmul ℝ ℝ) x) y‖₊ = ‖x‖₊ * ‖y‖₊

Tactic:
simp [nnnorm_smul, mul_comm]

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

Goal state before:
pp: X : Type u_2
E : Type u_4
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
μ : SignedMeasure X
⊢ ∀ (x : E) (y : ℝ), ‖((lsmul ℝ ℝ).flip x) y‖₊ = ‖x‖₊ * ‖y‖₊

Tactic:
simp [nnnorm_smul, mul_comm]

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
hf : μ.Integrable f
⊢ (μ.withDensity f B).variation ≤ (μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

Goal state after:
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
s : Set X
hs : MeasurableSet s
⊢ ‖(μ.withDensity f B) s‖ₑ ≤ ((μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ) s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case insert
ι : Type u_1
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
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
hf : (μ a).Integrable f ∧ ∀ a ∈ s, (μ a).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ a + ∑ i ∈ s, μ i] = ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
integral_add_vectorMeasure hf.1 (Integrable.finsetSum_vectorMeasure hf.2),

Goal state after:
case insert
ι : Type u_1
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
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
hf : (μ a).Integrable f ∧ ∀ a ∈ s, (μ a).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ a] + ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] =
    ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case insert
ι : Type u_1
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
a : ι
s : Finset ι
ha : a ∉ s
ih : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
⊢ ∫ᵛ (x : X), f x ∂[B a + ∑ i ∈ s, B i; μ] = ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]

Tactic:
integral_add_cbm hf,

Goal state after:
case insert
ι : Type u_1
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
a : ι
s : Finset ι
ha : a ∉ s
ih : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
⊢ ∫ᵛ (x : X), f x ∂[B a; μ] + ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] =
    ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case neg
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
hxu : a + x + u ∈ s
⊢ w + u ∈ f a

Tactic:
have hw₂ : w ∈ g (a + x + u) := by
      apply AddSemigroupIdeal.subset_closure
      refine Set.mem_sdiff_of_mem ?_ hw₁
      rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]

Goal state after:
case neg
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
hxu : a + x + u ∈ s
hw₂ : w ∈ g (a + x + u)
⊢ w + u ∈ f a
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:
by rw [BoundedFormula.realize_iff]

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : a + f x = b + g x
hy : a + f x + f y = b + g x + g y
hz : a + f x + f z = b + g x + g z
| a + f x + f y + f z

Tactic:
hy,

Goal state after:
M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : a + f x = b + g x
hy : a + f x + f y = b + g x + g y
hz : a + f x + f z = b + g x + g z
| b + g x + g y + f z
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
w✝ : f.dom ≤ g.dom
eq_fun : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
n : N
hn : n ∈ f.cod
m : ↥f.dom := f.toEquiv.symm ⟨n, hn⟩
this : (f.cod.subtype.comp f.toEquiv.toEmbedding) m = n
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝))) m ∈ g.cod

Tactic:
simp only [Embedding.comp_apply, coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
    SetLike.coe_mem]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case h
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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ (Substructure.closure L).toFun ((fun a ↦ ⟦Structure.Sigma.mk f i a⟧) '' range y) = S

Tactic:
← image_univ,

Goal state after:
case h
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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ (Substructure.closure L).toFun ((fun a ↦ ⟦Structure.Sigma.mk f i a⟧) '' y '' univ) = S
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
f : ↑hs.basisSet → ℕ
⊢ 0 ≤ (hs.basis.repr (toRatVec (∑ i, f i • ↑i))) i

Tactic:
simp_rw [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
f : ↑hs.basisSet → ℕ
⊢ 0 ≤ ∑ c, (hs.basis.repr (toRatVec (f c • ↑c))) i
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 := ⋯
δ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
⊢ ((μ.restrict s).transpose B).variation ≤ (μ.transpose B).variation

Tactic:
transpose_restrict,

Goal state after:
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
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
⊢ ((μ.transpose B).restrict s).variation ≤ (μ.transpose B).variation
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ hs.fract x ∈ hs.fundamentalDomain

Tactic:
by
  classical
  intro i
  constructor
  · rw [hs.toRatVec_fract_eq, add_sub_cancel_left]
    simp [← hs.basis_apply, Finsupp.single_apply]
  · rw [hs.toRatVec_fract_eq, add_sub_cancel_left]
    simp [← hs.basis_apply, Finsupp.single_apply, Int.fract_lt_one]

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

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

Tactic:
exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

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

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

Tactic:
exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) → ∃ i, M ∈ L.age (G i)

pp: case mpr
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ (∃ i, M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)

Tactic:
· rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]

Goal state after:
case mpr
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ (∃ i, M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := ⋯
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ ↑((r.comp g).equivRange x) = ↑((r.comp g).equivRange (s.equivRange.symm ⟨s x, ⋯⟩))

Tactic:
simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]

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
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
have h := StrongHomClass.map_rel f leSymb ![a, b]

Goal state after:
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 : RelMap leSymb (⇑f ∘ ![a, b]) ↔ RelMap leSymb ![a, b]
⊢ f a ≤ f b ↔ a ≤ b