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

Goal state before:
pp: κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
f : (i : κ) → Y i →ᵇ ℝ
g : Z →ᵇ ℝ
⊢ ∫ (x : Z × ((i : κ) → Y i)), (∏ i, (f i) ((e x).1 i)) * g (e x).2 ∂μ =
    ∫ (p : ((i : κ) → Y i) × Z), (∏ i, (f i) (p.1 i)) * g p.2 ∂Measure.map (⇑e) ν

Tactic:
integral_map_equiv

Goal state after:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
f : (i : κ) → Y i →ᵇ ℝ
g : Z →ᵇ ℝ
⊢ ∫ (x : Z × ((i : κ) → Y i)), (∏ i, (f i) ((e x).1 i)) * g (e x).2 ∂μ =
    ∫ (x : Z × ((i : κ) → Y i)), (∏ i, (f i) ((e x).1 i)) * g (e x).2 ∂ν
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 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (p : (Unit → Z) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) ν

Tactic:
integral_map_equiv

Goal state after:
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 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂ν
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ n, f n) \ ⋃ n ∈ Finset.range (N + 1), f n)).toReal +
      (μ ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)).toReal <
    ε

Tactic:
← add_halves ε

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ n, f n) \ ⋃ n ∈ Finset.range (N + 1), f n)).toReal +
      (μ ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)).toReal <
    ε / 2 + ε / 2
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
n : ℕ
⊢ MeasurableSet (B n)

Tactic:
simp only [dite_eq_ite, B]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
n : ℕ
⊢ MeasurableSet (if μ (A n) = 1 then A n else (A n)ᶜ)
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) = volume (closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n))

Tactic:
have := hε' n

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) = volume (closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n))
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ volume (closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n)) =
    1 - ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)

Tactic:
have := hε' n

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ volume (closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n)) =
    1 - ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

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

Tactic:
← add_halves ε

Goal state after:
case 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}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ‖indicatorConstLp p ms ⋯ a - indicatorConstLp p ms hμs b +
        (indicatorConstLp p ms hμs b - indicatorConstLp p mt hμt b)‖ <
    ε / 2 + ε / 2
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m ↑↑s - m ↑↑t‖ₑ ≤ μ (↑↑s \ ↑↑t) + μ (↑↑t \ ↑↑s)

Tactic:
nth_rewrite 1 [← Is]

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t) - m ↑↑t‖ₑ ≤ μ (↑↑s \ ↑↑t) + μ (↑↑t \ ↑↑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
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
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0

Tactic:
by_cases ht : MeasurableSet t; swap
  · simp [setIntegral_eq_zero_of_not_measurableSet ht]
  by_cases hf : AEStronglyMeasurable f (μ.restrict t).variation; swap
  · rw [integral_undef]
    contrapose hf
    exact hf.1
  simp only [variation_restrict ht] at hf
  have : ∫ᵛ x in t, hf.mk f x ∂[B; μ] = 0 := by
    refine integral_eq_zero_of_ae ?_
    simp only [variation_restrict ht]
    apply (ae_restrict_iff' ht).2
    filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
    rw [← hx h''x]
    exact h'x h''x
  rw [← this]
  apply integral_congr_ae
  simp only [variation_restrict ht]
  exact hf.ae_eq_mk

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ IsSemilinearSet (⋃₀ range s)

Tactic:
apply sUnion (finite_range s)

Goal state after:
M : Type u_1
ι : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ ∀ s_1 ∈ range s, IsSemilinearSet s_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

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

Tactic:
exact Or.inl rfl

Goal state after:
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
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : x i + y i = a
hxz : x + z ∈ s
hxzi : x i + z i = a
⊢ a = x i

Tactic:
hxi

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 z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : x i + y i = a
hxz : x + z ∈ s
hxzi : x i + z i = a
⊢ a = 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
⊢ IsSemilinearSet {y | y ∈ s ∧ a ≤ y}

Tactic:
convert_to IsSemilinearSet (a +ᵥ (f a : Set M))

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
⊢ {y | y ∈ s ∧ a ≤ y} = a +ᵥ ↑(f a)

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
⊢ IsSemilinearSet (a +ᵥ ↑(f a))
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
          ({ toFun := fun x ↦ x ∘ ⇑e.symm, map_add' := ⋯, map_smul' := ⋯ } (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘
            Sum.inl)
          ({ toFun := fun x ↦ x ∘ ⇑e.symm, map_add' := ⋯, map_smul' := ⋯ } (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘
            Sum.inr)}

Tactic:
LinearMap.coe_mk,

Goal state after:
α : 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 ({ toFun := fun x ↦ x ∘ ⇑e.symm, map_add' := ⋯ } (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inl)
          ({ toFun := fun x ↦ x ∘ ⇑e.symm, map_add' := ⋯ } (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inr)}
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight φ✝).IsPrenex

Tactic:
rw [hψ.toPrenexImpRight]; exact (hφ.imp hψ).isPrenex

Goal state after:
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
⊢ (φ ⇔ ∀' liftAt 1 n φ).Realize v xs

Tactic:
by
  rw [realize_iff, realize_all_liftAt_one_self]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ ((f' (m + k)).comp (Nat.leRecOn ⋯ (fun {k} g ↦ (f' k).comp g) (Embedding.refl L (G' m)))) x =
    (f' (m + k)) (Nat.leRecOn ⋯ (fun {k} ↦ ⇑(f' k)) x)

Tactic:
← natLERec,

Goal state after:
case succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ ((f' (m + k)).comp (natLERec f' m (m + k) ⋯)) x = (f' (m + k)) (Nat.leRecOn ⋯ (fun {k} ↦ ⇑(f' k)) x)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (s₁' ∩ s₂')

Tactic:
← image_preimage_eq (s₁' ∩ s₂') hf,

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f '' ⇑f ⁻¹' (s₁' ∩ s₂'))
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
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) m ∈ g.cod

Tactic:
← eq_fun

Goal state after:
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
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
h : f ≤ g
⊢ g.toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp f.toEquiv.toEmbedding

Tactic:
rw [← (subtype _).comp_inj, subtype_toEquiv_inclusion h]
  ext
  simp

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
F : L.Functions n✝
i : ι
y : Fin n✝ → G i
⊢ Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧) =
    funMap F (Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ∘ fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧)

Tactic:
change _ = funMap F (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y)

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
F : L.Functions n✝
i : ι
y : Fin n✝ → G i
⊢ Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧) =
    funMap F (Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ∘ Quotient.mk (setoid G f) ∘ Structure.Sigma.mk f i ∘ y)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥(map PM.toHom ⊤), str := inferInstance } ≈ P

Tactic:
← Hom.range_eq_map

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs ↔ RelMap graphRel.adj xs

Tactic:
rw [iff_eq_eq]
      change RelMap adj ![xs 0, xs 1] = _
      refine congr rfl (funext ?_)
      simp [Fin.forall_fin_two]

Goal state after: