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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ u ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), IsOpen[uniformSpace.toTopologicalSpace] u

pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u

Tactic:
· simp only [mem_iUnion₂, mem_range]
    rintro _ ⟨x, _, k, rfl⟩
    exact isOpen_ball x (hto k)

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f * f') x = 0 x

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ f x * f' x = 0 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f * f') x = 0 x

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x * f' x = 0 x
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 ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
⊢ TendstoLocallyUniformlyOn F f p s

Tactic:
by
  refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_
  obtain ⟨t, ht, htr⟩ := h x hx
  rw [tendstoUniformlyOn_iff_tendsto] at htr
  exact htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ max a 1 / max a⁻¹ 1 = a

Tactic:
rcases le_total a 1 with (h | h) <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuous (S.domRestrict ∘ F) ↔ UniformEquicontinuousOn F S

Tactic:
rw [UniformEquicontinuous, UniformEquicontinuousOn]
  conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]
  rfl

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]
  refine iInf_congr fun i => ?_
  cases i <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ Iic a * Iic b ⊆ Iic (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Iic (a * b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ Ici a * Ici b ⊆ Ici (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ici (a * b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Iic a * Iio b ⊆ Iio (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iio b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Iio (a * b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Iio a * Iic b ⊆ Iio (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Iio a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Iio (a * b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Ioi a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ioi (a * b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ioi b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ioi (a * b)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
rw [uIcc_subset_uIcc_iff_le] at h

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : CommMonoid 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)
⊢ ContinuousMul M

Tactic:
apply ContinuousMul.of_nhds_one hmul hleft

Goal state after:
M : Type u
inst✝¹ : CommMonoid 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)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∅ * V ⊆ U

pp: case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

pp: case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
· exact ⟨univ, by simp⟩

Goal state after:
case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
union_mul

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ 0

Tactic:
simpa using continuous_const

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
x : G
s : Set G
⊢ x ∈ closure[inst✝²] s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
inv_mul_cancel,

Goal state after:
case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / 1
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
inv_mul_cancel,

Goal state after:
case e'_5
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / 1
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
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 ∈ 𝓝 1, ∅ * V ⊆ U

pp: case refine_2
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
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

pp: case refine_3
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
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

pp: case refine_4
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
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
· exact ⟨univ, by simp⟩

Goal state after:
case refine_2
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
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

case refine_3
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
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

case refine_4
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
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case right
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
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
union_mul

Goal state after:
case right
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
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Tactic:
h _,

Goal state after:
case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ (-g) x = g x

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ Disjoint (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) (univ.pi fun i ↦ Ioc (update x i₀ m i) (y i))

Tactic:
rw [disjoint_left]
  rintro z h₁ h₂
  refine (h₁ i₀ (mem_univ _)).2.not_gt ?_
  simpa only [Function.update_self] using (h₂ i₀ (mem_univ _)).1

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
⊢ ∃ x, (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True

Tactic:
apply Exists.intro w

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
hz : z ∈ s ∩ Ioo x y
⊢ z ∈ u ∩ (s ∩ Ioi x)

Tactic:
exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
a : 𝕜
ha : 0 < a
⊢ Ioo 0 a = ((fun i ↦ Inv.inv '' Ioi i) ∘ Inv.inv) a

Tactic:
simp [inv_Ioi₀ (inv_pos.2 ha)]

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:
by
  rw [← inv_atBot₀, inv_inv]

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
nhds_eq_order

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
⊢ ∃ b ∈ Ioc 0 p, ↑b = a

Tactic:
by
  let b := QuotientAddGroup.equivIocMod hp.out 0 a
  exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑((a % ↑n) • p / ↑n)

Tactic:
Int.natMod,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑↑(a % ↑n).toNat / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑((a % ↑n) • p / ↑n)
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom (mk (↟N.subtype)).arrow ∘ₗ ↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv).range

Tactic:
LinearEquiv.range_comp

Goal state after:
case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) = (Hom.hom (mk (↟N.subtype)).arrow).range
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
      (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom

Tactic:
← cancel_epi ((μIso R X Y).inv ▷ _),

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R X Y).inv ▷ (free R).obj Z ≫
      (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (μIso R X Y).inv ▷ (free R).obj Z ≫
      (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
        (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₂'.Exact

Tactic:
by
  rw [← exact_op_iff, exact_iff_of_iso S.L₂'OpIso]
  exact S.op.L₁'_exact

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫ (coreflectorAdjunction R).counit.app (R.obj ((coreflector R).obj X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))

Tactic:
counit_obj_eq_map_counit,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫ R.map ((coreflector R).map ((coreflectorAdjunction R).counit.app X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.μ.app (D.obj j).A ≫ (D.obj j).a =
    T.map (T.map (c.π.app j) ≫ (D.obj j).a) ≫ (D.obj j).a

Tactic:
(D.obj j).assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j) ≫ (D.obj j).a) ≫ (D.obj j).a