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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f

Tactic:
UniformContinuousOn,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (univ ×ˢ univ)) (𝓤 β) ↔ UniformContinuous f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
⊢ y ∈ s i

Tactic:
rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s i
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := ⋯
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ball x (B (U b ⟨x, hx⟩)) ⊆ ⋃ x, ball (↑x) (B (U b x))

Tactic:
exact subset_iUnion (fun x => ball x.1 (B (U b x))) ⟨x, hx⟩

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

Goal state before:
pp: α : Type u_2
⊢ UniformSpace.comap id = id

Tactic:
ext : 2
  rw [uniformity_comap, Prod.map_id, comap_id]

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)

Tactic:
exact lift'_mono h le_rfl

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

Goal state before:
pp: α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
⊢ v ∈ (mulTSupport f)ᶜ → v ∈ f ⁻¹' N

Tactic:
hv

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases hsd.inter_open_nonempty (ball x <| t k) (isOpen_ball x (hto k))
        ⟨x, UniformSpace.mem_ball_self _ (ht_mem k)⟩ with
      ⟨y, hxy, hys⟩

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|

Tactic:
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
    abs_max_sub_max_le_max (-a) (-b) (-c) (-d)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ generate (UniformFun.basis α β 𝓕).sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets

Tactic:
le_generate_iff

Goal state after:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
UniformContinuousOn,

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V

Tactic:
ext uv
  exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
simp only [iInf_uniformity]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
simp [← map_prod_eq_map₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map₂ (fun x x_1 ↦ x) f g = f

Tactic:
rw [← map_prod_eq_map₂, map_fst_prod]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
UniformContinuousOn,

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α)) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (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_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
UniformContinuousOn,

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
UniformContinuousOn,

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
X : Type u_5
inst✝ : TopologicalSpace X
f : X → α →ᵤ[𝔖] β
⊢ Continuous[inst✝, topologicalSpace α β 𝔖] f ↔
    ∀ s ∈ 𝔖, Continuous[inst✝, UniformFun.topologicalSpace (↑s) β] (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖) ∘ f)

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt,
    UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformFun.tendsto_iff_tendstoUniformly,
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, @forall_comm X,
    Function.comp_def, domRestrict_eq, UniformFun.toFun_ofFun]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ 1 ≤ f / g ↔ ¬Disjoint f g

Tactic:
refine ⟨fun h hfg => ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False

case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g

Tactic:
· rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩
    exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

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

Goal state before:
pp: M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] (⋂ i, ⋂ i_1, {x | x (i • i_1) = σ i • x i_1})

Tactic:
exact isClosed_iInter fun c => isClosed_iInter fun x =>
    isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)

Goal state after:
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
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p

Tactic:
by
  classical
  obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp hF
  let F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
  have hF : F =ᶠ[p] F' := by
    rw [eventuallyEq_iff_exists_mem]
    refine ⟨s', hs', fun y hy => by grind⟩
  have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h
  apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h')
  rw [eventuallyEq_iff_exists_mem]
  refine ⟨s', hs', fun i hi => by grind⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
by
  rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
  rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
  use V, V1
  intro v w s t v_in w_in s_in t_in
  simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)

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
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ Int.negSucc n

Tactic:
simpa using (continuous_pow (n + 1)).fun_inv

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
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
⊢ map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)

Tactic:
simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using!
      (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
h' : G
⊢ h' ∈ ↑H → h ≠ h' → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'

Tactic:
h'_in

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
h' : G
h'_in : h' ∈ ↑H
⊢ h ≠ h' → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
by
    have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
    apply Countable.mono this
    simp [H, (subsingleton_isTop α).countable]

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 < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
x : R
hx : x ∈ {x | norm x < δ}
⊢ c * norm x < ε

Tactic:
exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : ↑e '' e.source = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'

Tactic:
rw [A, hs, I'] at I

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : e'.target = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ ∃ c, c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
by
  rcases isEmpty_or_nonempty α with hα | hα
  · exact ⟨∅, by simp, Subsingleton.elim _ _⟩
  obtain ⟨t, t_subs, t_count, ht⟩ : ∃ t ⊆ { s | ∃ a, s = Ioi a ∨ s = Iio a },
      t.Countable ∧ ts = generateFrom t :=
    exists_countable_of_generateFrom OrderTopology.topology_eq_generate_intervals
  have A : ∀ s ∈ t, ∃ a, s = Ioi a ∨ s = Iio a := t_subs
  choose! a ha using A
  refine ⟨a '' t, t_count.image _, ?_⟩
  apply le_antisymm
  · apply le_generateFrom_iff_subset_isOpen.2
    simp only [mem_image, exists_exists_and_eq_and, ofPred_subset_ofPred, forall_exists_index,
      and_imp]
    grind [isOpen_Iio', isOpen_Ioi']
  · rw [ht]
    apply generateFrom_anti
    grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ Preorder.topology α ≤ induced f inst✝¹

Tactic:
refine le_of_nhds_le_nhds fun a => ?_

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ 𝓝 a ≤ 𝓝 a
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : 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 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x

Tactic:
erw [equivIccQuot_comp_mk_eq_toIcoMod]

Goal state after:
case right
𝕜 : 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 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ CommGrp.forget C ⋙ toCommGrp C ≅ 𝟭 (CommGrp C)

Tactic:
refine NatIso.ofComponents (fun _ => CommGrp.mkIso (Iso.refl _) ?_ ?_) ?_

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.one ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom = MonObj.one

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul

case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f
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
⊢ (ConcreteCategory.hom (↟((Finsupp.lift (↑M) R X) ⇑(ConcreteCategory.hom f)))) (freeMk x) = (ConcreteCategory.hom f) x

Tactic:
Finsupp.lift_apply,

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (Finsupp.sum (freeMk x) fun x r ↦ r • (ConcreteCategory.hom f) x) = (ConcreteCategory.hom f) x
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.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Tactic:
by rw [← comp_τ₂, S.w₀₂, zero_τ₂]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) ((ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x) = 0

Tactic:
by
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]
  rfl

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }

Tactic:
· intro m hm
      ext
      dsimp only
      rw [← hm]
      simp [beckCoalgebraFork, X.counit]

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✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
← cancel_mono right.hom,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv) ≫ right.hom =
    (left.inv ≫ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) ≫ right.hom