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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
have := h.nonempty

Goal state after:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n N : ℕ
H : ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V n
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩

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

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

Tactic:
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs

Goal state after:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∧ (a, b) ∈ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i

Tactic:
mem_prod,

Goal state after:
α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (a b : α), (a ∈ S ∧ b ∈ S) ∧ (a, b) ∈ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, hV, hV'⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ x ∈ univ, f ≤ 𝓝 x

Tactic:
exact ⟨x, mem_univ x, hx⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
iSup_subtype',

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (⨆ x, f ↑x).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
by
  rw [ContinuousWithinAt, tendsto_nhds_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s', (Prod.map (F m.1.1) (F' m.1.2) x, Prod.map (F m.2.1) (F' m.2.2) x) ∈ u

Tactic:
mem_prod,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'), x.1 ∈ s ∧ x.2 ∈ s' → (Prod.map (F m.1.1) (F' m.1.2) x, Prod.map (F m.2.1) (F' m.2.2) x) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p ∈ U N

Tactic:
by
  refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux
  · exact setSeq_mono hf U_mem hm hp.1
  · exact setSeq_mono hf U_mem hn hp.2

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

Goal state before:
pp: case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

pp: case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Tactic:
· intro H
      have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
      obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
      exact ⟨i, hpi, hi.trans interior_subset⟩

Goal state after:
case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ range f ⊆ insert 1 (f '' mulTSupport f)

Tactic:
by
  grw [← subset_mulTSupport f]; exact range_subset_insert_image_mulSupport f

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
⊢ CompleteSpace α

Tactic:
obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
  have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
  refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
  · exact inter_subset_left (seq_pair_mem hf Hmem hm hn)
  · rcases hU'.1 hs with ⟨N, hN⟩
    exact ⟨N, Subset.trans inter_subset_right hN⟩

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

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f • f') x = 0 x

Tactic:
by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun a b ↦ m a (n b)) f g

Tactic:
rw [map₂_swap, map₂_map_left, map₂_swap]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b ↦ n b a) g f) h = map₂ n' (map₂ m' f h) g

Tactic:
map₂_swap n'

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b ↦ n b a) g f) h = map₂ (fun a b ↦ n' b a) g (map₂ m' f h)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
by
  have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
  rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
  rfl

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

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a

Tactic:
← hfg.of_mul_left.le_pure_iff,

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f ≤ pure a
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ioi a = Ioi (a / c)

Tactic:
simpa only [division_def] using! (OrderIso.mulRight₀ c h).preimage_Ioi a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
a✝ : ↑(S i)
⊢ (restrict (S i) (liftCover S φ hφ hS)) a✝ = (φ i) a✝

Tactic:
simp only [restrict_apply, liftCover_coe]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.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 : C(X, Y)
hf : IsQuotientMap ⇑f
g✝ : C(X, Z)
h✝ : FactorsThrough ⇑g✝ ⇑f
g : C(Y, Z)
x✝¹ x✝ : X
h : f x✝¹ = f x✝
⊢ (g.comp f) x✝¹ = (g.comp f) x✝

Tactic:
simp only [ContinuousMap.comp_apply]; rw [h]

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
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsProperMap f
hg : IsProperMap g
⊢ IsProperMap (Prod.map f g)

Tactic:
simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢
  constructor
  -- Continuity is clear.
  · exact hf.1.prodMap hg.1
  -- Let `𝒰 : Ultrafilter (X × Z)`, and assume that `f × g` tends to some `(y, w) : Y × W`
  -- along `𝒰`.
  · intro 𝒰 ⟨y, w⟩ hyw
  -- That means that `f` tends to `y` along `map fst 𝒰` and `g` tends to `w` along `map snd 𝒰`.
    simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw
  -- Thus, by properness of `f` and `g`, we get some `x : X` and `z : Z` such that `f x = y`,
  -- `g z = w`, `map fst 𝒰` tends to  `x`, and `map snd 𝒰` tends to `y`.
    rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using! hyw.1) with
      ⟨x, hxy, hx⟩
    rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using! hyw.2) with
      ⟨z, hzw, hz⟩
  -- By the properties of the product topology, that means that `𝒰` tends to `(x, z)`,
  -- which completes the proof since `(f × g)(x, z) = (y, w)`.
    refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
    rw [nhds_prod_eq, le_prod]
    exact ⟨hx, hz⟩

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
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s / t)

Tactic:
rw [← iUnion_div_right_image]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (⋃ a ∈ t, (fun x ↦ x / a) '' s)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst✝²] t
hs : IsCompact s
⊢ IsClosed[inst✝²] (t * s)

Tactic:
by
  rw [← image_op_smul]
  exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

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

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap, Function.comp_def]
  simp

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

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : ∀ (i : ι), i = a ∨ i ∈ s → UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x

Tactic:
forall_eq_or_imp

Goal state after:
case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
α : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace α
inst✝¹ : Zero α
inst✝ : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst✝⁵, inst✝²] f
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
by
  refine or_iff_not_imp_left.mpr fun h => ?_
  simp_rw [funext_iff, Pi.zero_apply] at h
  push Not at h
  obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h
  have : k ∈ 𝓝 x :=
    mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
  exact IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹)

Tactic:
← map_mul_left_nhds_one₀ hx,

Goal state after:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto Inv.inv (map (fun x_1 ↦ x * x_1) (𝓝 1)) (𝓝 x⁻¹)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x

Tactic:
· ext j
    obtain rfl | hij := eq_or_ne i j
    · exact Function.update_self ..
    · simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using! h j (mem_univ j)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ (𝓝[<] 0)⁻¹ = atBot

Tactic:
rw [← inv_atBot₀, inv_inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ g x * f x) l atBot

Tactic:
exact hg.mul_atBot' hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ ↑e '' (e.source ∩ s) = ↑e' '' (e.source ∩ s)

Tactic:
heq.image_eq

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ ↑e' '' (e.source ∩ s) = ↑e' '' (e.source ∩ s)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'

Tactic:
refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1
  · apply h.2
    rw [s]
    exact mem_univ _
  · apply h.symm'.2
    rw [symm_source, t]
    exact mem_univ _

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

Goal state before:
pp: case pos
α : 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 : α
b : β
hb : b ∈ Iio (f a)
x : α
hx : ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
rcases H₁ hb hx with ⟨y, hya, hyb⟩

Goal state after:
case pos
α : 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 : α
b : β
hb : b ∈ Iio (f a)
x : α
hx : ¬b < f x
y : α
hya : y < a
hyb : b ≤ f y
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : 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 : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
by_cases! h : ∃ x, ¬(f x < b)

Goal state after:
case pos
α : 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 : α
b : β
hb : b ∈ Ioi (f a)
h : ∃ x, ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

case neg
α : 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 : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x✝ : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)

Tactic:
exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : Type u
inst✝ : MonObj A
x : A
⊢ 1 * x = x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (one_mul A) (PUnit.unit, x)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
⊢ (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
convert! gcd_mul_addOrderOf_div_eq p m hn
  rw [h, one_mul]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
h₁ : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
exact addOrderOf_div_of_gcd_eq_one h h₁

Goal state after: