mathlib-initiative/mathlib-tactics huggingface dataset:
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 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
⊢ ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s + ↑ε

Tactic:
have I2 : ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
      ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) := calc
    _ = (g.map (‖·‖ₑ)).lintegral ((μ.transpose B).variation.restrict s) :=
      SimpleFunc.lintegral_eq_lintegral _ _
    _ = ∑ i ∈ g.range, ‖i‖ₑ * (μ.transpose B).variation.restrict s (g ⁻¹' {i}) :=
      SimpleFunc.map_lintegral _ _
    _ = ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) := by
      simp_rw [variation_restrict hs]

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 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
⊢ ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s + ↑ε
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
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂μ.variation

Tactic:
apply (enorm_setToFun_le _ (by simp)).trans
  gcongr
  simp [← coe_nnnorm]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
⊢ (∀ (x_1 : α), x x_1 = (v + ∑ x ∈ t.attach, ↑x * ↑(a x)) x_1) ↔ ∀ (b : α), x b = v b + ∑ i ∈ t.attach, ↑i b * a i

Tactic:
congr! 1 with i

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
i : α
⊢ x i = (v + ∑ x ∈ t.attach, ↑x * ↑(a x)) i ↔ x i = v i + ∑ i_1 ∈ t.attach, ↑i_1 i * a i_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
⊢ w ∈ ↑(f (a + x + u))

Tactic:
rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]

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

Goal state before:
pp: case a.inr
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 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
i : E
p : Set X
h'i : i ≠ 0
hi : i ∈ g.range ∧ p ∈ P i
pmeas : MeasurableSet p
this : IsFiniteMeasure ((μ.restrict s).variation.restrict p)
⊢ ‖⟨i, p⟩.fst‖ₑ * ‖(μ.transpose B) (p ∩ s)‖ₑ = ‖(B ⟨i, p⟩.fst) (μ (p ∩ s))‖ₑ

Tactic:
simp [transpose, hB, enorm_eq_nnnorm, mul_comm]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ ⦃φ_1 : L.Sentence⦄, φ_1 ∈ Insert.insert φ T → BoundedFormula.IsUniversal φ_1

Tactic:
simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]

Goal state after:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ a ∈ T, BoundedFormula.IsUniversal a
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
hy : y ∈ closure hs.basisSet
⊢ hs.floor x i ≤ hs.floor (x + y) i

Tactic:
classical
  simp only [floor]
  apply Int.floor_le_floor
  simp_rw [map_add, add_sub_right_comm, map_add, Finsupp.add_apply, le_add_iff_nonneg_right]
  rw [mem_closure_iff_of_fintype] at hy
  rcases hy with ⟨f, rfl⟩
  simp_rw [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply]
  apply Finset.sum_nonneg
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply, ite_nonneg]

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
⊢ ⨆ i, Substructure.map (lift L ι G f g Hg).toHom (Substructure.map (of L ι G f i).toHom ⊤) =
    ⨆ i, Substructure.map (g i).toHom ⊤

Tactic:
Substructure.map_map

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
⊢ ⨆ i, Substructure.map ((lift L ι G f g Hg).toHom.comp (of L ι G f i).toHom) ⊤ = ⨆ i, Substructure.map (g i).toHom ⊤
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Tactic:
let Slt := {x ∈ S.attach | x.val < a}.image f

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
⊢ ∃ f', f = f'.comp g

Tactic:
by
  let ⟨r⟩ := h
  let s := r.comp g
  let ⟨t, eq⟩ := M_homog s.toHom.range (S_FG.range s.toHom) (f.comp s.equivRange.symm.toEmbedding)
  use t.toEmbedding.comp r
  change _ = t.toEmbedding.comp s
  ext x
  have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩
  simp only [Embedding.comp_apply,
    coe_subtype] at eq'
  simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]
  apply (Embedding.equivRange (Embedding.comp r g)).injective
  ext
  simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
⊢ Nonempty (α ≃o β)

Tactic:
let G b := invOfIdeal b our_ideal (cofinal_meets_idealOfCofinals _ to_cofinal (Sum.inr b))

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b ↦ invOfIdeal b our_ideal ⋯
⊢ Nonempty (α ≃o β)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoTopOrder M
⊢ ∀ (a : M),
    ∃ a_1,
      ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)

Tactic:
a

Goal state after:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoTopOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoBotOrder M
⊢ ∀ (a : M),
    ∃ a_1,
      ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)

Tactic:
a

Goal state after:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoBotOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
⊢ ∀ (a a_1 : M),
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
      ∃ a_3,
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)

Tactic:
a

Goal state after:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a : M
⊢ ∀ (a_1 : M),
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
      ∃ a_3,
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝¹ : LinearOrder M := Language.order.linearOrderOfModels M
this✝ : LinearOrder N := Language.order.linearOrderOfModels N
this : DenselyOrdered N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := Language.order.noBotOrder_of_dlo N

Goal state after:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝² : LinearOrder M := Language.order.linearOrderOfModels M
this✝¹ : LinearOrder N := Language.order.linearOrderOfModels N
this✝ : DenselyOrdered N
this : NoBotOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)
Module: Mathlib.ModelTheory.Order

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

Tactic:
exact (isFraisseLimit_of_countable_nonempty_dlo M₁).nonempty_equiv
    (isFraisseLimit_of_countable_nonempty_dlo M₂)

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this : Finite ↥S
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype

Goal state after:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝ : Finite ↥S
this : Infinite { x // x ∉ S }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ ⋃₀ range T.typesWith = univ

Tactic:
rw [← Set.univ_subset_iff]
    exact Set.subset_sUnion_of_mem ⟨_, typesWith_top⟩

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3

Tactic:
contrapose! H

Goal state after:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ sumInv {p, q, r} ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4

Tactic:
contrapose! H

Goal state after:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6

Tactic:
contrapose! H

Goal state after:
r : ℕ+
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ (p ≠ 1 ∧ p ≠ 0) ∧ p ∈ Finset.range (p + 1)

Tactic:
and_comm (a := ¬ _),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ (p ≠ 0 ∧ ¬p = 1) ∧ p ∈ Finset.range (p + 1)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k

Tactic:
sub_self

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ 0 = 0
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ

Tactic:
have _ : NeZero n := ⟨Nat.ne_of_odd_add hn⟩

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
⊢ ¬IsCyclic (ZMod (m * n))ˣ
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A * evalNegHom (exp A) = 1

Tactic:
by
  convert! exp_mul_exp_eq_exp_add (1 : A) (-1) <;> simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ bernoulli 0 = 1

Tactic:
by simp [bernoulli]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (↑n + 1) • bernoulli n = (monomial n) (↑n + 1) - ∑ x ∈ range n, ↑((n + 1).choose x) • bernoulli x

Tactic:
← sum_bernoulli n,

Goal state after:
n : ℕ
⊢ (↑n + 1) • bernoulli n =
    ∑ k ∈ range (n + 1), ↑((n + 1).choose k) • bernoulli k - ∑ x ∈ range n, ↑((n + 1).choose x) • bernoulli x
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ ↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x = 0

Tactic:
sub_self

Goal state after:
n x : ℕ
hx : x ∈ range n
⊢ 0 = 0
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
this : ∏ p ∈ n.primeFactors, p ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#

Tactic:
rwa [Nat.prod_primeFactors_of_squarefree hn] at this

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : b < 1
⊢ 0 = 0 - 0

Tactic:
sub_self

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli 0 = 1

Tactic:
by simp [bernoulli]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h₂.refine_1
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
⊢ f p ≤ p

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
      refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le
      exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2.inl
n p : ℕ
hp : Prime p
this✝ : 1 < p
h✝ : p ≤ n
this : p ^ log p n ≤ n
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

Tactic:
grw [← le_sup (b := p ^ p.log n) (by grind)]

Goal state after:
case refine_2.inl
n p : ℕ
hp : Prime p
this✝ : 1 < p
h✝ : p ≤ n
this : p ^ log p n ≤ n
⊢ log p n ≤ (id (p ^ log p n)).factorization p
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a₁ : ℕ × ℕ)
    (ha₁ :
      a₁ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊})
    (a₂ : ℕ × ℕ)
    (ha₂ :
      a₂ ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    ((match a₁, ha₁ with
        | (k, p), x => p ^ k) =
        match a₂, ha₂ with
        | (k, p), x => p ^ k) →
      a₁ = a₂

Tactic:
simp +contextual only [hx, rpow_nonneg, le_floor_iff, mem_filter, mem_product, mem_Icc,
        one_le_iff_ne_zero, pos_iff_ne_zero, mem_Ioc, and_imp, Prod.forall, Prod.mk.injEq]

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a b : ℕ),
    a ≠ 0 →
      a ≤ N →
        b ≠ 0 →
          ↑b ≤ x →
            Nat.Prime b →
              ↑b ≤ x ^ (↑a)⁻¹ →
                ∀ (a_7 b_1 : ℕ),
                  a_7 ≠ 0 →
                    a_7 ≤ N →
                      b_1 ≠ 0 → ↑b_1 ≤ x → Nat.Prime b_1 → ↑b_1 ≤ x ^ (↑a_7)⁻¹ → b ^ a = b_1 ^ a_7 → a = a_7 ∧ b = b_1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ cardPowDegree (x - z) < a

Tactic:
← hyz'

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ cardPowDegree (x - y) < a