mathlib-initiative/mathlib-tactics huggingface dataset:
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
hzn : z ∈ n
hz : z ∈ ⋂ j ∈ js, (mulTSupport (f j))ᶜ
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_ofPred_eq, mem_iInter,
        and_imp] at hz

Goal state after:
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
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
by
  obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
  choose U hU T hT hb using fun a ha =>
    exists_mem_nhds_ball_subset_of_mem_nhds ((hf a ha).preimage_mem_nhds <| mem_nhds_left _ ht)
  obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU
  apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)
  rintro ⟨a₁, a₂⟩ h h₁
  obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)
  apply htr
  refine ⟨f a, SetRel.symm t <| hb _ _ _ haU ?_, hb _ _ _ haU ?_⟩
  exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ max (a / c) (b / c) = max a b / c

Tactic:
by
  simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹

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 ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun i ↦ F i a) p (𝓝 (f a))

Tactic:
refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
change _ ≤ _
  simp only [map_le_iff_le_comap, iInf_uniformity]
  exact iInf₂_le s h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
refine ⟨fun {F} hF ↦ ?_⟩
    have := hF.1
    have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
      CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))
    choose! g hg using this
    use ofFun 𝔖 g
    simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]
    intro s hs U ⟨hU, hUc⟩
    rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩
    filter_upwards [hV] with f hf x hx
    refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_
    filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Y₁
inst✝ : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x✝ : C(X₁, Y₁)
⊢ (fun g ↦ { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ }))
      ((fun f ↦ { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ })) x✝) =
    x✝

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Y₁
inst✝ : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x✝ : C(X₂, Y₂)
⊢ (fun f ↦ { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ }))
      ((fun g ↦ { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ })) x✝) =
    x✝

Tactic:
aesop

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 α
inst✝ : TopologicalSpace β
f : β → α
c : G
⊢ (Continuous[inst✝, inst✝⁴] fun x ↦ c • f x) ↔ Continuous[inst✝, inst✝⁴] f

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z (comap f ℱ) (g ∘ f)
⊢ ∃ x, g x = z ∧ ClusterPt x ℱ

Tactic:
rcases hgf.clusterPt_of_mapClusterPt h with ⟨x, rfl, hx⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 ℱ
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space (G ⧸ N) ↔ IsClosed[inst✝²] (mk ⁻¹' {↑1})

Tactic:
MulAction.IsPretransitive.t1Space_iff G (mk 1),

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsClosed[instTopologicalSpace N] {↑1} ↔ IsClosed[inst✝²] (mk ⁻¹' {↑1})
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
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (fun x ↦ (f x.1) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1
hr : ∀ (y : H), ContinuousAt (fun x ↦ (f x) y) 1
x✝ : G × H
x : G
y : H
⊢ ContinuousAt (fun x ↦ (f x.1) x.2) (x, y)

Tactic:
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *

Goal state after:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))
hr : ∀ (y : H), Tendsto (fun x ↦ (f x) y) (𝓝 1) (𝓝 ((f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x ↦ (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ Tendsto (fun x_1 ↦ (f x) y * (f x_1.1) y * ((f x) x_1.2 * (f x_1.1) x_1.2)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f x) y))
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
l : Filter α
f : G → α
⊢ Tendsto (fun x ↦ f x⁻¹) atBot l ↔ Tendsto f atTop l

Tactic:
by
  simp [← Function.comp_def, Tendsto, ← map_map, map_inv_atBot]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op ⁻¹' V * K ⊆ op ⁻¹' op '' U
⊢ op ⁻¹' V * K ⊆ U

Tactic:
preimage_image_eq _ op_injective

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op ⁻¹' V * K ⊆ U
⊢ op ⁻¹' V * K ⊆ U
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x : G₀
l : Filter α
f : α → G₀
hx : x ≠ 0
⊢ Tendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Tactic:
simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝ : Group α
_t : TopologicalSpace α := ⊥
⊢ Continuous[instTopologicalSpaceProd, _t] fun p ↦ p.1 * p.2

Tactic:
have := discreteTopology_bot α
        fun_prop

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
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)

Tactic:
have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
aesop

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
aesop

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}

Tactic:
aesop

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f b ≤ f x) x}

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : NonAssocRing R
inst✝ : SeparatelyContinuousMul R
⊢ Continuous[inst✝², inst✝²] fun a ↦ -a

Tactic:
by simpa using continuous_id.const_mul (-1 : R)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
simp_rw [forall_mem_comm]

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ (a b : β), a ∈ U₂ → b ∈ U₂ → (φ (b - a)) y₁ ∈ W'
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
inst✝² : IsTopologicalRing K
inst✝¹ : CompactSpace K
inst✝ : T2Space K
⊢ Finite K

Tactic:
suffices DiscreteTopology K by
    exact finite_of_compact_of_discrete
  rw [discreteTopology_iff_isOpen_singleton_zero]
  exact GroupWithZero.isOpen_singleton_zero

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
have : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[<] b, s ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE

Tactic:
simpa using! TFAE_mem_nhdsGT h.dual (ofDual ⁻¹' s)

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

Tactic:
convert! (config := { preTransparency := .default })
    nhdsGT_eq_bot_iff (a := OrderDual.toDual a) using 4
  exact ofDual_covBy_ofDual_iff

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

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, ts] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
OrderTopology.topology_eq_generate_intervals,

Goal state after:
α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, Preorder.topology α] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ (∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝] (f ⁻¹' s)) ↔
    ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑e.symm.symm.symm ⁻¹' e'.source

Tactic:
rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
⊢ e.source ∩ ↑e' ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s

Tactic:
source_eq he

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
⊢ e'.source ∩ ↑e' ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
Module: Mathlib.Algebra.Category.Grp.EnoughInjectives

Goal state before:
pp: A_ : AddCommGrpCat
⊢ (fun i ↦ { down := i 0 }) = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EnoughInjectives

Goal state before:
pp: A_ : AddCommGrpCat
⊢ ∀ (x y : ↑A_),
    { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun x +
        { toFun := fun a i ↦ { down := i a }, map_zero' := ⋯ }.toFun y

Tactic:
aesop

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

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] B
⊢ ∀ (x y : CharacterModule B),
    AddMonoidHom.comp (x + y) f.toAddMonoidHom =
      AddMonoidHom.comp x f.toAddMonoidHom + AddMonoidHom.comp y f.toAddMonoidHom

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: ⊢ (of PUnit.{u + 1}).isFinite

Tactic:
by rw [prop_isFinite_iff]; infer_instance

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

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (c + c').toAddMonoidHom ⋯) 0 = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) 0

Tactic:
aesop

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

Goal state before:
pp: case refine_2
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B),
    (liftAddHom (c + c').toAddMonoidHom ⋯) (x ⊗ₜ[R] y) =
      (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) (x ⊗ₜ[R] y)

Tactic:
aesop

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

Goal state before:
pp: case refine_3
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    (liftAddHom (c + c').toAddMonoidHom ⋯) x = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) x →
      (liftAddHom (c + c').toAddMonoidHom ⋯) y = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) y →
        (liftAddHom (c + c').toAddMonoidHom ⋯) (x + y) =
          (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) (x + y)

Tactic:
aesop

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

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    (liftAddHom (r • c).toAddMonoidHom ⋯) x = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) x →
      (liftAddHom (r • c).toAddMonoidHom ⋯) y = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) y →
        (liftAddHom (r • c).toAddMonoidHom ⋯) (x + y) = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) (x + y)

Tactic:
aesop

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

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
x✝ : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ ((uncurry ∘ₗ curry) x✝) 0 = (LinearMap.id x✝) 0

Tactic:
aesop

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

Goal state before:
pp: case refine_2
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
x✝ : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ ∀ (x : A) (y : B), ((uncurry ∘ₗ curry) x✝) (x ⊗ₜ[R] y) = (LinearMap.id x✝) (x ⊗ₜ[R] y)

Tactic:
aesop

Goal state after: