mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
by
  induction hA with
  | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]
  | rel R ts =>
    simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
⊢ IsLinearSet s ↔ ∃ a n f, s = a +ᵥ range ⇑f

Tactic:
isLinearSet_iff_exists_fg_eq_vadd,

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
⊢ (∃ a P, P.FG ∧ s = a +ᵥ ↑P) ↔ ∃ a n f, s = a +ᵥ range ⇑f
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
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Tactic:
let S : ℕ →o M ≃ₚ[L] N :=
    ⟨Subtype.val ∘ (Order.sequenceOfCofinals g D),
      (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
⊢ ∃ f, ↑g ≤ f.toPartialEquiv
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
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
surj_f : Function.Surjective ⇑F
⊢ DirectLimit G f ≃[L] DirectLimit G' f'

Tactic:
exact ⟨Equiv.ofBijective F ⟨F.injective, surj_f⟩, F.map_fun', F.map_rel'⟩

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
let S : ℕ →o M ≃ₚ[L] N :=
    ⟨Subtype.val ∘ (Order.sequenceOfCofinals g D),
      (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩

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, ↑g ≤ f.toEmbedding.toPartialEquiv
Module: Mathlib.ModelTheory.DirectLimit

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

Tactic:
eq_top_iff,

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

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

Tactic:
apply (Equiv_iSup S).injective
  simp only [Equiv.apply_symm_apply]
  rfl

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ hs.setOfFractNe =
    ⋃ u ∈ hs.fundamentalDomain \ {hs.base}, {x | ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = u + y}

Tactic:
ext x
    simp only [setOfFractNe, mem_iUnion, mem_ofPred_eq, exists_prop]
    constructor
    · intro hx
      refine ⟨hs.fract x, ⟨hs.fract_mem_fundamentalDomain x, hx⟩, ∑ i, (hs.floor x i).toNat • i.1,
        ?_, ∑ i, (-hs.floor x i).toNat • i.1, ?_, ?_⟩
      · exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _
      · exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _
      · exact hs.add_floor_neg_toNat_sum_eq x
    · 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.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    {x | x ∘ Sum.inr ∈ closure hs.basisSet ∧ ∃ y' ∈ closure hs.basisSet, x ∘ Sum.inl + y' = i + x ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure hs.basisSet} ∩ {a | ∃ y' ∈ closure hs.basisSet, a ∘ Sum.inl + y' = i + a ∘ Sum.inr})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    {x | x ∘ Sum.inr ∈ closure hs.basisSet ∧ (x ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr = i + (x ∘ Sum.inl) ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure hs.basisSet} ∩
      {a | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure {↑i} ∧
        ∃ z ∈ closure (hs.basisSet \ {↑i}),
          ∃ z' ∈ closure (hs.basisSet \ {↑i}), x ∘ Sum.inl + ↑i + x ∘ Sum.inr + z' = hs.base + z}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure {↑i}} ∩
      {a |
        ∃ z ∈ closure (hs.basisSet \ {↑i}),
          ∃ z' ∈ closure (hs.basisSet \ {↑i}), a ∘ Sum.inl + ↑i + a ∘ Sum.inr + z' = hs.base + z})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i}) ∧
        ∃ z' ∈ closure (hs.basisSet \ {↑i}),
          (x ∘ Sum.inl) ∘ Sum.inl + ↑i + (x ∘ Sum.inl) ∘ Sum.inr + z' = hs.base + x ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i})} ∩
      {a |
        ∃ z' ∈ closure (hs.basisSet \ {↑i}),
          (a ∘ Sum.inl) ∘ Sum.inl + ↑i + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base + a ∘ Sum.inr})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i}) ∧
        ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr =
          hs.base + (x ∘ Sum.inl) ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i})} ∩
      {a |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
          hs.base + (a ∘ Sum.inl) ∘ Sum.inr})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure {↑i} ∧
        ∃ z ∈ closure (hs.basisSet \ {↑i}),
          ∃ z' ∈ closure (hs.basisSet \ {↑i}), x ∘ Sum.inl + z' = hs.base + ↑i + x ∘ Sum.inr + z}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure {↑i}} ∩
      {a |
        ∃ z ∈ closure (hs.basisSet \ {↑i}),
          ∃ z' ∈ closure (hs.basisSet \ {↑i}), a ∘ Sum.inl + z' = hs.base + ↑i + a ∘ Sum.inr + z})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i}) ∧
        ∃ z' ∈ closure (hs.basisSet \ {↑i}),
          (x ∘ Sum.inl) ∘ Sum.inl + z' = hs.base + ↑i + (x ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i})} ∩
      {a |
        ∃ z' ∈ closure (hs.basisSet \ {↑i}),
          (a ∘ Sum.inl) ∘ Sum.inl + z' = hs.base + ↑i + (a ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr})
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    {x |
      x ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i}) ∧
        ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
          hs.base + ↑i + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x ∘ Sum.inl) ∘ Sum.inr}

Tactic:
rw [ofPred_and]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure (hs.basisSet \ {↑i})} ∩
      {a |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
          hs.base + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr})
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
⊢ Nonempty (M ≃[L] N)

Tactic:
let v : M ≃ₚ[L] N := {
    dom := S
    cod := emb_S.toHom.range
    toEquiv := emb_S.equivRange
  }

Goal state after:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty (M ≃[L] N)
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith φ)ᶜ

Tactic:
rw [← typesWith_not]; exact isOpen_typesWith _

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

Goal state before:
pp: ⊢ φ 4 = 2

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (g : (ZMod 8)ˣ), g ^ 2 = 1

Tactic:
decide

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

Goal state before:
pp: case «0»
n : ℕ
hn : 0 ≤ 2
⊢ φ (2 ^ 0) = 2 ^ (0 - 1)

Tactic:
decide

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

Goal state before:
pp: case «1»
n : ℕ
hn : 1 ≤ 2
⊢ φ (2 ^ 1) = 2 ^ (1 - 1)

Tactic:
decide

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

Goal state before:
pp: case «2»
n : ℕ
hn : 2 ≤ 2
⊢ φ (2 ^ 2) = 2 ^ (2 - 1)

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.134 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.134 ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊a⌋₊, c k
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : 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⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ f ↑⌊b⌋₊ • ∑ i ∈ range (⌊b⌋₊ + 1), c i - f ↑(⌊a⌋₊ + 1) • ∑ i ∈ range (⌊a⌋₊ + 1), c i -
      ∑ i ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(i + 1) - f ↑i) • ∑ i ∈ range (i + 1), c i =
    f b • ∑ i ∈ Icc 0 ⌊b⌋₊, c i - f a • ∑ i ∈ Icc 0 ⌊a⌋₊, c i - ∫ (x : ℝ) in a..b, deriv f x • ∑ i ∈ Icc 0 ⌊x⌋₊, c i

Tactic:
range_eq_Ico,

Goal state after:
case inr
𝕜 : 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⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ f ↑⌊b⌋₊ • ∑ x ∈ Ico 0 (⌊b⌋₊ + 1), c x - f ↑(⌊a⌋₊ + 1) • ∑ x ∈ Ico 0 (⌊a⌋₊ + 1), c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(x + 1) - f ↑x) • ∑ x ∈ Ico 0 (x + 1), c x =
    f b • ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a • ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x • ∑ x ∈ Icc 0 ⌊x⌋₊, c x
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inl
hn0 : 1 ≠ 0
⊢ IsCyclic (ZMod (4 * 1))ˣ ↔ 1 = 0 ∨ 1 = 1

pp: case inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
· simp [isCyclic_units_four]

Goal state after:
case inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
rintro ⟨p, m, -, -, -, rfl⟩

Goal state after:
case neg.inl
p m : ℕ
h0 : ¬2 * p ^ m = 0
h1 : ¬2 * p ^ m = 1
h2 : ¬2 * p ^ m = 2
h4 : ¬2 * p ^ m = 4
hn : Odd (2 * p ^ m)
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Exp

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

Tactic:
symm

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n.choose x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ 3 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ primesBelow 0 = ∅

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ primesBelow 1 = ∅

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ primesBelow 2 = ∅

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ range (k + n) | Prime x}) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
range_eq_Ico,

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 (k + n) | Prime x}) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 (k + n) | Prime x}) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
range_eq_Ico,

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 (k + n) | Prime x}) ≤ #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ

Tactic:
symm

Goal state after:
n p : ℕ
⊢ ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 0# = 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 1# = 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 2# = 2

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ Nat.choose 4 2 = 6

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with Nat.Prime p, p

Tactic:
by
  simp_rw [primorial, ← Ico_zero_eq_range]
  rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
  exacts [Nat.zero_le _, by lia, disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inl.inl
ihn : ∀ m < 0 + 0 + 1, m ≠ 0 → m# < 4 ^ m
hn : 0 + 0 + 1 ≠ 0
⊢ (0 + 0 + 1)# < 4 ^ (0 + 0 + 1)

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr.inl
ihn : ∀ m < 1 + 1, m ≠ 0 → m# < 4 ^ m
hn : 1 + 1 ≠ 0
ho : Odd 1
⊢ (1 + 1)# < 4 ^ (1 + 1)

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inl
⊢ 0# ≤ 4 ^ 0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
← exp_pow_sum,

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ (∑ k ∈ range n, exp ℚ ^ k) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: inst✝ : Fact (Nat.Prime 2)
hd : 2 ≥ 2
⊢ ¬2 ∣ 3

Tactic:
decide

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

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
let e := Fintype.equivFin ι

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : 2 * ↑k - 2 * ↑m + 1 = ↑(d + 1)
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))

Tactic:
rw [h_exp, h_denom_rat, mul_div_assoc]

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : 2 * ↑k - 2 * ↑m + 1 = ↑(d + 1)
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * (↑p ^ (d - 1) / ↑(d + 1)))