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

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n ↦ u (n + k)

Tactic:
exact h.comp_tendsto (tendsto_add_atTop_nat k)

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
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 α := fun b ↦ Bool.casesOn b s t
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)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ Disjoint (⋃ x, ball (↑x) (B (U false x))) (⋃ x, ball (↑x) (B (U true x)))

Tactic:
have hdj (b : Bool) (x : S b) (y : S (!b)) (hxy : U b x ≤ U (!b) y) :
        Disjoint (ball x.1 (B (U b x))) (ball y.1 (B (U (!b) y))) := by
      rw [Set.disjoint_iff]
      intro z hz
      exact (hU b x).notMem_of_mem_left (mem_ball_comp hz.1 (hB.antitone hxy hz.2)) y.2

Goal state after:
α : 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 α := fun b ↦ Bool.casesOn b s t
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)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : ↑(S b)) (y : ↑(S !b)),
    U b x ≤ U (!b) y → Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))
⊢ Disjoint (⋃ x, ball (↑x) (B (U false x))) (⋃ x, ball (↑x) (B (U true x)))
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιX : Type u_6
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pX : ιX → Prop
sX : ιX → Set X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hl : l.HasBasis pX sX
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∃ j, pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ a ∈ s, (f a, F x a) ∈ sβ i

Tactic:
by
  simp [hβ.tendstoUniformlyOn_iff_of_uniformity, hl.eventually_iff]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
⊢ ∃ i ∈ 𝓤 α, Prod.map mk mk ⁻¹' Prod.map mk mk '' id i ⊆ id U

Tactic:
refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩

Goal state after:
α : Type u
inst✝ : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
x✝¹ : α × α
x₁ x₂ : α
x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' Prod.map mk mk '' id U
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Prod.map mk mk (y₁, y₂) = Prod.map mk mk (x₁, x₂)
⊢ (x₁, x₂) ∈ id U
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.22
β : Type ?u.25
γ : Type ?u.31
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
⊢ Sort ?u.48

Tactic:
by
      haveI := sInf uas; haveI := sInf ubs
      exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2

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

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
exact fun H f hf hfs => ⟨Ultrafilter.of f, Ultrafilter.of_le f,
      (Ultrafilter.of f).cauchy_of_totallyBounded' (H.mono ((Ultrafilter.of_le f).trans hfs))⟩

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

Goal state before:
pp: α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
have :
    (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
      (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
    rw [uniformity_prod_eq_comap_prod]
    exact (𝓤 α).basis_sets.prod_self.comap _

Goal state after:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U ↦ U ∈ 𝓤 α) fun U ↦ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_ofPred_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_ofPred_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsOpen[inst✝¹] s
x : α
hx : x ∈ s
⊢ Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔ Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
by
    rw [hs.nhdsWithin_eq hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : 𝔖 ⊆ 𝔗
s : Set α
x✝ : s ∈ 𝔖
⊢ {s} ⊆ 𝔗

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (fun x ↦ ((⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)

Tactic:
change comap (Prod.map (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)) _ = _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (Prod.map (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
filter_upwards [hs y hys (ball_mem_nhds _ hV)] with i hi

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
hi : i ∈ (fun x ↦ F x y) ⁻¹' ball (f y) V
⊢ (F i x, z) ∈ id U
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = (fun x ↦ a * x) ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
by
  obtain ⟨aU, (haU | haU)⟩ := hU <;>
  simp only [hV, haU, mem_ofPred_eq] <;>
  use a⁻¹ * aU <;>
  rcases lt_or_gt_of_ne hb with (hb | hb)
  · right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
  · right; rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]

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
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
y : ι
hy : y ∈ s'
⊢ F y = F' y

Tactic:
by grind

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

Goal state before:
pp: α : Type u_2
β : Type u_3
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x ↦ c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)

Tactic:
simpa only [inv_smul_smul] using h.const_smul c⁻¹

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
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
⊢ ∀ (i : ι) (x : α), F' i x ∈ s

Tactic:
by grind

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
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
i : ι
hi : i ∈ s'
⊢ (fun i x ↦ g (F i x)) i = (fun i x ↦ g (F' i x)) i

Tactic:
by grind

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

Goal state before:
pp: case inl.inl
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
⊢ closure[inst✝²] (0 • ∅) = 0 • closure[inst✝²] ∅

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

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 • s) = 0 • closure[inst✝²] s
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
rw [key, ← Filter.map_map]

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

Goal state before:
pp: N : Type u_4
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : ContinuousMul N
s t : Set N
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)

Tactic:
rw [← image_mul_prod]
  exact (hs.prod ht).image continuous_mul

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

Goal state before:
pp: case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
x✝ : α
⊢ f x✝ = b⁻¹ * (b * f x✝)

Tactic:
inv_mul_cancel_left

Goal state after:
case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
x✝ : α
⊢ f x✝ = f x✝
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
⊢ c = b⁻¹ * (b * c)

Tactic:
inv_mul_cancel_left

Goal state after:
case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
⊢ c = c
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hg : Tendsto g l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto f l (𝓤 α)

Tactic:
by simpa using hfg.uniformity_mul hg.uniformity_inv

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
⊢ 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)

Tactic:
rw [Homeomorph.comap_nhds_eq]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓝 1 = 𝓝 ((Homeomorph.inv G).symm 1)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b \ update f i '' {b} = Icc (update f i a) (update f i b) \ {update f i b}

Tactic:
image_singleton,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b \ {update f i b} = Icc (update f i a) (update f i b) \ {update f i b}
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b \ update f i '' {a} = Icc (update f i a) (update f i b) \ {update f i a}

Tactic:
image_singleton,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b \ {update f i a} = Icc (update f i a) (update f i b) \ {update f i a}
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b \ update f i '' {a} = Ico (update f i a) (update f i b) \ {update f i a}

Tactic:
image_singleton,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b \ {update f i a} = Ico (update f i a) (update f i b) \ {update f i a}
Module: Mathlib.Topology.Algebra.Order.Group

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

pp: case inr
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)
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

Tactic:
· simp

Goal state after:
case inr
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)
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b
Module: Mathlib.Topology.Order.LeftRightNhds

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

Tactic:
simp [H, (subsingleton_isTop α).countable]

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

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

Tactic:
simpa only [mul_comm] using hg.atTop_mul_pos hC hf

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
f1 : α → Set α := fun a ↦ Ioi a
f2 : α → Set α := fun a ↦ Iio a
s : Set α
hs : s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
⊢ s ∈ range f1 ∪ range f2

Tactic:
by grind

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'
⊢ e = e'

Tactic:
have B : (e.symm : β → α) = e'.symm := by
    ext x
    exact hsymm x

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
⊢ e = e'
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
x₂ : ↑S.X₂
⊢ ∃ a,
    (fun x ↦
          match x with
          | (x₁, x₃) => (ConcreteCategory.hom S.f) x₁ + s x₃)
        a =
      x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])
      exact ⟨⟨x₁, S.g x₂⟩, by simp [hx₁]⟩

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

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

Tactic:
· rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

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

Goal state before:
pp: case h
𝕜 : 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
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ n • y - n • m.1 • p = ↑m.2 • p

Tactic:
sub_eq_iff_eq_add,

Goal state after:
case h
𝕜 : 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
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ n • y = ↑m.2 • p + n • m.1 • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x

Tactic:
rintro ⟨n, rfl⟩

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x

Tactic:
rintro ⟨n, rfl⟩

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ ↑((equivIco p a) x) ∈ Ioc a (a + p)

Tactic:
by grind

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

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))

Tactic:
simp_rw [TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin]

Goal state after:
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, f x ∈ s → ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' s