mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
h's : (↑t).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, μ.IntegrableOn f (s i)
⊢ ∫ᵛ (x : X) in ⋃ i ∈ t, s i, f x ∂[B; μ] = ∑ i ∈ t, ∫ᵛ (x : X) in s i, f x ∂[B; μ]

Tactic:
induction t using Finset.induction_on with

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, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ

Tactic:
obtain ⟨t, ts, t_meas, ht⟩ : ∃ t ⊆ s, MeasurableSet t ∧ 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ := by
    apply exists_subset_lt_enorm_apply_of_lt_semivariation hs
    rw [h's]
    finiteness

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‖ₑ
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
A : ∀ s ∈ supClosure C, ‖m₀ s‖ₑ ≤ μ s
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ MeasurableSet (P.parts.sup id)

Tactic:
Finset.sup_set_eq_biUnion

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
A : ∀ s ∈ supClosure C, ‖m₀ s‖ₑ ≤ μ s
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ MeasurableSet (⋃ x ∈ P.parts, id x)
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : IsFiniteMeasure μ.variation
s : Set (X × Y)
hs : MeasurableSet s
this : μ.prod ν B = μ.prodOfIsFiniteMeasureLeft ν B
⊢ (μ.prodOfIsFiniteMeasureLeft ν B) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ]

Tactic:
simp [prodOfIsFiniteMeasureLeft, hs]

Goal state after:
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
s : Set X
⊢ (μ.restrict s).transpose B = (μ.transpose B).restrict s

Tactic:
by_cases hs : MeasurableSet s
  · ext t ht : 1
    simp [VectorMeasure.restrict_apply, hs, ht, transpose]
  · simp [restrict_not_measurable _ hs]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
⊢ IsLinearSet (s₁ + s₂)

Tactic:
by
  rcases hs₁ with ⟨a, t₁, ht₁, rfl⟩
  rcases hs₂ with ⟨b, t₂, ht₂, rfl⟩
  exact ⟨a + b, t₁ ∪ t₂, ht₁.union ht₂, by simp [vadd_add_vadd, closure_union, coe_sup]⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ + ⋃₀ S₂)

Tactic:
simp_rw [sUnion_add, add_sUnion]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃ s ∈ S₁, ⋃ t ∈ S₂, s + t)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ ({a} ∪ t).Finite

Tactic:
by simp [ht]

Goal state after:
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
by
  refine setToFun_add_left'' (by simp [transpose]) hB hB ?_
    (norm_nonneg _) (norm_nonneg _) (norm_nonneg _)
  nth_rw 1 [← add_zero μ.variation]
  gcongr
  exact Measure.zero_le μ.variation

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

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Fintype α
t : presburger[[↑A]].Term α
⊢ ∃ k u, ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v

Tactic:
by
  classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

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

Goal state before:
pp: case pos
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
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : ¬AEStronglyMeasurable f (Measure.map φ μ.variation)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
· by_cases h'fm : μ.Integrable (f ∘ φ)
    · apply integral_map hφ.measurable hfm h'fm
    · rw [integral_undef, integral_undef]
      · exact h'fm
      · rwa [hφ.integrable_map_vectorMeasure]

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : ¬AEStronglyMeasurable f (Measure.map φ μ.variation)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs

Tactic:
exact And.right

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
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, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ =
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, i.fst ∂[B; μ.restrict s]‖ₑ

Tactic:
by
      congr! with ⟨i, p⟩ hi
      rcases eq_or_ne i 0 with rfl | h'i
      · simp
      simp only [Finset.mem_sigma] at hi
      have pmeas : MeasurableSet p := Pmeas i _ hi.2
      have : IsFiniteMeasure ((μ.restrict s).variation.restrict p) := by
        constructor
        rw [variation_restrict hs, Measure.restrict_restrict pmeas,
          MeasureTheory.Measure.restrict_apply_univ]
        apply lt_of_le_of_lt ?_ (g.integrable_iff.1 (memLp_one_iff_integrable.1 gmem) i h'i)
        exact measure_mono (inter_subset_left.trans (Pg i _ hi.2))
      rw [setIntegral_const, restrict_apply _ hs pmeas, restrict_apply _ hs pmeas]
      simp [transpose, hB, enorm_eq_nnnorm, mul_comm]

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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
⊢ Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ Structure.Sigma.mk f j (funMap F (unify f x j hj))

Tactic:
obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  refine ⟨k, ik, jk, ?_⟩
  rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, comp_unify]

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 ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
⊢ x a = ⟦Structure.Sigma.mk f i (unify f (Quotient.out ∘ x) i hi a)⟧

Tactic:
rw [Quotient.eq_mk_iff_out, unify]

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 ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f ((Quotient.out ∘ x) a).fst i ⋯) ((Quotient.out ∘ x) a).snd)
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
⊢ (liftInclusion S).toHom.range = ⨆ i, S i

Tactic:
liftInclusion,

Goal state after:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ (lift L ι (fun i ↦ ↥(S i)) (fun x x_1 h ↦ Substructure.inclusion ⋯) (fun x ↦ (S x).subtype) ⋯).toHom.range = ⨆ i, S i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
⊢ ∀ C ∈ Quotient.mk' '' L.age M, ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C

Tactic:
rintro _ ⟨N, ⟨N_fg, ⟨N_incl⟩⟩, N_eq⟩
  refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩
  exact FG.range N_fg (Embedding.toHom N_incl)

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

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

Tactic:
simp only [mem_range, Quotient.eq]

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N
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 : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hxS : x ∈ S
hyS : y ∉ S
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
else

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})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hxS : x ∈ S
hyS : y ∉ S
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩
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 : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hxS : x ∉ S
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
else

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})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hxS : x ∉ S
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩
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 β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | ↑x_1 < x})
Sgt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | x < ↑x_1})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hyS : y ∉ S
⊢ (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨x, hx⟩ <
    (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨y, hy⟩

Tactic:
else

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 β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | ↑x_1 < x})
Sgt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | x < ↑x_1})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hyS : y ∉ S
⊢ (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨x, hx⟩ <
    (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨y, hy⟩
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ¬¬{p | S ⊆ ↑p}.Nonempty

Tactic:
Classical.not_not,

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ {p | S ⊆ ↑p}.Nonempty
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ Pairwise fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
intro p q hpq

Goal state after:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
hpq : p ≠ q
⊢ ∃ U, IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
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 * 1 * ↑(p.choose 0) + ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * 1 * ↑(p.choose x_1) =
      1 + ↑p * u * (x + v * y)

Tactic:
Nat.choose_zero_right,

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,
    1 * 1 * ↑1 + ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * 1 * ↑(p.choose x_1) = 1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ Λ (n ^ k) = Λ n

Tactic:
simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
f g : MvPowerSeries σ R
⊢ pderivFun i (f + g) = pderivFun i f + pderivFun i g

Tactic:
by
  ext
  rw [coeff_pderivFun, map_add, map_add, coeff_pderivFun, coeff_pderivFun, add_mul]

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ

Tactic:
have : Nat.Coprime 4 n := (Nat.prime_two.coprime_iff_not_dvd.mpr h2n).pow_left 2

Goal state after:
case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ

Tactic:
let e := (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans .prodUnits

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
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ ¬IsCyclic (ZMod (m * n))ˣ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case hf
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‖ₑ)
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖⁻¹ • f x) (μ.withDensity fun x ↦ ‖f x‖ₑ)

pp: case hfC
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‖ₑ)
⊢ ∀ᵐ (x : X) ∂μ.withDensity fun x ↦ ‖f x‖ₑ, ‖‖f x‖⁻¹ • f x‖ ≤ 1

Tactic:
· apply AEStronglyMeasurable.mono_ac (withDensity_absolutelyContinuous _ _)
      exact hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable

Goal state after:
case hfC
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‖ₑ)
⊢ ∀ᵐ (x : X) ∂μ.withDensity fun x ↦ ‖f x‖ₑ, ‖‖f x‖⁻¹ • f x‖ ≤ 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
isCyclic_units_two_mul_iff_of_odd _ hn,

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ _root_.bernoulli n * ↑(n.choose 0) = _root_.bernoulli n

Tactic:
Nat.choose_zero_right,

Goal state after:
n : ℕ
⊢ _root_.bernoulli n * ↑1 = _root_.bernoulli n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
⊢ ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1)

Tactic:
hne'

Goal state after:
case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
hne' : ¬(p = 2 ∧ n = 2)
⊢ n + 1 ≤ p ^ (n - 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hy : 2 ≤ x
⊢ 0 < θ x

Tactic:
refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩
  · simp only [mem_filter] at hn; exact_mod_cast hn.2.one_lt
  · have : 0 ≤ x := by grind
    simpa using ⟨(le_floor_iff this).2 hy, prime_two⟩

Goal state after: