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

Goal state before:
pp: case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)

Goal state after:
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
⊢ T2Space (Quotient (MulAction.orbitRel Γ T))

Tactic:
let := MulAction.orbitRel Γ T
  set Q := Quotient (MulAction.orbitRel Γ T)
  rw [t2Space_iff_nhds]
  let f : T → Q := Quotient.mk'
  have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
  rintro ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀)
  change ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
  have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
  obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
  obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
  let bad_Γ_set := { γ : Γ | ((γ • ·) '' K₀ ∩ L₀).Nonempty }
  have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
  choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
  let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ
  let U₀ := U₀₀ ∩ K₀
  let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ
  let V₀ := V₀₀ ∩ L₀
  have U_nhds : f '' U₀ ∈ 𝓝 (f x₀) := by
    refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
    exact (continuous_const_smul _).continuousAt (hu γ)
  have V_nhds : f '' V₀ ∈ 𝓝 (f y₀) :=
    f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩
  rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ
  by_cases H : γ ∈ bad_Γ_set
  · exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩
  · rintro ⟨-, h'⟩
    simp only [bad_Γ_set, image_smul, not_nonempty_iff_eq_empty, mem_ofPred_eq] at H
    exact eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩

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

Goal state before:
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 V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

Tactic:
use V ∩ W, inter_mem V_in W_in

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 ∪ t) * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ ↑hUf.toFinset

Tactic:
rw [hUf.coe_toFinset]

Goal state after:
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i ↦ f i y
⊢ i ∈ {i | ((fun i ↦ mulSupport (f i)) i ∩ U).Nonempty}

Tactic:
exact ⟨y, hi, hy⟩

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
f_cont : Continuous[inst✝², inst✝¹] f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})

Tactic:
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous[inst✝², inst✝¹] f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)

Tactic:
rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x ↦ x * x₀⁻¹) (map (fun x ↦ x₀ * x) (𝓝 1)) = 𝓝 1

Tactic:
← hleft,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x ↦ x * x₀⁻¹) (𝓝 x₀) = 𝓝 1
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 : (⇑S.subtype ⁻¹' (((fun p ↦ p.1 * p.2) ∘ fun p ↦ (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ.Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H

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
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
· simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_pos]

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

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

Tactic:
use V ∩ W, inter_mem V_in W_in

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 ∪ t) * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
S : Submonoid α
hS : IsCompact ↑S
⊢ IsCompact ↑S.units

Tactic:
by
  have : IsCompact (S ×ˢ S.op) := hS.prod (opHomeomorph.isCompact_preimage.mp hS)
  exact isClosedEmbedding_embedProduct.isCompact_preimage this

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
⊢ 𝓤 G = 𝓤 G

Tactic:
change comap (fun (x : G × G) ↦ (Equiv.inv G x.1, Equiv.inv G x.2))
      (comap (fun p : G × G => p.1⁻¹ * p.2) (𝓝 1)) =
    comap (fun p : G × G => p.2 * p.1⁻¹) (𝓝 1)

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ comap (fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ (({z | z i₀ ≤ m} ∪ {z | m < z i₀}) ∩ univ.pi fun i ↦ Ioc (x i) (y i)) = univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
← ofPred_or,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ({a | a i₀ ≤ m ∨ m < a i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) = univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by
  have := hf.atTop_mul_pos (neg_pos.2 hC) hg.neg
  simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

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

Goal state before:
pp: case e_a
𝕜 : 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) = 𝓝 0

Tactic:
refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_

Goal state after:
case e_a
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 ((Homeomorph.mulLeft₀ x ⋯).symm 0) = 𝓝 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ 𝓝 a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), 𝓟 (Ioo l u)

Tactic:
by
  simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]; rfl

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0
⊢ a = 0

Tactic:
erw [ofSpanSingleton, LinearMap.toAddMonoidHom_coe, LinearMap.comp_apply,
     intSpanEquivQuotAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
    AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_apply_one,
    AddCircle.coe_eq_zero_iff] at h

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst✝³] a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
x : α
hx : x ∈ s
⊢ x ∈ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}

Tactic:
rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩

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)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
this : ⟨x, hx⟩ = ⟨y, hy⟩
⊢ x = y

Tactic:
exact Subtype.mk.inj this

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

Tactic:
let s := {x ∈ t | ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}

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}
⊢ {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 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : ↑x = ↑y
this : ⟨x, hx⟩ = ⟨y, hy⟩
⊢ x = y

Tactic:
exact Subtype.mk.inj this

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
⊢ atTop.IsCountablyGenerated

pp: case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ atTop.IsCountablyGenerated

Tactic:
· obtain ⟨s, s_count, hs⟩ := exists_countable_dense α
    have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_ofPred_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy
    rw [this]
    exact ⟨_, s_count.image _, rfl⟩

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ atTop.IsCountablyGenerated
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) = N

Tactic:
convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1

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

case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
by
  rw [equivIccQuot_comp_mk_eq_toIcoMod]
  funext x
  by_cases h : a ≡ x [PMOD p]
  · simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
    exact Quot.sound EndpointIdent.mk
  · simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : Free R C
f : (W ⟶ X) →₀ R
g : (X ⟶ Y) →₀ R
h : (Y ⟶ Z) →₀ R
⊢ ((f.sum fun f' s ↦ g.sum fun g' t ↦ single (f' ≫ g') (s * t)).sum fun f' s ↦
      h.sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    f.sum fun f' s ↦
      (g.sum fun f' s ↦ h.sum fun g' t ↦ single (f' ≫ g') (s * t)).sum fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
simp [sum_sum_index, add_mul, mul_add, Category.assoc, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t ↦ single (a ≫ g') (0 * t)) = 0

Tactic:
simp [add_mul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t ↦ single (a ≫ g') (b₁ * t)) + sum g fun g' t ↦ single (a ≫ g') (b₂ * t)

Tactic:
simp [add_mul]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑((↑eN.symm ∘ₗ f) ∘ₗ ↑eM) ⇑(↑eL.symm ∘ₗ g ∘ₗ ↑eN)

Tactic:
rwa [LinearEquiv.precomp_exact_iff_exact, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
⊢ { l //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
have h₁ : s.ι.f ≫ (T : C ⥤ C).map X.a = s.ι.f ≫ T.δ.app X.A :=
      congr_arg Comonad.Coalgebra.Hom.f s.condition
    have h₂ : s.pt.a ≫ (T : C ⥤ C).map s.ι.f = s.ι.f ≫ T.δ.app X.A := s.ι.h
    refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
    · dsimp
      rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]
      dsimp
      rw [Category.comp_id, Category.assoc, ← T.counit_naturality,
        reassoc_of% h₁, Comonad.left_counit]
      simp
    · ext
      simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using! h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A)
    · intro m hm
      ext
      dsimp only
      rw [← hm]
      simp [beckCoalgebraFork, X.counit]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
k : ℕ
hk : k < n + 1 + 1
hjk : ⟨j, hj⟩ ≤ ⟨k, hk⟩
⊢ map F f ⟨i, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨i, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
cases i

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : ⟨j, hj⟩ ≤ ⟨k, hk⟩
hi : 0 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : ⟨j, hj⟩ ≤ ⟨k, hk⟩
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

Tactic:
apply Cofan.IsColimit.hom_ext hc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
⊢ ∀ (i : J.L),
    c.inj i ≫ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
      c.inj i ≫ I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero

Tactic:
apply Cofan.IsColimit.hom_ext hc

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (i : J.L),
    c.inj i ≫ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
      c.inj i ≫ (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : ⟨j, hj⟩ ≤ ⟨k, hk⟩
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
· obtain _ | j := j
    · simp [Fin.ext_iff] at hij
    · obtain _ | k := k
      · simp [Fin.ext_iff] at hjk
      · dsimp
        rw [← F.map_comp, homOfLE_comp]

Goal state after: