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

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
obtain ⟨n, hn, hnf⟩ := hlf x

Goal state after:
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝² : UniformSpace β
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), (𝓤 (α i)).IsCountablyGenerated
⊢ (𝓤 ((i : ι) → α i)).IsCountablyGenerated

Tactic:
rw [Pi.uniformity]
  infer_instance

Goal state after:
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 ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoLocallyUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s

Tactic:
tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoLocallyUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) p
⊢ TendstoUniformlyOn F f p s
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)

Tactic:
by
  simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
    @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ _ F f univ p

Goal state after:
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 ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ TendstoLocallyUniformlyOn G f p s

Tactic:
have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2) := by
    simpa using eventually_prod_principal_iff.2 hg

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ TendstoLocallyUniformlyOn G f p s
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ

Tactic:
UniformFun.iInf_eq

Goal state after:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsUniformInducing ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)

Tactic:
constructor
    change
      comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _))
          _ = _
    simp_rw [UniformFun]
    rw [← uniformity_comap]
    congr
    unfold instUniformSpaceProd
    rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
    have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
    rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ i, UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) ((fun i ↦ uniformSpace α (δ i)) i)) =
    uniformSpace α ((i : ι) → δ i)

Tactic:
UniformFun.iInf_eq

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ i, UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) ((fun i ↦ uniformSpace α (δ i)) i)) =
    ⨅ i, uniformSpace α ((i : ι) → δ i)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
      (fun x ↦
        (((ofFun 𝔖).symm.trans
              ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
            x.1,
          ((ofFun 𝔖).symm.trans
              ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
            x.2))
      (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))) =
    𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
uniformity_prod,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
      (fun x ↦
        (((ofFun 𝔖).symm.trans
              ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
            x.1,
          ((ofFun 𝔖).symm.trans
              ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
            x.2))
      (comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 (α →ᵤ[𝔖] β)) ⊓ comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 (α →ᵤ[𝔖] γ))) =
    𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
⊢ T1Space α ↔ IsClosed[inst✝⁴] {x}

Tactic:
refine ⟨fun H ↦ isClosed_singleton, fun hx ↦ ⟨fun y ↦ ?_⟩⟩
  rcases MulAction.exists_smul_eq G x y with ⟨g, rfl⟩
  rw [← image_singleton, image_smul]
  exact hx.smul _

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Tactic:
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
  exact continuous_mul.tendsto _

Goal state after:
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
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i ↦ f i x) ⊆ ↑I

Tactic:
rcases hf x₀ with ⟨U, hxU, hUf⟩
  refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩
  rw [hUf.coe_toFinset]
  exact ⟨y, hi, hy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)

Tactic:
← tendsto_id'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ Tendsto ((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) 𝓕 (𝓤 α)

Tactic:
← tendsto_id'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) 𝓕 (𝓤 α)
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ -f x * -g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ Tendsto f l atTop

Tactic:
by
  simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr

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

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)

Tactic:
simpa using h.mul A

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 : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
s : Set α
hs : TotallyBounded s⁻¹
⊢ TotallyBounded s

Tactic:
by simpa using hs.inv

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

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

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

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

Tactic:
obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
x : B
⊢ φ x = ψ x

Tactic:
obtain ⟨y, rfl⟩ := hf x

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ φ (f y) = ψ (f y)
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
h0 : 0 ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Tactic:
have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S = (Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h ≫ ↟T.subtype)).range

Tactic:
ofMkLEMk_comp

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S = (Hom.hom (↟S.subtype)).range
Module: Mathlib.CategoryTheory.Abelian.Refinements

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

Tactic:
exact epi_of_epi_fac fac.symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

Tactic:
rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ T.map X.a ≫ T.ε.app (T.obj X.A)

Tactic:
reassoc_of% h₁,

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ T.δ.app X.A ≫ T.ε.app (T.obj X.A)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ 𝟙 (F.obj ⟨i, ⋯⟩) ≫ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i i ⋯ hj'

Tactic:
G.map'_self i,

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ 𝟙 (F.obj ⟨i, ⋯⟩) ≫ app ⟨i, ⋯⟩ = app ⟨i, ⋯⟩ ≫ 𝟙 (G.obj ⟨i, ⋯⟩)
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✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) =
      (match X with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) ≫
        ((Functor.const (WalkingMultispan J)).obj P).map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _) <;> dsimp <;>
          simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]
        symm
        apply w

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
G : Comonad C
X : G.adj.toComonad.Coalgebra
⊢ X.a ≫ G.δ.app X.A = X.a ≫ G.map X.a

Tactic:
simpa using X.coassoc

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
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (fun f ↦ equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯)
      ((fun f ↦ { f := (adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))), h := ⋯ }) f) =
    f

Tactic:
apply equalizer.hom_ext

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
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (fun f ↦ equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯)
        ((fun f ↦ { f := (adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))), h := ⋯ })
          f) ≫
      equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: case refine_2
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
h : (comparison adj).obj B ⟶ B'
⊢ (comparisonRightAdjointHomEquiv adj B' A) ((comparison adj).map g ≫ h) =
    g ≫ (comparisonRightAdjointHomEquiv adj B' B) h

Tactic:
apply equalizer.hom_ext

Goal state after:
case refine_2
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
h : (comparison adj).obj B ⟶ B'
⊢ (comparisonRightAdjointHomEquiv adj B' A) ((comparison adj).map g ≫ h) ≫
      equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A)) =
    (g ≫ (comparisonRightAdjointHomEquiv adj B' B) h) ≫ equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A))
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B)

Tactic:
apply equalizer.hom_ext

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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)) =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B) ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))
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
R : D ⥤ C
inst✝¹ : MonadicRightAdjoint R
inst✝ : PreservesColimitsOfShape J R
this : PreservesColimitsOfShape J (monadicLeftAdjoint R) :=
  monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape._proof_1 R
⊢ PreservesColimitsOfShape J (monadicLeftAdjoint R ⋙ R)

Tactic:
by
    apply CategoryTheory.Limits.comp_preservesColimitsOfShape _ _

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ -s • t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]
  exact image2_image_left_comm neg_smul

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
and_iff_right bot_le

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) ∈ I

Tactic:
by convert! I.mul_mem_left (s ^ n * x) h; ring

Goal state after: