mathlib-initiative/mathlib-tactics huggingface dataset:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε

Tactic:
rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ (algebraMap 𝕜 A) x ∈ ⇑(algebraMap 𝕜 A) '' μ.support

Tactic:
simp [hx]

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

Goal state before:
pp: case 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}
⊢ D.Countable

Tactic:
let f (nds : Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) : Lp E p μ := key nds.1 nds.2.1 nds.2.2
    have := count_𝒜₀.to_subtype
    have := countable_u.to_subtype
    have : D ⊆ range f := by
      rintro - ⟨n, d, s, rfl⟩
      use ⟨n, (d, s)⟩
    exact (countable_range f).mono this

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts, t ⊆ s
⊢ ∑ p ∈ (Q'.extendOfLE ⋯).parts, ‖μ p‖ₑ ≤ preVariationFun (fun p ↦ ‖μ p‖ₑ) s

Tactic:
apply preVariation.sum_le' (fun p => ‖μ p‖ₑ) hs

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := ⋯
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts, t ⊆ s
⊢ ∀ p ∈ (Q'.extendOfLE ⋯).parts, MeasurableSet p
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ μ.variation s = 0 ↔ ∀ t ⊆ s, MeasurableSet t → μ t = 0

Tactic:
refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
  · rw [← enorm_eq_zero, ← le_zero_iff, ← h]
    apply (enorm_measure_le_variation _ _).trans (measure_mono hts)
  · suffices μ.variation s ≤ (0 : Measure X) s by simpa
    apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
    simp [h t hts ht]

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : VectorMeasure X F
f : X → E
s : Set X
h : μ.Integrable f
⊢ μ.IntegrableOn f s

Tactic:
← integrableOn_univ

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : VectorMeasure X F
f : X → E
s : Set X
h : μ.IntegrableOn f univ
⊢ μ.IntegrableOn f s
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ¬∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0

Tactic:
simp [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
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0
⊢ ∫ᵛ (x : X) in univ, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
apply setIntegral_eq_of_subset_of_ae_sdiff_eq_zero hs MeasurableSet.univ (subset_univ _)

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
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation.restrict (univ \ s), f x = 0
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f✝ μ.variation
f g : X → E
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
⊢ Integrable g μ.variation →
    C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ] →
      C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ] →
        C ∫ᵛ (y : X), (f + g) y ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
g_int

Goal state after:
case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f✝ μ.variation
f g : X → E
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
⊢ C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ] →
    C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ] →
      C ∫ᵛ (y : X), (f + g) y ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[(compL ℝ F G H) C ∘SL B; μ]
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
a✝ : Disjoint (support f) (support g)
f_int : 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:
g_int

Goal state after:
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
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : 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; μ]
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
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
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
x : X
hx : f x = g x
⊢ C (f x) = C (g x)

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
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 : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s

Tactic:
simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero]

Goal state after:
case neg
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 : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
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
hx : x ∈ s
hs : ¬MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s

Tactic:
simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero]

Goal state after:
case neg
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
hx : x ∈ s
hs : ¬MeasurableSet s
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s
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 ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y

Tactic:
intro x hx y hy hxy z hz

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
hy : y ∈ s
hxy : x ≤ y
z : M
hz : z ∈ g x
⊢ z ∈ g y
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Fintype α
t : presburger[[↑A]].Term α
⊢ ∃ k u, ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v

Tactic:
classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊔ ψ ⟹ θ).Realize v xs

Tactic:
by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact fun h => h.elim (h₁ M v xs) (h₂ M v xs)

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isQF
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
xs : Fin n✝ → M
⊢ ∀ {ψ : L.BoundedFormula α n✝}, ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)

Tactic:
intro ψ

Goal state after:
case of_isQF
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
⊢ ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
⊢ ∀ {ψ : L.BoundedFormula α n✝}, ψ.IsPrenex → (((∀' φ✝).toPrenexImp ψ).Realize v xs ↔ (∀' φ✝ ⟹ ψ).Realize v xs)

Tactic:
intro ψ

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
⊢ ψ.IsPrenex → (((∀' φ✝).toPrenexImp ψ).Realize v xs ↔ (∀' φ✝ ⟹ ψ).Realize v xs)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
⊢ ∀ {ψ : L.BoundedFormula α n✝}, ψ.IsPrenex → (((∃' φ✝).toPrenexImp ψ).Realize v xs ↔ (∃' φ✝ ⟹ ψ).Realize v xs)

Tactic:
intro ψ

Goal state after:
case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
⊢ ψ.IsPrenex → (((∃' φ✝).toPrenexImp ψ).Realize v xs ↔ (∃' φ✝ ⟹ ψ).Realize v xs)
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
· obtain ⟨f, rfl⟩ := h
      exact ⟨range f, countable_range _, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ φ.toPrenex.Realize v xs

Tactic:
realize_toPrenex

Goal state after:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : ∅.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ φ.Realize v xs
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 ι
α : Type u_1
inst✝ : Finite α
x y : α → Σˣ f
xy : x ≈ y
i : ι
hi : i ∈ upperBounds (range fun a ↦ (x a).fst) ∩ upperBounds (range fun a ↦ (y a).fst)
⊢ ∃ i,
    ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy

Tactic:
simp_rw [← Function.comp_apply (f := Sigma.fst)] at hi

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 ι
α : Type u_1
inst✝ : Finite α
x y : α → Σˣ f
xy : x ≈ y
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Sigma.fst ∘ x) a) ∩ upperBounds (range fun a ↦ (Sigma.fst ∘ y) a)
⊢ ∃ i,
    ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy
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
n : ℕ
⊢ ⌊(hs.basis.repr (toRatVec (x + n • ↑i) - toRatVec hs.base)) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑n

Tactic:
rw [map_add, ← sub_add_eq_add_sub]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
n : ℕ
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (n • ↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑n
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun f ↦ f.toPartialEquiv

Tactic:
by
  intro _ _ h
  ext
  rw [PartialEquiv.ext_iff] at h
  rcases h with ⟨_, H⟩
  exact H _ (Substructure.mem_top _)

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
simp only [partialEquivLimit, Equiv.comp_toEmbedding, Embedding.comp_assoc]
  rw [Equiv_isup_symm_inclusion]
  congr

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

Goal state before:
pp: case a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
f : ↑hs.basisSet → ℕ
x✝ : ↑hs.basisSet
a✝ : x✝ ∈ Finset.univ
⊢ Int.fract ((hs.basis.repr (toRatVec (x + ∑ i, f i • ↑i) - toRatVec hs.base)) x✝) =
    Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝)

Tactic:
rw [map_add, ← sub_add_eq_add_sub]

Goal state after:
case a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
f : ↑hs.basisSet → ℕ
x✝ : ↑hs.basisSet
a✝ : x✝ ∈ Finset.univ
⊢ Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (∑ i, f i • ↑i))) x✝) =
    Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝)
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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) :=
  Embedding.codRestrict (⨆ i, S i) (liftInclusion S) liftInclusion_in_sup
m : M
hm✝ : m ∈ ⨆ i, S i
hm : m ∈ (liftInclusion S).toHom.range
⊢ ∃ a, F a = ⟨m, hm✝⟩

Tactic:
Hom.mem_range

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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) :=
  Embedding.codRestrict (⨆ i, S i) (liftInclusion S) liftInclusion_in_sup
m : M
hm✝ : m ∈ ⨆ i, S i
hm : ∃ y, (liftInclusion S).toHom y = m
⊢ ∃ a, F a = ⟨m, hm✝⟩