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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
  simp only [Prod.forall]
  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 y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Iic (a * b)

Tactic:
exact mul_le_mul' hya hzb

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 y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 ↦ x1 * x2) y z ∈ Ici (a * b)

Tactic:
exact mul_le_mul' hya hzb

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

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

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

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

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

Tactic:
rintro ⟨habx, hxac⟩

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
habx : a * b ≤ x
hxac : x ≤ a * c
⊢ x ∈ a • Icc b c
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹

Tactic:
by rw [← Filter.inv_le_inv_iff, inv_inv]

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:
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
⊢ {a} ∈ f
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1.refine_2
α : 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
⊢ g ≤ pure b

Tactic:
le_pure_iff

Goal state after:
case refine_1.refine_2
α : 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
⊢ {b} ∈ g
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {1} = 1

Tactic:
singleton_one

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ 1 = 1
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
s : Set X
hs : s ∈ 𝓝 0
⊢ univ • s = univ

Tactic:
refine Set.eq_univ_of_forall fun x ↦ ?_

Goal state after:
G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
s : Set X
hs : s ∈ 𝓝 0
x : X
⊢ x ∈ univ • s
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
inv_Ioo_0_right (inv_neg''.2 ha),

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ Iio a = Iio a⁻¹⁻¹
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₂ * r₁ = 1

Tactic:
symm
    simpa using h₂.mul h₁

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

Goal state before:
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 : M
hx : x ∈ K
this : U ∈ map (fun p ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 0)
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
mem_map,

Goal state after:
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 : M
hx : x ∈ K
this : (fun p ↦ p.1 * p.2) ⁻¹' U ∈ 𝓝 x ×ˢ 𝓝 0
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
⊢ Tendsto (fun x ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)

Tactic:
have := calc
    (𝓝 0).coprod (𝓝 0) ⊓ l
    _ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l :=
      inf_le_inf_left _ le_prod_map_fst_snd
    _ ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 :=
      coprod_inf_prod_le _ _ _ _
  apply (Tendsto.sup _ _).mono_left this
  · apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_snd hl
  · apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_fst hl

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ ∃ V, IsOpen[inst✝²] V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
by
  have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
    tendsto_mul (by simpa only [one_mul] using! hs)
  simpa only [prod_subset_iff] using! exists_nhds_square this

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

Goal state before:
pp: M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
rw [← sInf_range]
  exact continuousMul_sInf (Set.forall_mem_range.mpr h')

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (x : Y), {x}ᶜ ∈ map f (cocompact X)

Tactic:
mem_map,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (x : Y), f ⁻¹' {x}ᶜ ∈ cocompact X
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)

Tactic:
← h

Goal state after:
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 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₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto (((fun x ↦ x.2 * x.1⁻¹) ∘ fun x ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
simpa [Function.comp_def, div_eq_mul_inv, ← mul_assoc]

Goal state after:
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 : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atBot

Tactic:
by
  simp [div_eq_mul_inv, tendsto_mul_const_atTop_of_neg, hr]

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

Goal state before:
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 : G
hx : x ∈ K
this : U ∈ map (fun p ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 1)
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
mem_map,

Goal state after:
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 : G
hx : x ∈ K
this : (fun p ↦ p.1 * p.2) ⁻¹' U ∈ 𝓝 x ×ˢ 𝓝 1
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ t, K ⊆ ⋃ x ∈ t, interior ((fun x_1 ↦ x * x_1) ⁻¹' V)

Tactic:
by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
    rwa [mem_preimage, inv_mul_cancel_right]

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
⊢ ContinuousAt Inv.inv x

Tactic:
have hx' := inv_ne_zero 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
⊢ ContinuousAt Inv.inv x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ W' ∈
    map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))

Tactic:
mem_map,

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1) ⁻¹' W' ∈
    comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))
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 : α
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
⊢ s ∩ Ioo x y ⊆ u ∩ (s ∩ Ioi x)

Tactic:
intro z

Goal state after:
α : 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 : α
⊢ z ∈ s ∩ Ioo x y → z ∈ u ∩ (s ∩ Ioi x)
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
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)

Tactic:
rw [← this] at hG

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
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)
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
this : IsTopologicalGroup.leftUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)

Tactic:
rw [← this] at hG

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
this : IsTopologicalGroup.leftUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
by
  dsimp [μIso, freeMk]
  erw [finsuppTensorFinsupp'_single_tmul_single]
  rw [mul_one]

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

Goal state before:
pp: J : MultispanShape
a : WalkingMultispan J
⊢ ∀ (a_1 : a ⟶ a), a_1 = 𝟙 a

Tactic:
rintro ⟨⟩; rfl

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

Goal state before:
pp: case left.right.fst
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.fst l }
T₂ : Type := { u // J.snd l = J.fst l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.fst l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.fst l

pp: case left.right.snd
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.snd l }
T₂ : Type := { u // J.snd l = J.snd l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.snd l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.snd l

Tactic:
· exact ⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩

Goal state after:
case left.right.snd
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.snd l }
T₂ : Type := { u // J.snd l = J.snd l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.snd l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.snd l
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (m ≫ ↟(LinearMap.fst R ↑M ↑N))).prod (Hom.hom (m ≫ ↟(LinearMap.snd R ↑M ↑N))))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero

Tactic:
apply Fan.IsLimit.hom_ext hc
          simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B) ≫ G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

Tactic:
adj.right_triangle_components

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
⊢ I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)) = I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y))

Tactic:
have := c.condition ⟨⟨y, x⟩, hxy⟩
      dsimp at this ⊢
      rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj ((𝟭 D).obj A.1))

Tactic:
adj.right_triangle_components

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ 𝟙 (G.obj A.A) = 𝟙 (G.obj ((𝟭 D).obj A.1))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: case e_a
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
    equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a

Tactic:
exact (equalizer.condition _ _).symm

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso ((comparisonAdjunction adj).unit.app Y)

Tactic:
comparisonAdjunction_unit_app

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y))