mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
    hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ u ∈ 𝓤 β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, UniformContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
simpa [uniformContinuousOn_univ] using h

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩

Goal state after:
case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn F S

Tactic:
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢
  unfold UniformContinuousOn
  rw [iInf_uniformity]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun i ↦ F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Tactic:
exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹

Tactic:
mem_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ Inv.inv ⁻¹' s⁻¹ ∈ f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥

Tactic:
rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]

Tactic:
by
  simp only [uIcc, inv_Icc, inv_sup, inv_inf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ (↑f.symm).comp ↑f = ContinuousMap.id α

Tactic:
rw [← coe_trans, self_trans_symm, coe_refl]

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Iio c
⊢ b * f x✝¹ ∈ Iio (b * c)

Tactic:
by rw [Set.mem_Iio] at *; gcongr

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Iio c
⊢ f x✝¹ * b ∈ Iio (c * b)

Tactic:
by rw [Set.mem_Iio] at *; gcongr

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

Goal state before:
pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
· intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
⊢ IsOpen[inst✝³] {0}

Tactic:
by_cases H : ∃ x ≠ 0, x ∈ W

Goal state after:
case pos
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}

case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]
  -- Let `𝒰 ≤ 𝓟 (f ⁻¹' K)` an ultrafilter.
  intro 𝒰 h𝒰
  -- In other words, we have `map f 𝒰 ≤ 𝓟 K`
  rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰
  -- Thus, by compactness of `K`, the ultrafilter `map f 𝒰` tends to some `y ∈ K`.
  rcases hK.ultrafilter_le_nhds _ h𝒰 with ⟨y, hyK, hy⟩
  -- Then, by properness of `f`, that means that `𝒰` tends to some `x ∈ f ⁻¹' {y} ⊆ f ⁻¹' K`,
  -- which completes the proof.
  rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩
  exact ⟨x, hyK, hx⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x

Tactic:
eventually_all_finset

Goal state after:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ i ∈ s, ∀ᶠ (x : X) in l, f i x = g i x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s * t)

Tactic:
rw [← image_op_smul]
  exact hs.smul_left

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
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed[inst✝²] t
⊢ IsClosed[inst✝²] (t * ↑H)

Tactic:
exact ht.mul_right_of_isCompact hH

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
⊢ closure[inst✝²] s ⊆ s * s'

Tactic:
intro y hy
  obtain ⟨_, ⟨b, hb, rfl⟩, hc⟩ :=
    mem_closure_iff_nhds.mp hy ((y * ·) '' s')
      (by simpa using (isOpenMap_mul_left y).image_mem_nhds hs'₀)
  simpa using Set.mul_mem_mul hc (h_symm b hb)

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Tactic:
by
  simp only [ofPred_forall]
  exact isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

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
⊢ (𝓝[>] a)⁻¹ = 𝓝[<] a⁻¹

Tactic:
by
  convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2
  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
⊢ (𝓝[<] a)⁻¹ = 𝓝[>] a⁻¹

Tactic:
by
  convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

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

Tactic:
convert! (Homeomorph.divLeft c).map_nhds_eq .. using 2

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
⊢ U ∈ map (fun p ↦ p.2 * p.1⁻¹) ((comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)).lift' fun s ↦ SetRel.comp s s)

Tactic:
by
    rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩
    refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
    rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩
    simpa using V_mul _ hz₂ _ hz₁

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

Goal state before:
pp: G : Type u
inst✝³ : TopologicalSpace G
H : Type v
inst✝² : TopologicalSpace H
inst✝¹ : Mul G
inst✝ : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ IsOpen (⇑e.symm ⁻¹' s) ↔ IsOpen s

Tactic:
by convert! (he _).symm; exact (e.preimage_symm_preimage s).symm

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0

Tactic:
intro W'

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
⊢ W' ∈ 𝓝 0 →
    W' ∈
      map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
        (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:

Tactic:
|c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
        _ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul_le ..
        _ < δ * (ε / δ) := mul_lt_mul_of_lt_of_lt hc hd
        _ = ε := mul_div_cancel ..

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

Goal state before:
pp: 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
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

Tactic:
have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl

Goal state after:
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
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this✝ : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
this : m < l ∧ l < m + 1
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source

Tactic:
· intro x hx
    simp only [mem_inter_iff, restr_source] at hx
    exact he.2 hx.1

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
⊢ kl ⊆ k

Tactic:
simp [k_eq]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this : Finite ↑kl
⊢ kr ⊆ k

Tactic:
simp [k_eq]

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

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∀ (c : CharacterModule A), c a = 0
⊢ a = 0

Tactic:
contrapose! h

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ c, c a ≠ 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := ⋯
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 α := ⋯
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
⊢ Ioo (z x) (y x) ⊆ Ioc (z x) x

Tactic:
simp_rw [subset_def, mem_Ioo, mem_Ioc]

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
⊢ ∀ (x_1 : α), z x < x_1 ∧ x_1 < y x → z x < x_1 ∧ x_1 ≤ x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₁ = (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₂
⊢ ↑m₁ = ↑m₂

Tactic:
simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h
          refine nsmul_injOn_Iio_addOrderOf ?_ ?_ h <;> rw [addOrderOf_period_div hn]
          exacts [m₁.2.1, m₂.2.1]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ S = (fun N ↦ mk (↟N.subtype)) ((fun S ↦ (Hom.hom S.arrow).range) S)

Tactic:
fapply eq_mk_of_comm
        · apply LinearEquiv.toModuleIso
          apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)
          constructor
          · simp [← LinearMap.ker_eq_bot, ker_eq_bot_of_mono]
          · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict,
              Submodule.comap_subtype_self]
            exact LinearMap.mem_range_self _
        · ext x
          rfl

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 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝]
    (Quot.lift ((Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(equivIccQuot p a))

Tactic:
refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[instTopologicalSpaceQuot, inst✝] (Quot.lift ((Icc a (a + p)).domRestrict f) ⋯)
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
← cancel_epi (ComposableArrows.app' e.hom i),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = app' e.hom i ⋯ ≫ 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f

Tactic:
intro hf
    obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)
    rw [comp_id] at fac
    exact epi_of_epi_fac fac.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ ∀ (X Y : WalkingMultispan J), Small.{t, max w w'} (X ⟶ Y)

Tactic:
rintro (l | r) (l' | r')

Goal state after:
case left.left
J : MultispanShape
l l' : J.L
⊢ Small.{t, max w w'} (left l ⟶ left l')

case left.right
J : MultispanShape
l : J.L
r' : J.R
⊢ Small.{t, max w w'} (left l ⟶ right r')

case right.left
J : MultispanShape
r : J.R
l' : J.L
⊢ Small.{t, max w w'} (right r ⟶ left l')

case right.right
J : MultispanShape
r r' : J.R
⊢ Small.{t, max w w'} (right r ⟶ right r')
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
i : J.L
⊢ t.π.app (WalkingMulticospan.left i) = e.hom ≫ s.π.app (WalkingMulticospan.left i)

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
j : J.R
⊢ t.π.app (WalkingMulticospan.right j) = e.hom ≫ s.π.app (WalkingMulticospan.right j)

Tactic:
simp [← h]

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

Goal state before:
pp: 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
k : ℕ
⊢ ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
induction k with

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ a⁻¹⁻¹ • x ∈ S ↔ a • x ∈ S
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
a : A
⊢ (algebraMap A B) a ∈ g • P ↔ (algebraMap A B) a ∈ P

Tactic:
mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
a : A
⊢ g⁻¹ • (algebraMap A B) a ∈ P ↔ (algebraMap A B) a ∈ P
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized' S p f (sSup s) = sSup (localized' S p f '' s)

Tactic:
by rw [sSup_eq_iSup', localized'_iSup, sSup_image']

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

Goal state before:
pp: case mpr
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
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I

Tactic:
· rw [← mk'_spec S x y] at h
    obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)
    have := I.mul_mem_left b h
    rwa [mul_comm, mul_assoc, hb, mul_one] at this

Goal state after: