mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case a
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‖₊
⊢ (μ.transpose B).variation ≤ C • μ.variation

Tactic:
apply (variation_transpose_le _ _).trans

Goal state after:
case a
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‖₊
⊢ ‖B‖₊ • μ.variation ≤ C • μ.variation
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‖₊
hC : C ≠ 0
this : μ.variation ≤ C⁻¹ • (μ.transpose B).variation
⊢ C • μ.variation ≤ (μ.transpose B).variation

Tactic:
by
      grw [this, smul_smul, mul_inv_cancel₀ hC, one_smul]

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

Goal state before:
pp: case insert
ι : Type u_1
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
hf : μ.Integrable f
a : ι
s : Finset ι
ha : a ∉ s
ih : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
⊢ ∫ᵛ (x : X), f x ∂[B a; μ] + ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] =
    ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]

Tactic:
ih

Goal state after:
case insert
ι : Type u_1
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
hf : μ.Integrable f
a : ι
s : Finset ι
ha : a ∉ s
ih : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
⊢ ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ] =
    ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : t ∈ S
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t

Tactic:
apply hS at ht

Goal state after:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : IsProperLinearSet t
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
⊢ x ∈ ⋃₀ ↑S ↔ x + S.lcm p ∈ ⋃₀ ↑S

Tactic:
· simp only [mem_sUnion, SetLike.mem_coe]
      refine exists_congr fun t => and_congr_right fun ht => ?_
      have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht
      rw [dvd_iff_exists_eq_mul_left] at hpt
      rcases hpt with ⟨m, hpt⟩
      rw [hpt]
      clear hpt
      induction m with grind [Finset.sup_le_iff]

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

Goal state before:
pp: case h
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‖ₑ + ρ)
i : E
hi : i ∈ g.range
⊢ ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤ ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)

Tactic:
exact hP i

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

Goal state before:
pp: case imp
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
this : Fintype α
n✝ : ℕ
f₁✝ f₂✝ : presburger[[↑A]].BoundedFormula α n✝
ih₁ : IsSemilinearSet {v | f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}
ih₂ : IsSemilinearSet {v | f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}
⊢ IsSemilinearSet {v | f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}

Tactic:
| imp _ _ ih₁ ih₂ =>

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ FG L M ↔ ∃ S, S.Finite ∧ (closure L).toFun S = ⊤

Tactic:
rw [fg_def, Substructure.fg_def]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ CG L M

Tactic:
by
  simp only [cg_def, Substructure.cg_of_countable]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ (f' (m + k)) ((natLERec f' m (m + k) ⋯) x) = (f' (m + k)) (Nat.leRecOn ⋯ (fun {k} ↦ ⇑(f' k)) x)

Tactic:
ih

Goal state after:
case succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ (f' (m + k)) (Nat.leRecOn ⋯ (fun k ↦ ⇑(f' k)) x) = (f' (m + k)) (Nat.leRecOn ⋯ (fun {k} ↦ ⇑(f' k)) x)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
⊢ ∀ (g : (ι → ℕ) → ℤ), ↑t ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • toRatVec i = 0 → ∀ i ∈ t, g i = 0

Tactic:
f

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
⊢ ↑t ⊆ s → (∀ i ∉ t, f i = 0) → ∑ i ∈ t, f i • toRatVec i = 0 → ∀ i ∈ t, f i = 0
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:
relMap_equiv_unify G f R (fun a => .mk f i (x a)) i (fun _ ⟨_, hj⟩ => le_of_eq hj.symm)

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 (unify f (fun a ↦ Structure.Sigma.mk f i (x a)) i ⋯) = 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 ι
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
xy : (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) = (g (Quotient.out y).fst) (Quotient.out y).snd
hy : (Quotient.out y).fst ≤ i
⊢ x = y

Tactic:
← Hg y.out.1 i hy

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
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
⊢ ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

Tactic:
f

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
f : L.FGEquiv N M
⊢ ∀ (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
⊢ L.IsExtensionPair M N

Tactic:
f

Goal state after:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
⊢ ∀ (m : M), ∃ g, m ∈ (↑g).dom ∧ f ≤ g
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
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]

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 = ⊤
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) → ⟦N⟧ ∈ Quotient.mk' '' L.age M

Tactic:
rintro ⟨s, hs⟩

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs : (fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) s = ⟦N⟧
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p q : α × β
pf : p ∈ ↑f
qf : q ∈ ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
· exact f.prop _ pf _ qf

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
⊢ ∀ (f : ↥S ↪[L] M), ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
f

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
⊢ ∃ g, f = g.toEmbedding.comp S.subtype
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ((hs.floor x i).toNat - 1 + 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
tsub_add_cancel_of_le ((Int.le_toNat hi'.le).2 (Int.add_one_le_of_lt hi')),

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + (hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
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), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
f

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), ∃ g, f = g.comp (Substructure.inclusion ⋯)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ λ n = n.primeFactors.lcm fun p ↦ λ (p ^ n.factorization p)

Tactic:
nth_rw 1 [← n.prod_factorization_pow_eq_self <| NeZero.ne _]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ λ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n.primeFactors.lcm fun p ↦ λ (p ^ n.factorization p)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(μ m) * (Real.log ↑m - Real.log ↑n) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

Tactic:
mul_sub

Goal state after:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n
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 * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

Tactic:
← sub_mul,

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 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ ¬IsCyclic (ZMod n)ˣ

Tactic:
have := n.ordProj_dvd p
    rw [← Nat.mul_div_cancel' this]
    refine not_isCyclic_units_of_mul_coprime _ _ (hn.of_dvd_nat this) ?_
      (hn.of_dvd_nat (Nat.div_dvd_of_dvd this)) ?_ ((Nat.coprime_ordCompl hp hn0).pow_left ..)
    · simpa [(hp.factorization_pos_of_dvd hn0 dvd).ne'] using hp.ne_one
    · contrapose hnp
      conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul]

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

Goal state before:
pp: case succ
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) f
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)

Tactic:
ih

Goal state after:
case succ
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ * (‖f x‖ₑ⁻¹ * ‖f x‖ₑ) = ‖f x‖ₑ

Tactic:
ENNReal.inv_mul_cancel (by simpa using hx) (by simp),

Goal state after:
case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ * 1 = ‖f x‖ₑ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n

Tactic:
cases hn.lt_or_gt with
  | inl hlt => simp [lt_one_iff.mp hlt]
  | inr hgt =>
    cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

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

Goal state before:
pp: case h
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / ↑|b| < 1

Tactic:
rw [div_lt_one hb', cast_lt]

Goal state after:
case h
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv ((Algebra.norm R) a) ≤ normBound abv bS * y ^ Fintype.card ι

Tactic:
conv_lhs => rw [← bS.sum_repr a]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv ((Algebra.norm R) (∑ i, (bS.repr a) i • bS i)) ≤ normBound abv bS * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ ∃ i_1 j_1,
    i_1 ≠ j_1 ∧
      (distinctElems bS adm) i_1 - (distinctElems bS adm) j_1 =
        (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2

Tactic:
refine ⟨i, j, ?_, rfl⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ i ≠ j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
let a : ℕ → ℝ := Set.indicator (Set.ofPred Nat.Prime) (fun n ↦ 1)

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t

Tactic:
have int_deriv (f : ℝ → ℝ) :
      ∫ u in 2..x, deriv (fun x ↦ log x) u * f u =
      ∫ u in 2..x, f u / u :=
    intervalIntegral.integral_congr fun u _ ↦ by rw [deriv_log, mul_comm, div_eq_mul_inv]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
int_deriv : ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ log x) u * f u = ∫ (u : ℝ) in 2..x, f u / u
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t