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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < ‖μ t‖ₑ + ‖μ t‖ₑ

Tactic:
rcases le_total (‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ)
    (‖μ (⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p)‖ₑ) with h | h

Goal state after:
case inl
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
h : ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ ≤ ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < ‖μ t‖ₑ + ‖μ t‖ₑ

case inr
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
h : ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ ≤ ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < ‖μ t‖ₑ + ‖μ t‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
ht : MeasurableSet t
hf : AEStronglyMeasurable f (μ.variation.restrict t)
this : ∫ᵛ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂[B; μ] = 0
⊢ f =ᵐ[μ.variation.restrict t] AEStronglyMeasurable.mk f hf

Tactic:
exact hf.ae_eq_mk

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 * 1 + 2 * ‖μ s‖ₑ ≤ 2 * ‖μ t‖ₑ

Tactic:
add_comm,

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 * ‖μ s‖ₑ + 2 * 1 ≤ 2 * ‖μ t‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ μ.semivariation s ≤ ↑μ.bound

Tactic:
apply (semivariation_mono (subset_univ _)).trans_eq

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ μ.semivariation univ = ↑μ.bound
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s

Tactic:
by
  by_cases hs : MeasurableSet s; swap
  · simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero]
    by_cases h's : μ.variation s = 0
    · simp [Measure.real, h's]
    · have : NeBot (ae (μ.variation.restrict s)) := by simpa using h's
      obtain ⟨x, hx⟩ : ∃ x, ‖f x‖ ≤ C := hC.exists
      have : 0 ≤ C := le_trans (norm_nonneg _) hx
      positivity
  rw [← variation_restrict hs] at hC h
  apply (norm_integral_le_of_norm_le_const hC).trans_eq
  simp [variation_restrict hs]

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

Goal state before:
pp: case neg
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
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ.variation
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
rw [integral_non_aestronglyMeasurable h, norm_zero]

Goal state after:
case neg
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
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ.variation
⊢ 0 ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation
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})
⊢ (∑ i ∈ g.range, ‖i‖ₑ) * (∑ i ∈ g.range, ‖i‖ₑ)⁻¹ * ↑δ ≤ ↑δ

Tactic:
ENNReal.mul_inv_le_one,

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})
⊢ 1 * ↑δ ≤ ↑δ
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
t : Set ℕ
ht : t ∈ S
⊢ x ∈ t ↔ x + S.lcm p ∈ t

Tactic:
have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht

Goal state after:
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
t : Set ℕ
ht : t ∈ S
hpt : p t ∣ S.lcm p
⊢ x ∈ t ↔ x + S.lcm p ∈ t
Module: Mathlib.ModelTheory.FinitelyGenerated

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

Tactic:
have h := h.map S.subtype.toHom

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

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.CG
⊢ S.CG

Tactic:
have h := h.map S.subtype.toHom

Goal state after:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.CG
h : (map S.subtype.toHom ⊤).CG
⊢ S.CG
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ

Tactic:
refine fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ (⇑f ∘ default) (⇑f ∘ default)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ default default

Tactic:
exact Theory.realize_sentence_of_mem T hφ

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddMonoid.FG M
inst✝ : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ IsSemilinearSet (⋂ i, s i)

Tactic:
rw [← sInter_range]

Goal state after:
M : Type u_1
ι : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddMonoid.FG M
inst✝ : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ IsSemilinearSet (⋂₀ range s)
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:
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.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
⊢ (lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range

Tactic:
simp_rw [Hom.range_eq_map]
  rw [← iSup_range_of_eq_top, Substructure.map_iSup]
  simp_rw [Hom.range_eq_map, Substructure.map_map]
  rfl

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ T.IsSatisfiable

Tactic:
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
  rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm,
    ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOfPred_subset_eq_empty_iff]
  simp

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p

Tactic:
simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff,
    Sentence.Realize, Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]

Goal state after:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ (∀ (M : ModelType ↑p), ∀ φ ∈ t, φ.Realize default default) ↔
    ∀ x ∈ ↑t, ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
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
⊢ ∃ y, (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)

Tactic:
add_comm,

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
⊢ ∃ y, (u * x + 1) ^ p = 1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case succ
n : ℕ
hn : n + 1 ≠ 0
⊢ λ (n + 1) = exponent (ZMod (n + 1))ˣ

Tactic:
change Nat.find _ = _
  grind [exponent, ExponentExists.of_finite]

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

Goal state before:
pp: case succ
n✝ : ℕ
a : (ZMod (n✝ + 1))ˣ
⊢ a ^ λ (n✝ + 1) = 1

Tactic:
rw [carmichael_eq_exponent']

Goal state after:
case succ
n✝ : ℕ
a : (ZMod (n✝ + 1))ˣ
⊢ a ^ exponent (ZMod (n✝ + 1))ˣ = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

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

Tactic:
· let five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 <| gcd_pow_right_of_gcd_eq_one rfl
    rw [← ZMod.orderOf_five (n - 2), show n - 2 + 2 = n by lia,
      show (5 : ZMod (2 ^ n)) = five by rfl, orderOf_units]
    exact order_dvd_exponent five

Goal state after:
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
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ∑ i ∈ Finset.range p, f (a ^ p ^ k) ^ i * f (b ^ p ^ k) ^ (p - 1 - i) = 0

Tactic:
map_pow,

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
⊢ ∑ i ∈ Finset.range p, (f a ^ p ^ k) ^ i * f (b ^ p ^ k) ^ (p - 1 - i) = 0
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
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ∑ i ∈ Finset.range p, (f a ^ p ^ k) ^ i * f (b ^ p ^ k) ^ (p - 1 - i) = 0

Tactic:
map_pow,

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
⊢ ∑ i ∈ Finset.range p, (f a ^ p ^ k) ^ i * (f b ^ p ^ k) ^ (p - 1 - i) = 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1

Tactic:
intro H

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : ↑p ∣ 1
⊢ False
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
⊢ IsUnit (↑1 + ↑p)

Tactic:
← Nat.cast_add,

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
⊢ IsUnit ↑(1 + p)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑((pderiv i) f * g + f * (pderiv i) g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
add_comm,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(f * (pderiv i) g + (pderiv i) f * g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n✝ n : ℕ
⊢ ¬IsCyclic (ZMod (2 ^ (n + 3)))ˣ

Tactic:
intro H

Goal state after:
n✝ n : ℕ
H : IsCyclic (ZMod (2 ^ (n + 3)))ˣ
⊢ False
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
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : m = 2 ∨ n = 2
⊢ False

Tactic:
rcases h with (rfl | rfl)

Goal state after:
case inl
n : ℕ
hn : Odd n
hn1 : n ≠ 1
x✝¹ : NeZero n
hm : Odd 2
hm1 : 2 ≠ 1
hmn : Nat.Coprime 2 n
x✝ : NeZero 2
e : (ZMod (2 * n))ˣ ≃* (ZMod 2)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

case inr
m : ℕ
hm : Odd m
hm1 : m ≠ 1
x✝¹ : NeZero m
hn : Odd 2
hn1 : 2 ≠ 1
hmn : m.Coprime 2
x✝ : NeZero 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + ↑1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))

Tactic:
← Nat.cast_add,

Goal state after:
k m : ℕ
x✝ : m ∈ range (k + 1)
| ↑(k + 1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose x)

Tactic:
· rw [← choose_symm (mem_range_le hx)]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hg.hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x ↦ x

Tactic:
exact convexOn_id (convex_Ioi (0.5 : ℝ))

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n q : ℕ
hq : ∃ a, ((1 ≤ a ∧ a ≤ n) ∧ Nat.Prime a) ∧ ∃ a_1, (1 ≤ a_1 ∧ a_1 ≤ Nat.log a n) ∧ a ^ a_1 = q
⊢ 1 ≤ q ∧ q ≤ n

Tactic:
obtain ⟨p, _, k, ⟨_, hk⟩, rfl⟩ := hq

Goal state after:
case refine_1
n p : ℕ
left✝¹ : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left✝ : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ 1 ≤ p ^ k ∧ p ^ k ≤ n
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
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
hxz' : ¬x = z
⊢ cardPowDegree (x - z) < a

Tactic:
rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'

Goal state after:
case neg
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 ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ cardPowDegree (x - z) < a
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p : R[X][Y]
⊢ (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) p) = (aeval y) ((Transcendental.algEquivAdjoin hx) p)

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp_all [map_add]
  | monomial n a =>
    simp_all [aeval_algebraMap_apply, Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def]

Goal state after:
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
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)

Tactic:
obtain ⟨q, r, hr, hqr⟩ := exists_mem_finsetApprox bS adm a' hb'

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
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ (↑n).zmodRepr = n

Tactic:
zmodRepr_natCast (p := p) n,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ n % p = n
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val -
      x.appr m

Tactic:
add_comm,

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val +
        x.appr (m + k) -
      x.appr m
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / (log x / 2) ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
add_comm,

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (x - √x) / (log x / 2) ^ 2 + (√x - 2) / log 2 ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2