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

Goal state before:
pp: case inr
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
h_le : (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) ≤ fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}
i : ι
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun r ↦ r / √↑(Fintype.card ι)) atTop atTop

Tactic:
exact tendsto_id.atTop_div_const (by positivity)

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
z : E
⊢ Tendsto (fun r ↦ ⨆ i, (μ i) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
refine Nat.tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) (h z) (fun n u v huv ↦ by gcongr)

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
z : E
n : ℕ
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case pos
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
hs₁ : MeasurableSet s₁
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂

Tactic:
have := sum_le_preVariationFun_of_subset f hs₁ hs₂ h
    simp_all [preVariationFun]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂

Tactic:
by
  by_cases hs₁ : MeasurableSet s₁
  · have := sum_le_preVariationFun_of_subset f hs₁ hs₂ h
    simp_all [preVariationFun]
  · simp [preVariationFun, hs₁]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toFinite = μ

Tactic:
by
  rw [Measure.toFinite, Measure.toFiniteAux, if_pos, ProbabilityTheory.cond_univ]
  infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
⊢ ⋃ i, f i ∈ C → (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
hf_mem

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
rw [m.extend_eq hC hf_mem]

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

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

Tactic:
apply le_trans <| (OuterMeasure.ofFunction m addContent_empty).mono
      <| (iUnion_sdiff s f) ▸ sdiff_subset_sdiff_left hf_subset

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯).measureOf (⋃ i, f i \ s) ≤ ∑' (a : ℕ), ∑ u ∈ A a, m u
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μ : IsSeparable μ
⊢ IsSeparable μ.completion

Tactic:
obtain ⟨𝒜, count_𝒜, h𝒜⟩ := exists_countable_measureDense μ

Goal state after:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
hμ : IsSeparable μ
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
⊢ IsSeparable μ.completion
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
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)
⊢ 0 < 3 * (1 + μ.real s ^ (1 / p.toReal))

Tactic:
linarith [μs_pow_nonneg]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
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
⊢ 0 < 1 + μ.real s ^ (1 / p.toReal)

Tactic:
linarith [μs_pow_nonneg]

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
a : ℝ≥0∞
ha : a < μ.variation s
⊢ ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ

Tactic:
simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply]
    at ha ⊢
  obtain ⟨P, hP⟩ : ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet),
      a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) p :=
    preVariation.exists_Finpartition_sum_gt (‖μ ·‖ₑ) _ ha
  refine ⟨P.parts.map (Function.Embedding.subtype _), ?_, ?_, ?_, ?_⟩
  · simp only [mem_map, Function.Embedding.subtype_apply, Subtype.exists, exists_and_right,
      exists_eq_right, forall_exists_index]
    intro t ht h't
    exact P.le h't
  · intro i hi  j hj hij
    simp only [coe_map, Function.Embedding.subtype_apply, Set.mem_image, SetLike.mem_coe,
      Subtype.exists, exists_and_right, exists_eq_right] at hi hj
    rcases hi with ⟨h'i, i_mem⟩
    rcases hj with ⟨h'j, j_mem⟩
    exact (disjoint_subtype_iff (fun _ _ hs ht ↦ hs.inter ht) _).1
      (P.disjoint i_mem j_mem (by simpa using hij))
  · simp +contextual
  · rwa [Finset.sum_map]

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 : α
⊢ hf.vectorMeasure (Iio a) = Function.leftLim f a - atBot.limUnder f

Tactic:
have := hf.vectorMeasure_Iic a
  rw [← Iio_union_Icc_eq_Iic le_rfl, VectorMeasure.of_union (by simp) measurableSet_Iio
    measurableSet_Icc, hf.vectorMeasure_Icc le_rfl] at this
  grind

Goal state after:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ

Tactic:
grw [variation_transpose_le]

Goal state after:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ eLpNorm (f - ⇑g) 1 (‖B‖₊ • μ.variation) ≤ ↑δ
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ ⊤.FG

Tactic:
refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩

Goal state after:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ (map S.subtype.toHom ⊤).FG

case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.FG
⊢ S.FG
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))

Tactic:
rw [← Fin.comp_snoc]

Goal state after:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)
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 ι
i : ι
x y : G i
h : (fun a ↦ ⟦Structure.Sigma.mk f i a⟧) x = (fun a ↦ ⟦Structure.Sigma.mk f i a⟧) y
⊢ x = y

Tactic:
rw [Quotient.eq] at h
    obtain ⟨j, h1, _, h3⟩ := h
    exact (f i j h1).injective h3

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
x y : DirectLimit G f
xy : (g (Quotient.out x).fst) (Quotient.out x).snd = (g (Quotient.out y).fst) (Quotient.out y).snd
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
⊢ x = y

Tactic:
rw [← Hg x.out.1 i hx, ← Hg y.out.1 i hy] at xy

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
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
xy :
  (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) =
    (g i) ((f (Quotient.out y).fst i hy) (Quotient.out y).snd)
⊢ x = y
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩

Tactic:
rw [Embedding.subtype_equivRange] at ff'2

Goal state after:
case refine_1.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 : (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) = f
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ hs.fract x ∈ hs.fundamentalDomain

Tactic:
classical
  intro i
  constructor
  · rw [hs.toRatVec_fract_eq, add_sub_cancel_left]
    simp [← hs.basis_apply, Finsupp.single_apply]
  · rw [hs.toRatVec_fract_eq, add_sub_cancel_left]
    simp [← hs.basis_apply, Finsupp.single_apply, Int.fract_lt_one]

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

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
⊢ hs.floor (hs.base + y) i = 0

Tactic:
· rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]

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
M_cg : Structure.CG L M
N_cg : Structure.CG L N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
rcases M_cg with ⟨X, X_count, X_gen⟩
  rcases N_cg with ⟨Y, Y_count, Y_gen⟩
  have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
  have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
  have _ : Countable (↑Y : Type _) := by simpa only [countable_coe_iff]
  have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _
  let D : Sum X Y → Order.Cofinal (FGEquiv L M N) := fun p ↦
    Sum.recOn p (fun x ↦ ext_dom.definedAtLeft x) (fun y ↦ ext_cod.definedAtRight y)
  let S : ℕ →o M ≃ₚ[L] N :=
    ⟨Subtype.val ∘ (Order.sequenceOfCofinals g D),
      (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩
  let F := @DirectLimit.partialEquivLimit L M N _ _ ℕ _ _ _ S
  have _ : X ⊆ F.dom := by
    intro x hx
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)
    exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this
  have _ : Y ⊆ F.cod := by
    intro y hy
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inr ⟨y, hy⟩)
    exact cod_le_cod
      (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this
  have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
  have cod_top : F.cod = ⊤ := by rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
  refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩
  convert! le_partialEquivLimit S 0
  rw [toEquivOfEqTop_toEmbedding]
  apply Embedding.toPartialEquiv_toEmbedding

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ 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 →
    ∃ M, Countable ↑M ∧ L.age ↑M = K

Tactic:
rintro ⟨Kn, _, cq, hfg, hp, jep⟩

Goal state after:
case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
Kn : K.Nonempty
left✝ : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
cq : (Quotient.mk' '' K).Countable
hfg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Countable ↑M ∧ L.age ↑M = K
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.preorderTheory

Tactic:
simp only [preorderTheory, Theory.model_insert_iff, Relations.realize_reflexive, relMap_leSymb,
    Theory.model_singleton_iff, Relations.realize_transitive, Matrix.cons_val_zero,
    Matrix.cons_val_one]
  exact ⟨inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
this : ∀ (n : ℕ) (K : PositiveCompacts X), ∃ K', closure ↑K' ⊆ f n ∩ interior ↑K
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U

Tactic:
choose K_next hK_next using this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts X → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure ↑(K_next n K) ⊆ f n ∩ interior ↑K
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ {2, 3}
⊢ Admissible {2, q, r}

Tactic:
fin_cases hq4

Goal state after:
case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n) ((d⁄dX R) f) = Polynomial.derivative ((trunc (n + 1)) f)

Tactic:
ext d
  rw [coeff_trunc]
  split_ifs with h
  · have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
    rw [coeff_derivative, Polynomial.coeff_derivative, coeff_trunc, if_pos this]
  · have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
    rw [Polynomial.coeff_derivative, coeff_trunc, if_neg this, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ

Tactic:
simp_rw [eval_monomial]

Goal state after:
n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ

Tactic:
simp_rw [eval_monomial]
    symm
    rw [← sum_flip _, sum_range_succ]
    simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
      add_tsub_cancel_right]
    apply sum_congr rfl fun x hx => _
    intro x hx
    apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
    · rw [Nat.sub_sub_self (mem_range_le hx)]
    · rw [← choose_symm (mem_range_le hx)]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
| 2 * 512

Tactic:
equals 2 ^ 10 => norm_num1

Goal state after: