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 + ↑δ
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 ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, g x - f x + f x ∂[B; μ.restrict s]‖ₑ =
    ∑ i ∈ g.range.sigma P,
      ‖∫ᵛ (x : X) in i.snd, g x - f x ∂[B; μ.restrict s] + ∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ

Tactic:
by
      congr! with i hi
      rw [integral_fun_add]
      · apply Integrable.restrict
        apply Integrable.restrict
        apply Integrable.sub (memLp_one_iff_integrable.1 gmem) hf
      · apply hf.restrict.restrict

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
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩

Goal state after:
case refine_1
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
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
| Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
rw [Int.fract_eq_self.2 (hx i), ← hs.basis_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
| (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ x ∈ s ↔ hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)

Tactic:
hs.eq_base_vadd_closure_periods

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ x ∈ hs.base +ᵥ ↑(closure hs.periods) ↔
    hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)

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

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
⊢ hs.base + ∑ i with ↑i ∈ hs.periods, (hs.floor x i).toNat • ↑i = x

Tactic:
rw [Finset.sum_filter, ← hx₁]

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
⊢ (hs.fract x + ∑ a, if ↑a ∈ hs.periods then (hs.floor x a).toNat • ↑a else 0) = x
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ (Substructure.closure L).toFun (⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯) = ⊤

Tactic:
· rw [eq_top_iff, Substructure.closure_iUnion]
    simp_rw [← Embedding.coe_toHom, Substructure.closure_image]
    rw [le_iSup_iff]
    intro S hS x _
    let out := Quotient.out (s := DirectLimit.setoid G f)
    refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩
    · rw [(Classical.choose_spec (h (out x).1).out).2]
      trivial
    · simp only [out, Embedding.coe_toHom, DirectLimit.of_apply, Sigma.eta, Quotient.out_eq]

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
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ ↑g ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ ((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x =
    (of L ι (fun x ↦ ↥(S x)) (fun x x_1 h ↦ Substructure.inclusion ⋯) i) x

Tactic:
exact Equiv_isup_symm_inclusion_apply _ x

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y

Tactic:
intro x hx y hy

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
x : β
hx : x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a})
y : β
hy : y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1})
⊢ x < y
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_1
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 ⋯
⊢ Structure.CG L ↑(Bundled.of (DirectLimit (fun n ↦ ↑↑(G n)) f))

pp: case refine_2
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 ⋯
⊢ L.age ↑(Bundled.of (DirectLimit (fun n ↦ ↑↑(G n)) f)) = K

Tactic:
· exact DirectLimit.cg _ (fun n => (fg _ (G n).2).cg)

Goal state after:
case refine_2
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 ⋯
⊢ L.age ↑(Bundled.of (DirectLimit (fun n ↦ ↑↑(G n)) f)) = K
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑f ⊆ Finset.image ⇑(Equiv.prodComm β α) ↑f'

Tactic:
← Finset.coe_subset,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑↑f ⊆ ↑(Finset.image ⇑(Equiv.prodComm β α) ↑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
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ ∃ f', f = f'.comp g

Tactic:
use t.toEmbedding.comp r

Goal state after:
case h
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
r : T ↪[L] M
s : S ↪[L] M := ⋯
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ f = (t.toEmbedding.comp r).comp g
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := ⋯
n : ↑N
⊢ ↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) =
    ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)

Tactic:
have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange n)

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn :
  ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding) ((PM.comp NP).equivRange n) =
    (g.toEmbedding.comp (PM.comp NP).toHom.range.subtype) ((PM.comp NP).equivRange n)
⊢ ↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) =
    ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
· refine ⟨mem_univ _, ?_⟩
    · rw [nhds_generateFrom]
      apply le_iInf₂
      rintro _ ⟨hφ, φ, rfl⟩
      rw [Filter.le_principal_iff]
      exact hφ

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ ↑(⌊a⌋₊ + 1) ≤ b

Tactic:
← Nat.le_floor_iff aux1

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ ⌊a⌋₊ + 1 ≤ ⌊b⌋₊
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a - f b = 0
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)

Tactic:
sub_eq_zero

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = (if m✝ + single i 1 < n + single i 1 then (coeff (m✝ + single i 1)) f else 0) * (↑(m✝ i) + 1)

Tactic:
if_neg ((add_lt_add_iff_right _).not.mpr h),

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = 0 * (↑(m✝ i) + 1)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = 0 * (↑(m✝ i) + 1)

Tactic:
zero_mul

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ 0 = 0 * (↑d + 1)

Tactic:
zero_mul

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ (trunc (0 - 1)) ((d⁄dX R) f) = Polynomial.derivative ((trunc 0) f)

Tactic:
simp [trunc_derivative]

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

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

Tactic:
simp [trunc_derivative]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ! * (n - x)! ∣ n !

Tactic:
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _)]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ cons 0 (Ioc 0 ⌊b⌋₊) ⋯, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
conv_lhs =>
    apply_congr
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]

Goal state after:
n : ℕ
⊢ ∑ x ∈ range (n + 1 - 0),
      ∑ x_1 ∈ range (n + 1 - x), (↑((n + 1 - x).choose x_1) * _root_.bernoulli x_1) • (monomial x) ↑((n + 1).choose x) =
    (monomial n) ↑n + (monomial n) 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
smul_X_eq_monomial,

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

Goal state before:
pp: case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
⊢ ((d + 2).choose x✝ • bernoulli x✝).comp (1 + X) = ?a.g x✝

Tactic:
rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Goal state after:
case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
| (d + 2).choose x✝ • (bernoulli x✝ + x✝ • X ^ (x✝ - 1))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) - ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (1 + X) =
    (d + 2) • X ^ (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1)

Tactic:
conv_lhs =>
    congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) - ∑ x ∈ range (d + 1), (d + 2).choose x • (bernoulli x + x • X ^ (x - 1)) =
    (d + 2) • X ^ (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: p n : ℕ
hp : Prime p
q : ℕ
hpq : p ∣ q
hqn : q ≤ n
hq : Prime q
⊢ p ≤ n

Tactic:
exact (Nat.le_of_dvd hq.pos hpq).trans hqn

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
add_right_comm

Goal state after:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + 1 + m)# = (m + 1 + m)#
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (m + m + 1).choose m

Tactic:
add_right_comm

Goal state after:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + 1)# * (m + m + 1).choose m = (m + 1)# * (m + m + 1).choose m
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ 4 ^ (m + 1 + m) ≤ 4 ^ (m + m + 1)

Tactic:
add_right_comm

Goal state after:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ 4 ^ (m + m + 1) ≤ 4 ^ (m + m + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli n = 0

Tactic:
by
  rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < b.degree
⊢ (A i₁).coeff j - (A i₀).coeff j = 0

Tactic:
sub_eq_zero

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j