mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p ↦ Ico p.1 p.2) (pure a ×ˢ pure a) ⊥.smallSets

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p ↦ Ioc p.1 p.2) (pure a ×ˢ pure a) ⊥.smallSets

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p ↦ Ioo p.1 p.2) (pure a ×ˢ pure a) ⊥.smallSets

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
m : ℤ
hm : a ^ (m - 1) < a ^ m
hm' : a ^ m < a ^ (m - 1) * a * a
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = a ^ (m - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg✝ : Tendsto g l (𝓝 C)
x : α
hg : C / 2 < g x
⊢ 0 ≤ f x → f x * (C / 2) ≤ f x * g x

Tactic:
hf

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf✝ : Tendsto f l atTop
hg✝ : Tendsto g l (𝓝 C)
x : α
hg : C / 2 < g x
hf : 0 ≤ f x
⊢ f x * (C / 2) ≤ f x * g x
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), 0 < i ↔ ((fun x ↦ 0 < x) ∘ Inv.inv) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][0]? =
    some (s ∈ 𝓝[≥] a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][3]? =
    some (∃ u ∈ Ioc a u', Ico a u ⊆ s)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][4]? =
    some (∃ u ∈ Ioi a, Ico a u ⊆ s)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), i < 0 ↔ ((fun x ↦ x < 0) ∘ Inv.inv) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][0]? =
    some (s ∈ 𝓝[≤] a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][3]? =
    some (∃ l ∈ Ico l' a, Ioc l a ⊆ s)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][4]? =
    some (∃ l ∈ Iio a, Ioc l a ⊆ s)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : ↑e.source), e.source.domRestrict (↑e) x ∈ e.target

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : ↑e.target), e.target.domRestrict e.invFun x ∈ e.source

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε

Tactic:
simp [nhds_eq_iInf_mabs_div, mabs_div_comm a]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b / a|ₘ < ε}

Tactic:
simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |b / a|ₘ < r}).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b / a|ₘ < ε}
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)

Tactic:
gcongr <;> apply min_le_right

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
c d : 𝕜
⊢ Tendsto (fun x ↦ c * x ^ 0) atTop (𝓝 d) ↔ (c = 0 ∨ 0 = 0) ∧ c = d

Tactic:
simp [tendsto_const_nhds_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inr.inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d

Tactic:
simp [tendsto_const_nhds_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case e_a
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 ((Homeomorph.mulLeft₀ x ⋯).symm 0) = 𝓝 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[ts] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
by
  rw [t.topology_eq_generate_intervals]; rfl

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).source = s

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).target = s

Tactic:
simp

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : IsEmpty α
⊢ ∅.Countable

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).1 = (↑(PartialEquiv.refl (α × β)) (x, y)).1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).2 = (↑(PartialEquiv.refl (α × β)) (x, y)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hsymm.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).1 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hsymm.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).2 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔ (x, y) ∈ (PartialEquiv.refl (α × β)).source

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).1 = (↑((e.trans f).prod (e'.trans f')) (x, y)).1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).2 = (↑((e.trans f).prod (e'.trans f')) (x, y)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).1 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).2 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source

Tactic:
simp

Goal state after:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)) x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hsymm
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).symm x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)).symm x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hs
ι : Type u_5
αi : ι → Type u_6
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).source ↔ x✝ ∈ (PartialEquiv.refl ((i : ι) → αi i)).source

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.target = univ
⊢ e.source ⊆ univ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Mono f], ⊤ Y → ⊤ X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Epi f], ⊤ X → ⊤ Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Extensions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : HasZeroMorphisms C
⊢ ∀ {S : ShortComplex C}, S.ShortExact → ⊤ S.X₁ → ⊤ S.X₃ → ⊤ S.X₂

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
hl : ∃ l, l < a
hu : ∃ u, a < u
s : Set α
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) ↔ ∃ i, (i.1 < a ∧ a < i.2) ∧ Ioo i.1 i.2 ⊆ s

Tactic:
simp

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
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
⊢ ENat.card (Fin n) ≤ ↑n

Tactic:
simp

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
⊢ {x | n • x = 0}.encard = {x | n.natAbs • x = 0}.encard

Tactic:
simp

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
n : ℕ
hx : 0 < n • p
⊢ ↑n • p = n • p

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), OrderTopology (X i)
a b x : (i : ι) → X i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioc_mem_nhds (ha i) (hb i)

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : Field 𝕜
p q : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
x : AddCircle p
⊢ ↑((↑0)⁻¹ * ↑((equivIco p 0) x)) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ f.hom.hom.app { as := PUnit.unit } ≫ Y✝.map (𝟙 { as := PUnit.unit }) =
    X✝.map (𝟙 { as := PUnit.unit }) ≫ f.hom.hom.app (𝟙_ (Discrete PUnit.{u + 1}))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (ConcreteCategory.hom (cokernel.π g))
      (y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)) =
    (ConcreteCategory.hom (cokernel.π g)) y

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
hx : a ∈ Ico a (a + p)
⊢ f (a + p) = f a

Tactic:
hf

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
hx : a ∈ Ico a (a + p)
⊢ f (a + p) = f (a + p)
Module: Mathlib.CategoryTheory.Monoidal.CommGrp_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
X : CommGrp C
⊢ η ≫ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom = η

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommGrp_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
X : CommGrp C
⊢ μ ≫ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom =
    ((Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom ⊗ₘ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom) ≫ μ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ (a ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ (z ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 1 • (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • (ConcreteCategory.hom f) x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ Cofork.π c ≫ (Iso.refl c.pt).hom =
    Cofork.π (CokernelCofork.ofπ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.g ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : (free R).obj X ⟶ M
x✝ : X
⊢ (ConcreteCategory.hom
        ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝¹)))
      (freeMk x✝) =
    (ConcreteCategory.hom x✝¹) (freeMk x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₁ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₁

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₂ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₃ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₃

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : X ⟶ ↑M
x✝ : X
⊢ (ConcreteCategory.hom
          ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x))
            ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) x✝¹))).toFun
      x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₁ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₁

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₂ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₃ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₃

Tactic:
simp

Goal state after: