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

Goal state before:
pp: case hFs
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ ∀ᶠ (n : ι) in p, MapsTo (F n) univ t

Tactic:
simpa [MapsTo]

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

Goal state before:
pp: case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
rcases comp_symm_of_uniformity hu with ⟨u', u'_mem, u'_symm, hu'⟩
    intro x hx
    obtain ⟨v, hv, w, hw, hvw⟩ :
      ∃ v ∈ 𝓝[s] q, ∃ w ∈ 𝓝[k] x, v ×ˢ w ⊆ f.uncurry ⁻¹' {z | (f q x, z) ∈ u'} :=
        mem_nhdsWithin_prod_iff.1 (hf (q, x) ⟨hq, hx⟩ (mem_nhds_left (f q x) u'_mem))
    refine ⟨w, hw, v, hv, fun p hp y hy ↦ ?_⟩
    have A : (f q x, f p y) ∈ u' := hvw (⟨hp, hy⟩ : (p, y) ∈ v ×ˢ w)
    have B : (f q x, f q y) ∈ u' := hvw (⟨mem_of_mem_nhdsWithin hq hv, hy⟩ : (q, y) ∈ v ×ˢ w)
    exact hu' <| SetRel.prodMk_mem_comp (u'_symm A) B

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ⇑toFun)

Tactic:
change _ ≤ _
  rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
  exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ i, uniformSpace α γ

Tactic:
ext : 1

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ uniformSpace α β =
    UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓
      UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)

Tactic:
ext : 1

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_3.inl
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₁
⊢ (toFun (f, g).1 (φ₁ y), toFun (f, g).2 (φ₁ y)) ∈ U

pp: case refine_3.inr
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₂
⊢ (toFun (f, g).1 (φ₂ y), toFun (f, g).2 (φ₂ y)) ∈ U

Tactic:
· exact hfg.1 y

Goal state after:
case refine_3.inr
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₂
⊢ (toFun (f, g).1 (φ₂ y), toFun (f, g).2 (φ₂ y)) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ uniformSpace α β = ⨅ i, UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)

Tactic:
ext : 1

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
by
  rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}
huf : Tendsto id u (𝓝 f)
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Tactic:
UniformOnFun.tendsto_iff_tendstoUniformlyOn

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}
huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun x ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
let Γ₀ := {γ : Γ | ((γ • ·) '' V ∩ V).Nonempty ∧ γ • x ≠ x}

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun x ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
h : ContinuousAt (t.domRestrict (f i)) ⟨x, hx⟩
hi : i ∈ l
⊢ Tendsto (fun b ↦ f i ↑b) (𝓝 ⟨x, hx⟩) (𝓝 (f i ↑⟨x, hx⟩))

Tactic:
exact h

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_clusterPt]
  -- Let `ℱ : Filter X` and `y` some cluster point of `map f ℱ`.
    refine ⟨H.1, fun ℱ y hy ↦ ?_⟩
  -- That means that the singleton `pure y` meets the "closure" of `map f ℱ`, by which we mean
  -- `Filter.lift' (map f ℱ) closure`. But `f` is closed, so
  -- `closure (map f ℱ) = map f (closure ℱ)` (see `IsClosedMap.lift'_closure_map_eq`).
  -- Thus `map f (closure ℱ ⊓ 𝓟 (f ⁻¹' {y})) = map f (closure ℱ) ⊓ 𝓟 {y} ≠ ⊥`, hence
  -- `closure ℱ ⊓ 𝓟 (f ⁻¹' {y}) ≠ ⊥`.
    rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy
  -- Now, applying the compactness of `f ⁻¹' {y}` to the nontrivial filter
  -- `closure ℱ ⊓ 𝓟 (f ⁻¹' {y})`, we obtain that it has a cluster point `x ∈ f ⁻¹' {y}`.
    rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y})) inf_le_right with ⟨x, hxy, hx⟩
    refine ⟨x, hxy, ?_⟩
  -- In particular `x` is a cluster point of `closure ℱ`. Since cluster points of `closure ℱ`
  -- are exactly cluster points of `ℱ` (see `clusterPt_lift'_closure_iff`), this completes
  -- the proof.
    rw [← clusterPt_lift'_closure_iff]
    exact hx.mono inf_le_left

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure[inst✝²] {1} = closure[inst✝²] K

Tactic:
apply Subset.antisymm ?_ ?_

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure[inst✝²] {1} ⊆ closure[inst✝²] K

G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] K ⊆ K * closure[inst✝²] {1}
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

Tactic:
have ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1) := by
      rw [← one_mul 1]
      refine .mul ?_ ?_
      · rw [uniformity_eq_comap_inv_mul_nhds_one]
        exact tendsto_comap.comp tendsto_fst
      · rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
        exact tendsto_comap.comp tendsto_snd

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Module: Mathlib.Order.Filter.AtTopBot.Field

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

Tactic:
by
  rcases lt_trichotomy r 0 with (hr | rfl | hr)
  · simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_neg]
  · simp [not_tendsto_const_atTop]
  · simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_pos]

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

Goal state before:
pp: G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ IsTopologicalGroup.rightUniformSpace G = u

Tactic:
ext : 1

Goal state after:
G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ 𝓤 G = 𝓤 G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
x : G
hL1 : L ∈ 𝓝 ((Homeomorph.mulLeft x) ((Homeomorph.mulLeft x).symm 1))
⊢ (range (denseSeq G) ∩ (fun y ↦ x * y) ⁻¹' L).Nonempty

Tactic:
exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)

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
⊢ UniformSpace.comap op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G

Tactic:
ext : 1

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓤 G = 𝓤 G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformSpace.comap op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G

Tactic:
ext : 1

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓤 G = 𝓤 G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G) = IsTopologicalGroup.rightUniformSpace G

Tactic:
ext : 1

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓤 G = 𝓤 G
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 : ι
b : α i
⊢ update f i '' Ioc (f i) b = Ioc f (update f i b)

Tactic:
by simpa using image_update_Ioc f i (f i) b

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)

Tactic:
uIcc,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = Icc (update f i a ⊓ update f i b) (update f i a ⊔ update f i b)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ IsTopologicalGroup.rightUniformSpace G = us

Tactic:
ext : 1

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ IsTopologicalGroup.leftUniformSpace G = us

Tactic:
ext : 1

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) =
    (⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | x⁻¹ < a / a_1}) ⊓ ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | a / a_1 < x}

Tactic:
refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) = ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | a / a_1 < x}

case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 1), 𝓟 {a_1 | x⁻¹ < a / a_1}
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : ↑e = f
g : β → α
hg : ↑e.symm = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ e.copy f hf g hg s hs t ht = e

Tactic:
by
  subst f g s t
  cases e
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
e' : β ≃ γ
f'' : PartialEquiv γ δ
⊢ (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Tactic:
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc, trans_toPartialEquiv]

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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
⊢ dual 0 = 0

Tactic:
ext f
  exact map_zero f

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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ φ (f y) = ψ (f y)

Tactic:
change (dual f) φ _ = (dual f) ψ _

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) φ) y = ((dual f) ψ) y
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIocDiv hp a =ᶠ[𝓝[>] x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
by
  simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]
  apply Ioc_mem_nhdsGT_of_mem
  rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ (equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = (equivIco p a).toFun ((equivIco p a).invFun ⟨y, hy⟩)

Tactic:
exact h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : (equivIoc p a) ↑x = (equivIoc p a) ↑y
⊢ (equivIoc p a).toFun ((equivIoc p a).invFun ⟨x, hx⟩) = (equivIoc p a).toFun ((equivIoc p a).invFun ⟨y, hy⟩)

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ (𝟭 (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)).map f ≫
      (isoOfComponents (fun x ↦ Y✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom =
    (isoOfComponents (fun x ↦ X✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom ≫ (laxBraidedToCommMon C ⋙ commMonToLaxBraided C).map f

Tactic:
ext ⟨⟨⟩⟩; dsimp; simp

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ (Icc a (a + p)).domRestrict f ⟨a, ⋯⟩ = (Icc a (a + p)).domRestrict f ⟨a + p, ⋯⟩

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ π ≫ γ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ

Tactic:
rw [hz]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ z ≫ S.homologyπ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
hi : 0 + 2 ≤ 2
⊢ S.map' 0 (0 + 1) ⋯ ⋯ ≫ S.map' (0 + 1) (0 + 2) ⋯ hi = 0

Tactic:
exact h

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
hi : 0 + 2 ≤ 2
⊢ (S.sc hS 0 hi).Exact

Tactic:
exact h

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

Goal state before:
pp: case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
j : ι
⊢ (hom (limit.π (wideCospan B X f) (some j))) x = (hom (limit.π (wideCospan B X f) (some j))) y

Tactic:
apply h

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
a : J.L
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.left a))) x =
    (hom (limit.π I.multicospan (WalkingMulticospan.left a))) y

Tactic:
apply h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (S.map (restrictScalars f)).f)
    ⇑(ConcreteCategory.hom (S.map (restrictScalars f)).g)

Tactic:
exact h

Goal state after: