mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)) +
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯))

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)) +
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯))
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) = ↑x + (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) = ↑x + (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑y
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Tactic:
]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : (range Subtype.val).OrdConnected
⊢ (range Subtype.val).OrdConnected

Tactic:
]

Goal state after:
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : (range Subtype.val).OrdConnected
⊢ (range Subtype.val).OrdConnected
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[≥] a = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
rw [nhdsWithin, nhds_eq_order]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Icc a a = Icc a a

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s

Tactic:
]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIcoDiv ?hp a x = toIcoDiv hp a x

pp: case hp
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ 0 < p

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIocDiv ?hp a x = toIocDiv hp a x

pp: case hp
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ 0 < p

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) ψ) y = ((dual f) ψ) y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x✝ : 𝕜
⊢ ¬x ≡ a [PMOD p]

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x✝ : 𝕜
⊢ ¬x ≡ a [PMOD p]
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: ⊢ Finite ↑(of PUnit.{u + 1})

Tactic:
]

Goal state after:
⊢ Finite ↑(of PUnit.{u + 1})
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hN : N.isFinite
⊢ M.isFinite

Tactic:
]

Goal state after:
M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hN : N.isFinite
⊢ M.isFinite
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
hM : M.isFinite
⊢ N.isFinite

Tactic:
]

Goal state after:
M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
hM : M.isFinite
⊢ N.isFinite
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Epi f
hM : M.isFinite
⊢ N.isFinite

Tactic:
by
    rw [AddCommGrpCat.epi_iff_surjective] at hf
    simp only [prop_isFinite_iff] at hM ⊢
    exact Finite.of_surjective _ hf

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] (⋃ z, Ioo (a + z • p) (a + p + z • p))

Tactic:
]

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] (⋃ z, Ioo (a + z • p) (a + p + z • p))
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ Finite ↑S.X₂

Tactic:
]

Goal state after:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ Finite ↑S.X₂
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ¬x ≡ a [PMOD p]

Tactic:
]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ¬x ≡ a [PMOD p]
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
hm : (fun x ↦ x • p) (((Int.divModEquiv n) m').1 * ↑n + ↑↑((Int.divModEquiv n) m').2) = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
hm : (fun x ↦ x • p) (((Int.divModEquiv n) m').1 * ↑n + ↑↑((Int.divModEquiv n) m').2) = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
x : ℤ
⊢ x • a = 0 ↔ x • a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)

Tactic:
]

Goal state after:
case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ (fun x ↦ x • p) (↑↑m.2 + m.1 * ↑n) = ↑m.2 • p + n • m.1 • p

Tactic:
]

Goal state after:
case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ (fun x ↦ x • p) (↑↑m.2 + m.1 * ↑n) = ↑m.2 • p + n • m.1 • p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)

Tactic:
]

Goal state after:
case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0

Tactic:
]

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

pp: A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a

Tactic:
]

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : ¬addOrderOf a = 0
hn : a = 0
⊢ a = 0

Tactic:
]

Goal state after:
case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : ¬addOrderOf a = 0
hn : a = 0
⊢ a = 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc : (dual (ℤ ∙ a).subtype) c = ofSpanSingleton a
h : c a = 0
⊢ ((dual (ℤ ∙ a).subtype) c) ⟨a, ⋯⟩ = 0

Tactic:
]

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc : (dual (ℤ ∙ a).subtype) c = ofSpanSingleton a
h : c a = 0
⊢ ((dual (ℤ ∙ a).subtype) c) ⟨a, ⋯⟩ = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Nonempty (Unique (A' ⧸ f.range))

Tactic:
]

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Nonempty (Unique (A' ⧸ f.range))
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x' = ↑x'

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioo (z x) (y x))

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioo (z x) (y x))
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down

Tactic:
]

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ n • p = n • p

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = ↑↑⟨x, hx⟩

Tactic:
]

Goal state after: