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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
⊢ HasSum (fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G; swap
  · simp [integral_of_not_completeSpace hG]
  have I : ∑' i, ‖B‖ₑ * ∫⁻ x in s i, ‖f x‖ₑ ∂μ.variation < ∞ := calc
    ∑' i, ‖B‖ₑ * ∫⁻ x in s i, ‖f x‖ₑ ∂μ.variation
    _ = ‖B‖ₑ * ∫⁻ x in (⋃ i, s i), ‖f x‖ₑ ∂μ.variation := by
      rw [ENNReal.tsum_mul_left, lintegral_iUnion hm hd]
    _ < ∞ := by
      simp only [VectorMeasure.IntegrableOn, VectorMeasure.Integrable,
        variation_restrict (MeasurableSet.iUnion hm)] at hfi
      exact ENNReal.mul_lt_top (by simp) hfi.2
  have : Summable (fun n ↦ ∫ᵛ x in s n, f x ∂[B; μ]) := by
    apply Summable.of_enorm (lt_of_le_of_lt _ I).ne
    gcongr
    exact enorm_setIntegral_le_lintegral_enorm
  apply (Summable.hasSum_iff_tendsto_nat this).2
  simp_rw [tendsto_iff_edist_tendsto_0, edist_eq_enorm_sub, enorm_sub_rev]
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (ENNReal.tendsto_sum_nat_add _ I.ne) (by positivity) (fun N ↦ ?_)
  have : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ (⋃ n, s (n + N)) := by
    ext x
    have : (∃ i, x ∈ s (i + N)) ↔ (∃ i ≥ N, x ∈ s i) :=
      ⟨fun ⟨i, hi⟩ ↦ ⟨i + N, by grind⟩, fun ⟨i, hi, h'i⟩ ↦ ⟨i - N, by grind⟩⟩
    simp only [mem_iUnion, Finset.mem_range, mem_union, exists_prop, this, ge_iff_le]
    grind
  rw [this, setIntegral_union]; rotate_left
  · simp only [Finset.mem_range, disjoint_iUnion_right, disjoint_iUnion_left]
    intro i j hi
    apply hd (by grind)
  · apply MeasurableSet.biUnion (Finset.countable_toSet _) (fun i hi ↦ hm i)
  · apply MeasurableSet.iUnion (fun i ↦ hm _)
  · apply hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s])
  · apply hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s])
  rw [setIntegral_biUnion_finset]; rotate_left
  · exact fun i hi ↦ hm i
  · exact fun i hi j hj hij ↦ hd hij
  · exact fun i hi ↦ hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s])
  simp only [add_sub_cancel_left]
  apply enorm_setIntegral_le_lintegral_enorm.trans_eq
  rw [lintegral_iUnion (fun i ↦ hm _), ENNReal.tsum_mul_left]
  exact fun i j hij ↦ hd (by grind)

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
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

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
hf : ¬μ.Integrable f
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

Tactic:
· rw [integral_eq_setToFun_transpose hf]
    apply (enorm_setToFun_le _ (by simp)).trans (by simp)

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
hf : ¬μ.Integrable f
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst✝ : Finite α
hs : IsSemilinearSet s
⊢ A.Definable presburger s

Tactic:
by
  rw [isSemilinearSet_iff] at hs
  rcases hs with ⟨S, hS, rfl⟩
  choose φ hφ using fun s : S => (hS s.1 s.2).definable
  refine ⟨Formula.iSup φ, ?_⟩
  ext x
  have := fun s hs x => Set.ext_iff.1 (hφ ⟨s, hs⟩).symm x
  simp only [mem_ofPred_eq] at this
  simp [this]

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
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
⊢ ((μ.map φ).transpose B).variation = Measure.map φ (μ.transpose B).variation

Tactic:
by
  rw [transpose_map, hφ.variation_map]

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)
h'fm : μ.Integrable (f ∘ φ)
⊢ ∫ᵛ (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)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
· apply integral_map hφ.measurable hfm h'fm

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)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
⊢ (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs

Tactic:
by
  induction hψ with
  | of_isQF hψ => rw [hψ.toPrenexImpRight]
  | all _ ih =>
    refine _root_.trans (forall_congr' fun _ => ih hφ.liftAt) ?_
    simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
    exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
  | ex _ ih =>
    unfold toPrenexImpRight
    rw [realize_ex]
    refine _root_.trans (exists_congr fun _ => ih hφ.liftAt) ?_
    simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_ex]
    refine ⟨?_, fun h' => ?_⟩
    · rintro ⟨a, ha⟩ h
      exact ⟨a, ha h⟩
    · by_cases h : φ.Realize v xs
      · obtain ⟨a, ha⟩ := h' h
        exact ⟨a, fun _ => ha⟩
      · inhabit M
        exact ⟨default, fun h'' => (h h'').elim⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
⊢ Countable (M →[L] N)

Tactic:
have g_inj : Function.Injective g := by
    intro f f' h
    apply Hom.eq_of_eqOn_dense closure_S
    intro x x_in_S
    exact congr_fun h ⟨x, x_in_S⟩

Goal state after:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
g_inj : Function.Injective g
⊢ Countable (M →[L] N)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ ↑(AddMonoidHom.mrange f)
⊢ s = a +ᵥ ↑(AddMonoidHom.mrange f)

Tactic:
· rw [hs]

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

Goal state before:
pp: case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₁')

Tactic:
apply Nat.isSemilinearSet_preimage

Goal state after:
case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₁'
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₂')

Tactic:
apply Nat.isSemilinearSet_preimage

Goal state after:
case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₂'
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g h : M ≃ₚ[L] N
⊢ f ≤ g → g ≤ h → f ≤ h

Tactic:
rintro ⟨le_fg, eq_fg⟩ ⟨le_gh, eq_gh⟩

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ f ≤ h
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.fract (hs.base + y) = hs.base

Tactic:
hs.fract_add_of_mem_closure,

Goal state after:
case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.fract hs.base = hs.base

case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ y ∈ closure hs.basisSet
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:
nth_rw 1 [hs.eq_base_vadd_closure_periods]
  simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
  constructor
  · rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
  · intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]

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 : ι → ℕ
⊢ (∃ i ∈ hs.fundamentalDomain \ {hs.base}, ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = i + y) →
    hs.fract x ≠ hs.base

Tactic:
rintro ⟨u, ⟨hu, hu'⟩, y, hy, y', hy', heq⟩
      apply congr_arg hs.fract at heq
      rw [hs.fract_add_of_mem_closure hy', hs.fract_add_of_mem_closure hy,
        hs.fract_eq_self_of_mem_fundamentalDomain hu] at heq
      rwa [heq]

Goal state after:
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs ↔ RelMap graphRel.adj xs

Tactic:
| =>

Goal state after:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs ↔ RelMap graphRel.adj xs
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h.inr
α : 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
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : a < p1
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
· have : a < p1 ∧ b < p2 :=
      ⟨hr, hb.2 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hr⟩, rfl⟩)⟩
    rw [← cmp_eq_gt_iff, ← cmp_eq_gt_iff] at this
    exact this.1.trans this.2.symm

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

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

Tactic:
by
      rcases (F a).prop with ⟨f, hf, ha⟩
      rcases (G b).prop with ⟨g, hg, hb⟩
      rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
      exact m.prop (a, _) (fm ha) (_, b) (gm hb)

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M

Tactic:
constructor
  · intro M_homog ⟨f, f_FG⟩ m
    let S := f.dom ⊔ closure L {m}
    have dom_le_S : f.dom ≤ S := le_sup_left
    let ⟨f', eq_f'⟩ := M_homog.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG)
      ((subtype _).comp f.toEquiv.toEmbedding) (inclusion dom_le_S) (h := ⟨subtype _⟩)
    refine ⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
      subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩
    ext
    simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, coe_subtype, eq_f',
      Embedding.equivRange_apply, Substructure.coe_inclusion]
  · intro h S S_FG f
    let ⟨g, ⟨dom_le_dom, eq⟩⟩ :=
      equiv_between_cg M_CG M_CG ⟨⟨S, f.toHom.range, f.equivRange⟩, S_FG⟩ h h
    use g
    simp only [Embedding.subtype_equivRange] at eq
    rw [← eq]
    ext
    rfl

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

Goal state before:
pp: a b : ℕ
⊢ λ (a.lcm b) = (λ a).lcm (λ b)

Tactic:
by
  by_cases! h₀ : a = 0 ∨ b = 0
  · grind [Nat.lcm_eq_zero_iff, map_zero]
  apply dvd_antisymm
  · rw [carmichael_eq_exponent h₀.left, carmichael_eq_exponent h₀.right,
      carmichael_eq_exponent <| lcm_ne_zero h₀.left h₀.right, ← lcm_eq_nat_lcm <| exponent _,
      ← exponent_prod, ← exponent_eq_of_mulEquiv .prodUnits]
    exact exponent_dvd_of_monoidHom _ <| Units.map_injective <| ZMod.castHom_injective _
  · have ha := carmichael_dvd <| Nat.dvd_lcm_left a b
    have hb := carmichael_dvd <| Nat.dvd_lcm_right a b
    exact Nat.lcm_dvd ha hb

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

Goal state before:
pp: ⊢ liouville 1 = 1

Tactic:
simp [liouville_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
⊢ ∃ y, ((1 + u * x) ^ p) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y)

Tactic:
obtain ⟨y, hy⟩ := exists_one_add_mul_pow_prime_eq hp hvu hpuv x

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ∃ y, ((1 + u * x) ^ p) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ 0

Tactic:
| =>

Goal state after:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ (n + 1)

Tactic:
| =>

Goal state after:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ (n + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∀ i ∈ (n + 1).divisors, 0 ≤ Λ i

Tactic:
by exact fun _ _ => vonMangoldt_nonneg

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

Goal state before:
pp: case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑↑(p ^ (n + m)) * ↑a = 0

Tactic:
← Int.cast_mul,

Goal state after:
case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(↑(p ^ (n + m)) * a) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : m✝ < n
⊢ (coeff m✝) (pderivFun i f) = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

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 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

Tactic:
· rw [coeff_pderivFun, coeff_pderiv, coeff_trunc, if_pos (add_lt_add_left 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 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (2 ^ 0))ˣ ↔ 0 ≤ 2

Tactic:
| =>

Goal state after:
n : ℕ
⊢ IsCyclic (ZMod (2 ^ 0))ˣ ↔ 0 ≤ 2
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (2 ^ 1))ˣ ↔ 1 ≤ 2

Tactic:
| =>

Goal state after:
n : ℕ
⊢ IsCyclic (ZMod (2 ^ 1))ˣ ↔ 1 ≤ 2
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (2 ^ 2))ˣ ↔ 2 ≤ 2

Tactic:
| =>

Goal state after:
n : ℕ
⊢ IsCyclic (ZMod (2 ^ 2))ˣ ↔ 2 ≤ 2
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
| =>

Goal state after:
n✝ n : ℕ
⊢ IsCyclic (ZMod (2 ^ (n + 3)))ˣ ↔ n + 3 ≤ 2
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
⊢ (coeff n) f = (coeff n) g

Tactic:
have : single i 1 ≤ n := fun j ↦ by
    by_cases hj : j = i <;> grind [single_eq_same, single_eq_of_ne]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k ∈ Finset.range n, exp A ^ k = mk fun p ↦ ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹

Tactic:
simp only [exp_pow_eq_rescale_exp, rescale]

Goal state after:
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k ∈ Finset.range n,
      { toFun := fun f ↦ mk fun n ↦ ↑k ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        (exp A) =
    mk fun p ↦ ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
_root_.bernoulli_one

Goal state after:
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ ∀ i ∈ {p ∈ range (n + 1) | Nat.Prime p}, 1 ≤ id i

Tactic:
grind [→ Prime.pos]

Goal state after: