mathlib-initiative/mathlib-tactics huggingface dataset:
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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
this : m₁ ⟨s'', ⋯⟩ = m s''
⊢ edist (m₁ ⟨s'', ⋯⟩) (m₁ s) < 3 * δ

Tactic:
apply (m₁_lip _ _).trans_lt

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 μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := ⋯
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := ⋯
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
this : m₁ ⟨s'', ⋯⟩ = m s''
⊢ ↑1 * edist ⟨s'', ⋯⟩ s < 3 * δ
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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
Is : ‖m s'' - m₁ s‖ₑ < 3 * δ
s''t'C : s'' ∪ t' ∈ C
this : m₁ ⟨s'' ∪ t', ⋯⟩ = m (s'' ∪ t')
⊢ edist (m₁ ⟨s'' ∪ t', ⋯⟩) (m₁ ⟨↑s ∪ ↑t, ⋯⟩) < 4 * δ

Tactic:
apply (m₁_lip _ _).trans_lt

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 μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := ⋯
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := ⋯
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
Is : ‖m s'' - m₁ s‖ₑ < 3 * δ
s''t'C : s'' ∪ t' ∈ C
this : m₁ ⟨s'' ∪ t', ⋯⟩ = m (s'' ∪ t')
⊢ ↑1 * edist ⟨s'' ∪ t', ⋯⟩ ⟨↑s ∪ ↑t, ⋯⟩ < 4 * δ
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case pos
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
h : μ.HasProd ν B
s : Set X
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

Tactic:
by_cases h't : MeasurableSet t

Goal state after:
case pos
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
h : μ.HasProd ν B
s : Set X
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
h't : MeasurableSet t
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

case neg
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
h : μ.HasProd ν B
s : Set X
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
h't : ¬MeasurableSet t
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_add
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f : X → H
C : H →L[ℝ] E
hf : Integrable f μ.variation
hG : CompleteSpace G
⊢ ∀ ⦃f g : X → H⦄,
    Disjoint (support f) (support g) →
      Integrable f μ.variation →
        Integrable g μ.variation →
          ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ] →
            ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ] →
              ∫ᵛ (y : X), C ((f + g) y) ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[B ∘SL C; μ]

Tactic:
intro f g _ f_int g_int hf hg
    simp only [Pi.add_apply, _root_.map_add]
    rw [integral_fun_add (C.integrable_comp f_int) (C.integrable_comp g_int), hf, hg,
      integral_fun_add f_int g_int]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
⊢ IsSemilinearSet (⋃₀ S)

Tactic:
exact ⟨S, hS, fun s hs => (hS' s hs).isLinearSet, rfl⟩

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 : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ - ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
rw [sub_eq_add_neg, integral_add_vectorMeasure hμ hν.neg_vectorMeasure,
    integral_neg_vectorMeasure, ← sub_eq_add_neg]

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

Goal state before:
pp: case hf
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ∀ i ∈ Finset.range N, μ.IntegrableOn f (s i)

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ‖∑ i ∈ Finset.range N, ∫ᵛ (x : X) in s i, f x ∂[B; μ] + ∫ᵛ (x : X) in ⋃ n, s (n + N), f x ∂[B; μ] -
        ∑ i ∈ Finset.range N, ∫ᵛ (x : X) in s i, f x ∂[B; μ]‖ₑ ≤
    ∑' (k : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s (k + N), ‖f x‖ₑ ∂μ.variation

Tactic:
· exact fun i hi ↦ hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s])

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ‖∑ i ∈ Finset.range N, ∫ᵛ (x : X) in s i, f x ∂[B; μ] + ∫ᵛ (x : X) in ⋃ n, s (n + N), f x ∂[B; μ] -
        ∑ i ∈ Finset.range N, ∫ᵛ (x : X) in s i, f x ∂[B; μ]‖ₑ ≤
    ∑' (k : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s (k + N), ‖f x‖ₑ ∂μ.variation
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ‖∫ᵛ (x : X) in ⋃ n, s (n + N), f x ∂[B; μ]‖ₑ ≤ ∑' (k : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s (k + N), ‖f x‖ₑ ∂μ.variation

Tactic:
apply enorm_setIntegral_le_lintegral_enorm.trans_eq

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ‖B‖ₑ * ∫⁻ (x : X) in ⋃ n, s (n + N), ‖f x‖ₑ ∂μ.variation =
    ∑' (k : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s (k + N), ‖f x‖ₑ ∂μ.variation
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hs : s.Finite
⊢ (closure L).toFun ↑hs.toFinset = (closure L).toFun s

Tactic:
by rw [hs.coe_toFinset]

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✝ : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋂ i ∈ s, t i)

Tactic:
← sInter_image

Goal state after:
M : Type u_1
ι : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋂₀ (t '' s))
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 ι
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)⟧
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S

Tactic:
use i

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)⟧
⊢ ∃ T, Substructure.map (of L ι G f i).toHom T = S
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C✝

Tactic:
refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ N_incl.toHom.range.FG
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, hs.floor x i < 0) →
    ∃ i,
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z

Tactic:
intro ⟨hx, i, hi⟩
      refine ⟨i, ((- hs.floor x i).toNat - 1) • i.1, ?_,
        ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
        ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.1, ?_, ?_⟩
      · exact nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · rw [add_assoc x, ← succ_nsmul',
          tsub_add_cancel_of_le
            ((Int.le_toNat (neg_pos.2 hi).le).2 (le_neg.1 (Int.cast_le_neg_one_of_neg hi))),
          add_assoc x,
          Finset.add_sum_erase _ (fun j => (-hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 hi.le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x

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

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ i,
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z) →
    hs.fract x = hs.base ∧ ∃ i, hs.floor x i < 0

Tactic:
intro ⟨i, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, ?_⟩
      · apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz), hs.fract_base] at heq
      · rw [mem_closure_singleton] at hy
        rcases hy with ⟨n, rfl⟩
        apply congr_arg (hs.floor · i) at heq
        rw [hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz,
          hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',
          hs.floor_base, add_assoc x, ← succ_nsmul', hs.floor_add_nsmul_self,
          ← eq_neg_iff_add_eq_zero] at heq
        simpa [heq] using neg_one_lt_zero.trans_le (Nat.cast_nonneg _)

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
by
  constructor
  · rintro ⟨M, h1, h2, rfl⟩
    refine ⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1,
      age.hereditary M, age.jointEmbedding M⟩
  · rintro ⟨Kn, _, cq, hfg, hp, jep⟩
    obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep
    exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsUltrahomogeneous M → L.IsExtensionPair M M

Tactic:
intro M_homog

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
⊢ L.IsExtensionPair M M
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ↑i + ((hs.floor x i).toNat - 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
add_assoc hs.base,

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + (↑i + ((hs.floor x i).toNat - 1) • ↑i) + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + (hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
add_assoc hs.base,

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ((hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + ↑i + n • ↑i) i
⊢ 0 < hs.floor x i

Tactic:
add_assoc hs.base,

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + (↑i + n • ↑i)) i
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)

Tactic:
obtain ⟨_⟩ := denumerable_iff.2 h₁

Goal state after:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
val✝ : Denumerable ↑M₁
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case inl
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ ∃ U, IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ TotallySeparatedSpace (T.CompleteType α)

Tactic:
rw [totallySeparatedSpace_iff_exists_isClopen]
  intro p q hpq
  simp only [ne_eq, SetLike.ext_iff, not_forall, not_iff] at hpq
  obtain ⟨φ, hφ⟩ := hpq
  cases mem_or_not_mem p φ with
  | inl h =>
    refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
  | inr h =>
    refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ C r • pderivFun i f + f • 0 = C r * pderivFun i f

Tactic:
smul_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ C r • pderivFun i f + 0 = C r * pderivFun i f
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
n : σ →₀ ℕ
⊢ (n + single i 1) i ≠ (single j 1) i

Tactic:
grind [Finsupp.add_apply]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
g : MvPowerSeries σ R
n : ℕ
⊢ (pderiv R i) (g ^ n) = ↑n * g ^ (n - 1) * (pderiv R i) g

Tactic:
Derivation.leibniz_pow,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
g : MvPowerSeries σ R
n : ℕ
⊢ n • g ^ (n - 1) • (pderiv R i) g = ↑n * g ^ (n - 1) * (pderiv R i) g
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (φ m).Coprime (φ n)
⊢ False

Tactic:
Nat.totient_coprime_totient_iff,

Goal state after:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
⊢ False