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

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval i) f ≤ 𝓝 (x i)
⊢ f ≤ 𝓝 x

Tactic:
rwa [nhds_pi, le_pi]

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

Goal state before:
pp: case hmono
α : 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
t' t : Set β
ht't : t' ⊆ t
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u

Tactic:
⟨v, v_mem, hv⟩

Goal state after:
case hmono
α : 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
t' t : Set β
ht't : t' ⊆ t
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case hunion
α : 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
t t' : Set β
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) →
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u

Tactic:
⟨v, v_mem, hv⟩

Goal state after:
case hunion
α : 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
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ (fun a b ↦ m (n a.1 a.2) b) (f ×ˢ g) h = map₂ m' f (map (fun p ↦ n' p.1 p.2) (g ×ˢ h))

Tactic:
map₂_map_right,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ (fun a b ↦ m (n a.1 a.2) b) (f ×ˢ g) h = map₂ (fun a b ↦ m' a (n' b.1 b.2)) f (g ×ˢ h)
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₂ n f g) h = map₂ n' (map₂ m' f h) g

Tactic:
rw [map₂_swap n, map₂_swap n']
  exact map₂_assoc fun _ _ _ => h_right_comm _ _ _

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

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

Tactic:
map₂_map_right,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map₂ (fun a b ↦ n (m a b)) f g = map₂ (fun a b ↦ m' (n₁ a) (n₂ b)) f g
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀

Tactic:
exact hA.closure' (Pi.continuous_domRestrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

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 β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ ∃ x, F ≤ 𝓝 x

Tactic:
use ofFun 𝔖 g

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ F ≤ 𝓝 ((ofFun 𝔖) g)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c : α
⊢ a • Icc b c = Icc (a * b) (a * c)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ

Tactic:
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

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 : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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 c : α
this : ∀ (a_1 : Set α), (fun x ↦ a * x⁻¹) '' a_1 = (fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' a_1
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
ext x

Goal state after:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Ioo a 0)⁻¹ = Iio a⁻¹

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹
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
⊢ ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x

Tactic:
ext x

Goal state after:
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
x : M
⊢ ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) x = x₀ * y₀ * x
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 x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)

Tactic:
by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : (𝓝 1).HasBasis p s
⊢ (𝓝 1).HasBasis p fun i ↦ s i * s i

Tactic:
by
  rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]
  simpa only [← image_mul_prod] using! h.prod_self.map _

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

Goal state before:
pp: case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ↑𝒰 ≤ 𝓝 x

Tactic:
rwa [nhds_pi, le_pi]

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

Goal state before:
pp: case e'_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ ((fun x ↦ b * x) ∘ fun x ↦ a * x) = id

Tactic:
ext x

Goal state after:
case e'_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
x : M
⊢ ((fun x ↦ b * x) ∘ fun x ↦ a * x) x = id x
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
inst✝ : T1Space Y
y : Y
H : CompactSpace X
y' : Y
⊢ IsCompact ((fun x ↦ y) ⁻¹' {y'})

Tactic:
simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
⊢ ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U

Tactic:
ext x

Goal state after:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U ↔ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty} = ⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K

Tactic:
ext x

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
x : ↥S
⊢ x ∈ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty} ↔ x ∈ ⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
intro K L hK hL
      have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
      rw [preimage_compl, compl_compl] at H
      convert! H
      ext x
      simp only [image_smul, mem_ofPred_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
      exact Set.smul_inter_nonempty_iff'

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
⊢ ⇑S.equivOp ⁻¹' {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty} = Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L

Tactic:
ext x

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
x : ↥S
⊢ x ∈ ⇑S.equivOp ⁻¹' {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty} ↔ x ∈ Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = ((fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
⊢ IsClosed[inst✝³] ↑H

Tactic:
have hd : IsDiscrete (H : Set G) := isDiscrete_iff_discreteTopology.mpr ‹_›

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
⊢ IsClosed[inst✝³] ↑H
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: G : Type u
inst✝⁷ : TopologicalSpace G
H : Type v
inst✝⁶ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : Mul M
inst✝² : Mul N
L : Type u_3
inst✝¹ : Mul L
inst✝ : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme1.trans cme2.toMulEquiv).toFun

Tactic:
by convert! Continuous.comp cme2.continuous_toFun cme1.continuous_toFun

Goal state after:
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 = Icc (update f i a) (update f i b)

Tactic:
ext x

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ Icc (update f i a) (update f i b)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x ↦ x ^ (-↑n)) atTop (𝓝 0)

Tactic:
by
  simpa only [zpow_neg, zpow_natCast] using! (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}

Tactic:
by simp_rw [or_comm]

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

Tactic:
ext 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
x : α
⊢ ↑e x = ↑e' x
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.symm = ↑e'.symm

Tactic:
ext 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'
x : β
⊢ ↑e.symm x = ↑e'.symm x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (e.prod e').symm = e.symm.prod e'.symm

Tactic:
ext x

Goal state after:
case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).1 = (↑(e.symm.prod e'.symm) x).1

case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).2 = (↑(e.symm.prod e'.symm) x).2

case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).1 = (↑(e.symm.prod e'.symm).symm x).1

case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).2 = (↑(e.symm.prod e'.symm).symm x).2

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x
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
r : R
c : CharacterModule B
⊢ AddMonoidHom.comp (r • c) f.toAddMonoidHom = (RingHom.id R) r • AddMonoidHom.comp c f.toAddMonoidHom

Tactic:
ext x

Goal state after:
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
r : R
c : CharacterModule B
x : A
⊢ (AddMonoidHom.comp (r • c) f.toAddMonoidHom) x = ((RingHom.id R) r • AddMonoidHom.comp c f.toAddMonoidHom) x
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) ψ
⊢ φ = ψ

Tactic:
ext x

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) ψ
x : B
⊢ φ x = ψ x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ ↑(x + p) = ↑x

Tactic:
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : WellFoundedLT α
s : Set α
h : IsUpperSet s
⊢ IsClosed[inst✝³] s

Tactic:
obtain rfl | ⟨a, rfl⟩ := h.eq_empty_or_Ici

Goal state after:
case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : WellFoundedLT α
h : IsUpperSet ∅
⊢ IsClosed[inst✝³] ∅

case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : WellFoundedLT α
a : α
h : IsUpperSet (Ici a)
⊢ IsClosed[inst✝³] (Ici a)