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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a * x) ∘ fun x ↦ x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
b c : G₀
hbc : b ≤ c
ha : 0 ≤ 0
⊢ (fun x ↦ 0 * x) '' Icc b c = Icc (0 * b) (0 * c)

pp: case inr
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha✝ : 0 ≤ a
hbc : b ≤ c
ha : 0 < a
⊢ (fun x ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
· simp [(nonempty_Icc.2 hbc).image_const]

Goal state after:
case inr
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha✝ : 0 ≤ a
hbc : b ≤ c
ha : 0 < a
⊢ (fun x ↦ a * x) '' Icc b c = Icc (a * b) (a * c)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
⊢ F =ᶠ[p] F'

Tactic:
rw [eventuallyEq_iff_exists_mem]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
⊢ ∃ s ∈ p, EqOn F F' s
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := ⋯
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ (fun i x ↦ g (F i x)) =ᶠ[p] fun i x ↦ g (F' i x)

Tactic:
rw [eventuallyEq_iff_exists_mem]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ ∃ s ∈ p, EqOn (fun i x ↦ g (F i x)) (fun i x ↦ g (F' i x)) s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s

Tactic:
zero_smul_set hs,

Goal state after:
case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst✝²] 0 = 0 • closure[inst✝²] s
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsProperMap (f i)
⊢ IsProperMap fun x i ↦ f i (x i)

Tactic:
simp_rw [isProperMap_iff_ultrafilter] at h ⊢
  constructor
  -- Continuity is clear.
  · exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)
  -- Let `𝒰 : Ultrafilter (Π i, X i)`, and assume that `Π i, f i` tends to some `y : Π i, Y i`
  -- along `𝒰`.
  · intro 𝒰 y hy
  -- That means that each `f i` tends to `y i` along `map (eval i) 𝒰`.
    have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by
      simpa [tendsto_pi_nhds] using! hy
  -- Thus, by properness of all the `f i`s, we can choose some `x : Π i, X i` such that, for all
  -- `i`, `f i (x i) = y i` and `map (eval i) 𝒰` tends to  `x i`.
    choose x hxy hx using fun i ↦ (h i).2 (this i)
  -- By the properties of the product topology, that means that `𝒰` tends to `x`,
  -- which completes the proof since `(Π i, f i) x = y`.
    refine ⟨x, funext hxy, ?_⟩
    rwa [nhds_pi, le_pi]

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 * p.2

Tactic:
by
    rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul

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 Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsLT (a := a⁻¹)

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

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one]
        exact tendsto_comap.comp tendsto_fst

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
by
  simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]

Goal state after:
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 : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x | x i₀ ∈ Ioc m (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) = {z | m < z i₀} ∩ univ.pi fun j ↦ Ioc (x j) (y j)

Tactic:
← pi_inter_compl ({i₀} : Set ι),

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

Tactic:
← pi_inter_compl ({i₀} : Set ι),

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₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioc (x i₀) m} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ (({i₀}.pi fun j ↦ Ioc (x j) (y j)) ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j))
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 : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ y⁻¹ < x

Tactic:
exact inv_lt_of_inv_lt₀ (by positivity) hy

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 : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atBot l
⊢ Tendsto f (𝓝[<] 0) l

Tactic:
by
  convert! h.comp tendsto_inv_nhdsLT_zero
  grind

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 c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]

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.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s :=
      exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩

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}
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx⟩ ∧ n • y_1 = ↑k • p

Tactic:
rw [Set.mem_ofPred, ← mk_nsmul, eq_zero_iff] at hx

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.Order.Basic

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
h : s ∈ 𝓝 a
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
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
⊢ (LinearMap.toSpanSingleton ℤ A a).ker = Ideal.span {↑(addOrderOf a)}

Tactic:
by
    ext1 x
    rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ IsEmpty { u // ¬IsOfFinAddOrder u }

Tactic:
simpa [isEmpty_subtype] using h

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

Goal state before:
pp: 𝕜 : 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)
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIoc p a f ↑x = f x

Tactic:
obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx

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)
⊢ liftIoc p a f ↑a = f a

case inr
𝕜 : 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)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : a < x ∧ x < a + p
⊢ liftIoc p a f ↑x = f x
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact

Tactic:
refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.Exact

Tactic:
refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact
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
⊢ Epi S.L₀'.g

Tactic:
dsimp only [L₀']; infer_instance

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₂
⊢ F.map (f₁ + f₂) ≫ (α.app Y).hom = (α.app X).hom ≫ G.map (f₁ + f₂)

Tactic:
rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i i ⋯ hj'

Tactic:
rw [F.map'_self i, G.map'_self i, id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J✝ : Type u
inst✝³ : Category.{v, u} J✝
T : Comonad C
D : J✝ ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j
⊢ m = { f := t.lift (T.forget.mapCone s), h := ⋯ }

Tactic:
by
    ext1
    apply t.hom_ext
    intro j
    simpa using congr_arg Coalgebra.Hom.f (J j)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ IsColimit ((comonadicRightAdjoint R).mapCocone c)

Tactic:
apply isColimitChangeEmptyCocone D (colimit.isColimit F)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih.refine_1
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ OrderDual.ofDual (OrderDual.toDual (sInf c))

Tactic:
rw [OrderDual.ofDual_toDual, le_sInf_iff]
    exact fun _ hx => (hc hx).2

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
set S := { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p }
  suffices h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (· ∈ S) m by
    obtain ⟨p, hJp, hp⟩ := h
    exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩
  apply zorn_le_nonempty₀
  swap
  · refine ⟨show J.IsPrime by infer_instance, e⟩
  rintro (c : Set (Ideal R)) hc hc' J' hJ'
  refine
    ⟨OrderDual.toDual (sInf c),
      ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩
  · rw [OrderDual.ofDual_toDual, le_sInf_iff]
    exact fun _ hx => (hc hx).2
  · rintro z hz
    rw [OrderDual.le_toDual]
    exact sInf_le hz

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case e'_4
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ p = comap (algebraMap R S) P

Tactic:
exact Ideal.LiesOver.over

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
hx : x ∈ I
s : ↥M
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) x s * (algebraMap R S) ↑(⟨x, hx⟩, s).2 =
    (algebraMap R S) ↑(⟨x, hx⟩, s).1

Tactic:
rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_spec]

Goal state after: