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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
this : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : μ (⋃ i ∈ Ici n, f i) < ε / 2
⊢ μ ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ i, f i) ≤ μ ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i)

Tactic:
gcongr
      intro x hx
      simp only [Finset.mem_range, mem_symmDiff, mem_iUnion, exists_prop, not_exists, not_and,
        mem_Ici, mem_union] at hx ⊢
      grind

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

Goal state before:
pp: ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
⊢ μ = ν

Tactic:
by
  let e : ((Π i, X i) × T) ≃ᵐ ((Π i, X i) × (Unit → T)) :=
    { toFun p := ⟨fun i ↦ p.1 i, fun _ ↦ p.2⟩
      invFun p := ⟨fun i ↦ p.1 i, p.2 ()⟩
      left_inv p := by simp
      right_inv p := by simp }
  rw [← e.map_measurableEquiv_injective.eq_iff]
  refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map_equiv, integral_map_equiv]
  simpa [e] using h f (g ())

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

Goal state before:
pp: case hab
𝕜 : 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 := ⋯
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
⊢ infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖

Tactic:
infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]),

Goal state after:
case hab
𝕜 : 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
⊢ dist a ((algebraMap 𝕜 A) x) ≤ ‖(algebraMap 𝕜 A) x - a‖
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ

Tactic:
simp_rw [restrict_withDensity ht.compl]

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this :
  ProbabilityMeasure.toFiniteMeasure '' {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} = {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
⊢ IsCompact {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Tactic:
exact isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le 1 hu hK h

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
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : VectorMeasure X F
f : X → E
s t : Set X
hs : MeasurableSet s
hts : t ⊆ s
h : μ.IntegrableOn f s
ht : ¬MeasurableSet t
⊢ μ.IntegrableOn f t

pp: case pos
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 t : Set X
hs : MeasurableSet s
hts : t ⊆ s
h : μ.IntegrableOn f s
ht : MeasurableSet t
⊢ μ.IntegrableOn f t

Tactic:
· simp [VectorMeasure.IntegrableOn, restrict_not_measurable _ ht]

Goal state after:
case pos
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 t : Set X
hs : MeasurableSet s
hts : t ⊆ s
h : μ.IntegrableOn f s
ht : MeasurableSet t
⊢ μ.IntegrableOn f t
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
hs : MeasurableSet s
⊢ μ.Integrable (s.indicator f) ↔ μ.IntegrableOn f s

Tactic:
by
  simp [VectorMeasure.Integrable, VectorMeasure.IntegrableOn, MeasureTheory.IntegrableOn,
    MeasureTheory.integrable_indicator_iff hs, variation_restrict hs]

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

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
inst✝ : BorelSpace α
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
this✝ : MeasurableSpace α := borel α
⊢ {s | ∃ u v, u ≤ v ∧ s = Ioc u v} = {S | ∃ l u, l ≤ u ∧ Ioc l u = S}

Tactic:
grind only

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

Goal state before:
pp: α : 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
hf : BoundedVariationOn f univ
a : α
this✝ : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
this : Ici a = ⋃ n, Icc a (u n)
i j : ℕ
hij : i ≤ j
x : α
hx : x ∈ (fun n ↦ Icc a (u n)) i
⊢ x ∈ (fun n ↦ Icc a (u n)) j

Tactic:
by grind [Monotone]

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
x : E
y : F
⊢ ‖(B x) y‖₊ ≤ C * ‖x‖₊ * ‖y‖₊

Tactic:
by simp [hB]

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

Goal state before:
pp: case pos
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : μ.Integrable f
⊢ μ.withDensity f B = μ.withDensity g B

Tactic:
simp only [withDensity, hf, ↓reduceDIte, Integrable.congr hf h, mk.injEq]

Goal state after:
case pos
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : μ.Integrable f
⊢ (fun s ↦ ∫ᵛ (x : X) in s, f x ∂[B; μ]) = fun s ↦ ∫ᵛ (x : X) in s, g x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB✝ : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
hB : ‖B‖₊ = 0
⊢ ‖B‖₊ * 1 ≤ δ

Tactic:
by simp [hB]

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ.variation ⇑(μ.transpose B) ⋯ ↑↑f

Tactic:
exact continuous_setToFun _

Goal state after:
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ψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImp ψ).IsPrenex

Tactic:
rw [hφ.toPrenexImp]

Goal state after:
case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).IsPrenex
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✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs

Tactic:
rw [hφ.toPrenexImp]

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✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs
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
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
s : Set M
hs : ∃ a n f, s = a +ᵥ range ⇑f
f : F
⊢ IsSemilinearSet (⇑f ⁻¹' s)

Tactic:
rcases hs with ⟨a, n, g, rfl⟩

Goal state after:
M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet (⇑f ⁻¹' (a +ᵥ range ⇑g))
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✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ (f i ijk ⋯) x = (f k ijk ⋯) z

Tactic:
← DirectedSystem.map_map _ hiij hijijk,

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✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ (f ij ijk hijijk) ((f i ij hiij) x) = (f k ijk ⋯) z
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 (Sum.elim (fun a ↦ (x a).fst) 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:
rw [Sum.elim_range, upperBounds_union] 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 ↦ (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
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f ≤ g →
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom), (inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)

pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom), (inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)) →
    f ≤ g

Tactic:
· exact fun h ↦ ⟨dom_le_dom h, cod_le_cod h,
      by intro x; apply (subtype _).inj'; rwa [toEquiv_inclusion_apply]⟩

Goal state after:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom), (inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)) →
    f ≤ g
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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = RelMap R x

Tactic:
rw [relMap_quotient_mk']

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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a ↦ Structure.Sigma.mk f i (x a)) = RelMap R 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✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)

Tactic:
have : (.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd) : Σˣ f).fst ≤ i :=
    le_rfl

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 : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)
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 : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (f (Quotient.out (x a)).fst i ⋯) (Quotient.out (x a)).snd =
    (f (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst i this)
      (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).snd

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 : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (Quotient.out (x a)).fst ∈ range fun a ↦ (Quotient.out (x a)).fst

Tactic:
· simp only [DirectedSystem.map_self]

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 : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (Quotient.out (x a)).fst ∈ range fun a ↦ (Quotient.out (x a)).fst
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ toRatVec x ≤ toRatVec hs.base + toRatVec (∑ i, ↑i)

Tactic:
map_sum,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ toRatVec x ≤ toRatVec hs.base + ∑ x, toRatVec ↑x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
map_sum,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
f : ↑hs.basisSet → ℕ
⊢ 0 ≤ (∑ x, hs.basis.repr (toRatVec (f x • ↑x))) i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
hy : y ∈ closure t
this : (hs.basis.repr (toRatVec y)) i = 0
⊢ hs.floor (x + y) i = hs.floor x i

Tactic:
by
    simp [floor, this]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2.zero
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
e : ↑(F 0).out ≃[L] ↑N
⊢ ↑(F 0).out ↪[L] ↑(F 0).out

Tactic:
exact Embedding.refl _ _

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: α : Type u_2
s : Finset α
f : α → ℕ
⊢ λ (s.lcm f) = s.lcm (⇑λ ∘ f)

Tactic:
by
  classical
  refine s.induction ?_ fun a s ha ih ↦ ?_
  · exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton
  rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]
  exact carmichael_lcm ..

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
← ZMod.orderOf_five (n - 2),

Goal state after:
case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf 5 ∣ exponent (ZMod (2 ^ n))ˣ