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

Goal state before:
pp: L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) ↔ ∃ i, M ∈ L.age (G i)

Tactic:
constructor

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) → ∃ i, M ∈ L.age (G i)

case mpr
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ (∃ i, M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Language.simpleGraphOfStructure V = G

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (Language.simpleGraphOfStructure V).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
⊢ (simpleGraphOfStructure V).structure = S

Tactic:
ext

Goal state after:
case funMap
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Functions x✝²
x✝ : Fin x✝² → V
⊢ funMap x✝¹ x✝ = funMap x✝¹ x✝

case RelMap
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Relations x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, hs.floor x i < 0) ↔
    ∃ i,
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, hs.floor x i < 0) →
    ∃ i,
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z

case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ i,
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + ↑i + y + z' = hs.base + z) →
    hs.fract x = hs.base ∧ ∃ i, hs.floor x i < 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : x + ↑i + n • ↑i + z' = hs.base + z
⊢ hs.floor x i < 0

Tactic:
apply congr_arg (hs.floor · i) at heq

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + ↑i + n • ↑i + z') i = hs.floor (hs.base + z) i
⊢ hs.floor x i < 0
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
constructor

Goal state after:
case mp
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) →
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K →
    ∃ M, Countable ↑M ∧ L.age ↑M = K
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i) ↔
    ∃ i,
      ↑i ∉ hs.periods ∧
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i) →
    ∃ i,
      ↑i ∉ hs.periods ∧
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z

case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ i,
      ↑i ∉ hs.periods ∧
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z) →
    hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := ⋯
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ (r.comp g).equivRange x = (r.comp g).equivRange (s.equivRange.symm ⟨s x, ⋯⟩)

Tactic:
ext

Goal state after:
case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := ⋯
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ ↑((r.comp g).equivRange x) = ↑((r.comp g).equivRange (s.equivRange.symm ⟨s x, ⋯⟩))
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

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsUltrahomogeneous M → L.IsExtensionPair M M

case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsExtensionPair M M → L.IsUltrahomogeneous M
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
⊢ (↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
      ((↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).toEquiv.toEmbedding.comp
        (Substructure.inclusion dom_le_S)) =
    (↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding

Tactic:
ext

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion dom_le_S)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case h
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
⊢ g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    g.toEmbedding.comp S.subtype

Tactic:
ext

Goal state after:
case h
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
x✝ : ↥S
⊢ (g.toEmbedding.toPartialEquiv.cod.subtype.comp
        (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)))
      x✝ =
    (g.toEmbedding.comp S.subtype) x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : x + z' = hs.base + ↑i + n • ↑i + z
⊢ 0 < hs.floor x i

Tactic:
apply congr_arg (hs.floor · i) at heq

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + z') i = hs.floor (hs.base + ↑i + n • ↑i + z) i
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
this : LE M := L.leOfStructure M
⊢ L.OrderedStructure M

Tactic:
constructor

Goal state after:
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
this : LE M := ⋯
⊢ ∀ (x : Fin 2 → M), RelMap leSymb x ↔ x 0 ≤ x 1
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
⊢ L.IsExtensionPair M N

Tactic:
intro ⟨f, f_FG⟩ m

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
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ sᶜ = hs.setOfFractNe ∪ (hs.setOfFloorNeg ∪ hs.setOfFloorPos)

Tactic:
ext

Goal state after:
ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x✝ : ι → ℕ
⊢ x✝ ∈ sᶜ ↔ x✝ ∈ hs.setOfFractNe ∪ (hs.setOfFloorNeg ∪ hs.setOfFloorPos)
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
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty (↥S ↪[L] N)
g : ↥(f.dom ⊔ (closure L).toFun {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
⊢ (↑⟨{ dom := S, cod := g.toHom.range, toEquiv := g.equivRange }, S_FG⟩).cod.subtype.comp
      ((↑⟨{ dom := S, cod := g.toHom.range, toEquiv := g.equivRange }, S_FG⟩).toEquiv.toEmbedding.comp
        (Substructure.inclusion ⋯)) =
    (↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding

Tactic:
ext

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
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty (↥S ↪[L] N)
g : ↥(f.dom ⊔ (closure L).toFun {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := S, cod := g.toHom.range, toEquiv := g.equivRange }, S_FG⟩).cod.subtype.comp
        ((↑⟨{ dom := S, cod := g.toHom.range, toEquiv := g.equivRange }, S_FG⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
⊢ BaireSpace X

Tactic:
constructor

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
⊢ ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)

Tactic:
ext

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ ↦ {p | φ ∈ p}) '' S)
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
⊢ ⋂ i, {p | S i ⊆ ↑p} = {p | ⋃ i, S i ⊆ ↑p}

Tactic:
ext

Goal state after:
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ ⋂ i, {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ i, S i ⊆ ↑p}
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ CompactSpace (T.CompleteType α)

Tactic:
constructor

Goal state after:
L : Language
T : L.Theory
α : Type u_1
⊢ IsCompact univ
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: n : ℕ
⊢ IsAlmostPrime 1 n ↔ Prime n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ IsAlmostPrime 1 n → Prime n

case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: k l m n : ℕ
hm : k.IsAlmostPrime m
hn : l.IsAlmostPrime n
⊢ Ω m + Ω n = k + l

Tactic:
hm.2,

Goal state after:
k l m n : ℕ
hm : k.IsAlmostPrime m
hn : l.IsAlmostPrime n
⊢ k + Ω n = k + l
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}

Tactic:
replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩

Goal state after:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k ∧ ↑k + 1 ≤ b

Tactic:
constructor

Goal state after:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k

case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inr
𝕜 : 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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
← intervalIntegrable_iff_integrableOn_Icc_of_le (aux3.trans aux2)

Goal state after:
case inl.inr
𝕜 : 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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
⊢ IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
rw [pow_one]

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:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
f g : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (pderivFun i (f + g)) = (coeff n✝) (pderivFun i f + pderivFun i g)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

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

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (pderivFun i ↑f) = (coeff n✝) ↑((pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

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

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((trunc R n) (pderivFun i f)) =
    MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf (1 + 4 * ↑a) = 2 ^ n

Tactic:
convert! orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n using 1

Goal state after:
a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf (1 + 4 * ↑a) = orderOf (1 + ↑2 ^ 2 * ↑a)

a : ℤ
ha : Odd a
n : ℕ
⊢ ¬↑2 ∣ a
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ (d⁄dX R) ↑f = ↑(Polynomial.derivative f)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ (coeff n✝) ((d⁄dX R) ↑f) = (coeff n✝) ↑(Polynomial.derivative f)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (exp A) = exp A'

Tactic:
ext

Goal state after:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (exp A)) = (coeff n✝) (exp A')
Module: Mathlib.RingTheory.PowerSeries.Exp

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

Tactic:
rw [coeff_derivative] at eq2

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

Goal state before:
pp: 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 !)⁻¹

Tactic:
ext

Goal state after:
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ (coeff 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)) =
    (coeff n✝) (mk fun p ↦ ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ (π ∘ fun n ↦ n - 1) = π'

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ (π ∘ fun n ↦ n - 1) x✝ = π' x✝
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ derivative 1 = 0

Tactic:
derivative_one

Goal state after:
case zero
⊢ 0 = 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert! sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int
  all_goals rw [Nat.floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
eval_finsetSum,

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

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ (-1) ^ n * bernoulli' n = 0

Tactic:
bernoulli'_eq_zero_of_odd h_odd hlt,

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ (-1) ^ n * 0 = 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : ¬K.Nonempty
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume

Tactic:
· rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
    exact integrableOn_empty

Goal state after: