mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
x✝ : M
⊢ x✝ ∈ U ↔ x✝ ∈ (fun m' ↦ m' * m⁻¹) ⁻¹' ↑(MulAction.stabilizer M x)

Tactic:
simp [← smul_smul, U, eq_inv_smul_iff.mpr hm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = (fun x ↦ a * x) ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU <;>
  simp only [hV, haU, mem_ofPred_eq] <;>
  use a⁻¹ * aU <;>
  rcases lt_or_gt_of_ne hb with (hb | hb)
  · right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
  · right; rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ ⋃ i ∈ I, range (ψ S i) = univ

Tactic:
simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover

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
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
⊢ IsProperMap f

Tactic:
refine ⟨hf, fun ℱ y h ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
⊢ IsOpen[inst✝³] {0}

Tactic:
obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one

Goal state after:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
⊢ IsOpen[inst✝³] {0}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))
hr : ∀ (y : H), Tendsto (fun x ↦ (f x) y) (𝓝 1) (𝓝 ((f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x ↦ (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ Tendsto (fun x_1 ↦ (f x) y * (f x_1.1) y * ((f x) x_1.2 * (f x_1.1) x_1.2)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f x) y))

Tactic:
refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)

Goal state after:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))
hr : ∀ (y : H), Tendsto (fun x ↦ (f x) y) (𝓝 1) (𝓝 ((f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x ↦ (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ 𝓝 ((f x) y * (f 1) y * ((f x) 1 * (f 1) 1)) = 𝓝 ((f x) y)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
x✝ : β × β
⊢ (conj ∘ ⇑φ) x✝ = dr x✝

Tactic:
simp [conj, φ, dr]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ comap (fun x ↦ (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α

Tactic:
nth_rw 1 [← uniformity_translate_mul a, comap_map]
      rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩
      simp only [Prod.mk.injEq, mul_left_inj, imp_self]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
⊢ h ∈ ↑H → ∀ ⦃y : G⦄, y ∈ ↑H → h ≠ y → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h y

Tactic:
h_in

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
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
⊢ ∀ ⦃y : G⦄, y ∈ ↑H → h ≠ y → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h y
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ (n + 1)) a = f a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
let ee := fun u : β × β => (e u.1, e u.2)

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ 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'

Tactic:
let ee := fun u : β × β => (e u.1, e u.2)

Goal state after:
α : 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
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ 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'
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : 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₀ : γ
this :
  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₀))) ≤
    𝓝 0
⊢ map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓤 G

Tactic:
rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_eq]

Goal state after:
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 β
U_nhds : ∃ t ∈ 𝓝 x₀, ⇑e ⁻¹' t ⊆ U
V : Set δ
V_nhds : V ∈ comap (⇑f) (𝓝 y₀)
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'
⊢ 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:
rcases U_nhds with ⟨U', U'_nhds, U'_sub⟩

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 δ
V_nhds : V ∈ comap (⇑f) (𝓝 y₀)
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
⊢ 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₀)))
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]

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 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 ↦ x * x_1) (𝓝 0) ⊓ comap (fun x_1 ↦ x * x_1) (𝓟 (Ioi 0)) = 𝓝 0 ⊓ 𝓟 (Ioi 0)

Tactic:
comap_principal,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 ↦ x * x_1) (𝓝 0) ⊓ 𝓟 ((fun x_1 ↦ x * x_1) ⁻¹' Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₃

Tactic:
have := hS.epi_g

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Epi S.g
⊢ P S.X₃
Module: Mathlib.CategoryTheory.ObjectProperty.Extensions

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : P.IsClosedUnderExtensions
F : D ⥤ C
inst✝³ : HasZeroMorphisms D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
S✝ : ShortComplex D
hS : S✝.ShortExact
h₁ : P.inverseImage F S✝.X₁
h₃ : P.inverseImage F S✝.X₃
this : Mono S✝.f
⊢ P.inverseImage F S✝.X₂

Tactic:
have := hS.epi_g

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : P.IsClosedUnderExtensions
F : D ⥤ C
inst✝³ : HasZeroMorphisms D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
S✝ : ShortComplex D
hS : S✝.ShortExact
h₁ : P.inverseImage F S✝.X₁
h₃ : P.inverseImage F S✝.X₃
this✝ : Mono S✝.f
this : Epi S✝.g
⊢ P.inverseImage F S✝.X₂
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩

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}
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

Tactic:
have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y := fun x hx ↦ hx.2

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}
this : ∀ x ∈ s, ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ ↑a = 0 ↔ a = 0

Tactic:
have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out
  have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]
  rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ EqOn f g (QuotientAddGroup.mk '' Ico a (a + p))

Tactic:
rintro - ⟨x, hx, rfl⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ f ↑x = g ↑x
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 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f ↑x = g ↑x
⊢ EqOn f g (QuotientAddGroup.mk '' Ioc a (a + p))

Tactic:
rintro - ⟨x, hx, rfl⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f ↑x = g ↑x
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ f ↑x = g ↑x
Module: Mathlib.Algebra.Category.Grp.Ulift

Goal state before:
pp: J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))

Tactic:
isColimit_iff_bijective_desc,

Goal state after:
J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c))
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f

Tactic:
· intro _ A a
    exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (equivPullbackObj hc) x = (equivPullbackObj hc) y

Tactic:
ext <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (h.isLimit.conePointUniqueUpToIso
          ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
      x₁ =
    (h.isLimit.conePointUniqueUpToIso
          ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
      y₁

Tactic:
ext <;> assumption

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

Goal state before:
pp: case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ (hom (ι f default)) ((hom (f default)) y) = (hom (head f)) y

Tactic:
simp only [← arrow_ι _ default, ConcreteCategory.comp_apply]

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✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
⊢ (comparison adj).IsEquivalence

Tactic:
by
    have : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X) := by
      intro X
      apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).counit.app X).f
        rw [comparisonAdjunction_counit_f]
        exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
          (counitLimitOfPreservesEqualizer X)).isIso_inv
    have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by
      intro Y
      rw [comparisonAdjunction_unit_app]
      change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
      · infer_instance
      have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) := by
        apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
        · rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)
        · rw [← G.map_id]
          simp
      apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
      apply reflectsLimit_of_reflectsIsomorphisms
    exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j

Tactic:
simp [Coalgebra.counit (D.obj j)]

Goal state after: