mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
x✝ : ↑s × β
⊢ (fun gx ↦ (gx.1, ↑gx.1 • gx.2)) ((fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2)) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed[inst✝⁵] t
⊢ IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)

Tactic:
rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
    MulAction.quotient_preimage_image_eq_union_mul]

Goal state after:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed[inst✝⁵] t
⊢ IsClosed[inst✝⁵] (⋃ g, (fun x ↦ g • x) '' t)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] (K * {1}) = closure[inst✝²] K

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ closure[inst✝²] (F * {1}) = F

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ (fun x1 x2 ↦ x1 * x2) (x * g) g⁻¹ = x

Tactic:
by simp

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
x y : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) x = ((MulDistribMulAction.toMonoidEnd H G) h) y → x = y

Tactic:
by simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))

Tactic:
by simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))

Tactic:
by simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))

Tactic:
by simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ ↑⊥.topologicalClosure = closure[inst✝²] {1}

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
⊢ map (fun x_1 ↦ x * x_1) (𝓝 1) = 𝓝 x

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
⊢ map (fun x_1 ↦ x_1 * x) (𝓝 1) = 𝓝 x

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
V : Set G
hV : V ∈ 𝓝 1 ∧ V ∩ ↑S = {1}
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U⁻¹
hgx : (fun x ↦ g * x) x ∈ U
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x ↦ g * x) x) x⁻¹ = g

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ U

Tactic:
by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ 𝓝 (x * y) = map (fun x_1 ↦ x * x_1) (map (fun x ↦ x * y) (𝓝 1 * 𝓝 1))

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (fun p ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
by
  simp [Cauchy, uniformity_eq_comap_nhds_one_swapped, ← tendsto_iff_comap]

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x : G₀
⊢ (∃ x_1, x_1 ≠ 0 ∧ x_1 = x) ↔ x ∈ {g | g = 0 → False}

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x✝ : { g // g ≠ 0 }
⊢ (fun g ↦ ⟨(↑g)⁻¹, ⋯⟩) ((fun g ↦ ⟨(↑g)⁻¹, ⋯⟩) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 ((Homeomorph.mulRight₀ a ha).symm.symm 1) = 𝓝 a

Tactic:
by simp

Goal state after:
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₀ : MonotoneOn f a
h₁ : AntitoneOn f c
⊢ b ∈ Iic b

Tactic:
by simp

Goal state after:
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₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
by simp

Goal state after:
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
⊢ b ∈ Iic b

Tactic:
by simp

Goal state after:
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:
by simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun a ↦ f (g a))
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)
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:
by 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:
by 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:
by simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' uIcc a (f i) = uIcc (update f i a) f

Tactic:
by
  simpa using image_update_uIcc f i a (f i)

Goal state after:
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:
by simp

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

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < 1} ×ˢ {x | norm x < ε}
hx : x ∈ {x | norm x < 1}
hy : y ∈ {x | norm x < ε}
⊢ uncurry (fun x1 x2 ↦ x1 * x2) (x, y) ∈ {x | norm x < ε}

Tactic:
calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
    _ < ε := (mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := ⋯
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ᶠ (x : α) in l, |f x| ≤ C

Tactic:
filter_upwards [hb, hB]

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C
Module: Mathlib.Topology.Algebra.Order.Field

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

Tactic:
have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]

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

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

Tactic:
by 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:
by 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:
by simp

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.target

Tactic:
t

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ
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:
by 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:
by 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:
by 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:
by simp

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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
⊢ uncurry ∘ₗ curry = LinearMap.id

Tactic:
by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop

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:
by 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:
by 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:
by simp

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:
by 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 = η

Tactic:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case refine_2
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
⊢ (∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0

Tactic:
rintro ⟨A', π, hπ, x, fac⟩

Goal state after:
case refine_2
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
A' : C
π : A' ⟶ A
hπ : Epi π
x : A' ⟶ X
fac : π ≫ y = x ≫ f
⊢ y ≫ Cofork.π c = 0
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
z₂ : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
by 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
z₂ z₂' : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
by 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
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ (z₂' ≫ S.iCycles) ≫ S.g = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₁.f ≫ S.L₁.g = 0 ≫ S.v₀₁.τ₃

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = S.L₀.g

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀.g ≫ S.δ = 0

Tactic:
by
  rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]

Goal state after: