mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤
    ∑' (i : ℕ), (m (f i ∩ s) + ∑ u ∈ A i, m u)

Tactic:
ENNReal.tsum_add

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤
    ∑' (a : ℕ), m (f a ∩ s) + ∑' (a : ℕ), ∑ u ∈ A a, m u
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
this : f = (⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2
⊢ MemLp ((⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2) p μ

Tactic:
exact MemLp.add (Isometry.inl.lipschitz.comp_memLp (by simp) h.1)
      (Isometry.inr.lipschitz.comp_memLp (by simp) h.2)

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 = ∞
⊢ (μ.restrict μ.sigmaFiniteSetᶜ) s ≤ μ s

Tactic:
exact μ.restrict_le_self _

Goal state after:
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}
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) ⋯)
⊢ ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ = ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)‖

Tactic:
congr

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}
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) ⋯)
⊢ MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg) = MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : 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))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ε * ∑' (i : ℕ), 2 ^ (-(↑i + 1)) = ε * 1

Tactic:
congr

Goal state after:
case e_a
𝓧 : 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))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ∑' (i : ℕ), 2 ^ (-(↑i + 1)) = 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
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
hf : AEStronglyMeasurable f (μ.variation.restrict t)
⊢ ∀ᵐ (x : X) ∂μ.variation, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x

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
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
ht : MeasurableSet t
hf : AEStronglyMeasurable f (μ.variation.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ AEStronglyMeasurable.mk f hf x = 0 x
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ μ.restrict s - ν.restrict s = 0

Tactic:
exact sub_eq_zero_of_le hs.le_on

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
have h₂' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
  sub_apply_eq_zero_of_isHahnDecomposition hsc

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ (VectorMeasure.variation μ) (s ∩ r ∪ sᶜ ∩ r) = (VectorMeasure.variation μ) r

Tactic:
congr

Goal state after:
case e_6
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ s ∩ r ∪ sᶜ ∩ r = r
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 : E →L[ℝ] F →L[ℝ] G
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ.variation
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal = ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm

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 : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ.variation
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal =
    ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal
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
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

Tactic:
rw [integral_eq_setToFun_transpose hf]
    apply (enorm_setToFun_le _ (by simp)).trans (by simp)

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
⊢ dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ ‖B‖ * (∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal

Tactic:
grw [dist_eq_norm, ← integral_sub hf hg, norm_integral_le_lintegral_norm]
  simp [edist_eq_enorm_sub]

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

Goal state before:
pp: case _1
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s

Tactic:
rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx

Goal state after:
case _1
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : k + (x - k) % p + (x - k) / p * p ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case e_f
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
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ f x = f default

Tactic:
congr

Goal state after:
case e_f
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
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ x = default
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
⊢ ∀ (b c : (i : ι) → M i),
    x + b ∈ {x | x ∈ s ∧ x i = a} → x + c ∈ {x | x ∈ s ∧ x i = a} → x + b + c ∈ {x | x ∈ s ∧ x i = a}

Tactic:
y

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y : (i : ι) → M i
⊢ ∀ (c : (i : ι) → M i),
    x + y ∈ {x | x ∈ s ∧ x i = a} → x + c ∈ {x | x ∈ s ∧ x i = a} → x + y + c ∈ {x | x ∈ s ∧ x i = 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})
x : M
hx : x ∈ s
⊢ ∀ y ∈ s, x ≤ y → g x ≤ g y

Tactic:
y

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})
x : M
hx : x ∈ s
y : M
⊢ y ∈ s → x ≤ y → g x ≤ g y
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), x + y ∈ f a → y ∈ f a

Tactic:
y

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 : x ∈ f a
y : M
⊢ x + y ∈ f a → y ∈ f a
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → N.FG

Tactic:
rintro ⟨t', h, rfl⟩

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
t' : Set M
h : t'.Finite
⊢ ((closure L).toFun t').FG
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : Set M
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
exact h.substructure_closure L

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 : ι → ℕ
hx : x ∈ {x | a + f x = b + g x}
⊢ ∀ (b_1 c : ι → ℕ),
    x + b_1 ∈ {x | a + f x = b + g x} → x + c ∈ {x | a + f x = b + g x} → x + b_1 + c ∈ {x | a + f x = b + g x}

Tactic:
y

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 : ι → ℕ
hx : x ∈ {x | a + f x = b + g x}
y : ι → ℕ
⊢ ∀ (c : ι → ℕ), x + y ∈ {x | a + f x = b + g x} → x + c ∈ {x | a + f x = b + g x} → x + y + c ∈ {x | a + f x = b + g x}
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
⊢ IsSlice {x | a + f x = b + g x}

Tactic:
intro x hx y z hy hz

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 : ι → ℕ
hx : x ∈ {x | a + f x = b + g x}
y z : ι → ℕ
hy : x + y ∈ {x | a + f x = b + g x}
hz : x + z ∈ {x | a + f x = b + g x}
⊢ x + y + z ∈ {x | a + f x = b + g x}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
⊢ IsSemilinearSet {x | a + f x = b + g x}

Tactic:
rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, h, hh⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : AddMonoidHom.mrange h = ⊤
⊢ IsSemilinearSet {x | a + f x = b + g x}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) = ↑⟨a, ⋯⟩ +ᵥ ↑(closure (⇑(closure (insert a t)).subtype '' ⇑(closure (insert a t)).subtype ⁻¹' t))

Tactic:
congr

Goal state after:
case e_a
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ t = ⇑(closure (insert a t)).subtype '' ⇑(closure (insert a t)).subtype ⁻¹' t
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i ↦ (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i ↦ ↥(S i).dom) (fun x x_1 hij ↦ inclusion ⋯) (fun i ↦ ↥(S i).cod)
              (fun x x_1 hij ↦ inclusion ⋯) (fun i ↦ (S i).toEquiv) ⋯).toEmbedding.comp
        (of L ι (fun x ↦ ↥({ toFun := fun i ↦ (S i).dom, monotone' := ⋯ } x)) (fun x x_1 h ↦ inclusion ⋯) i)) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
congr

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) := ⋯
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)

Tactic:
simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h

Goal state after:
case refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f ↦ ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : cod_f.subtype.toHom.comp equiv_f.toHom = (↑f').cod.subtype.toHom.comp (↑f').toEquiv.toHom
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)