mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
rcases hK.ultrafilter_le_nhds _ h𝒰 with ⟨y, hyK, hy⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.2 / x.1) (𝓝 1)

Tactic:
simp_rw [div_eq_mul_inv]
  exact uniformity_eq_comap_mul_inv_nhds_one Gᵣ

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i ↦ {y | y * x⁻¹ ∈ s i}

Tactic:
exact hb.comap _

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

Goal state before:
pp: G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
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
hf : ContinuousAt (fun x ↦ (f x.1) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1
hr : ∀ (y : H), ContinuousAt (fun x ↦ (f x) y) 1
x✝ : G × H
x : G
y : H
⊢ ContinuousAt (fun x ↦ (f x.1) x.2) (x, y)

Tactic:
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *
  refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
  simp only [map_one, mul_one, MonoidHom.one_apply]

Goal state after:
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)
conj_φ : conj ∘ ⇑φ = dr
x✝ : β × β
⊢ (snd ∘ ⇑φ) x✝ = dl x✝

Tactic:
simp [φ, dl]

Goal state after:
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₁
φ_ψ_conj : φ = g * ψ * g⁻¹
ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
exact φ_ψ_conj ▸ ψ_tendsto.conj_nhds_one g

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 1, p x
⊢ ∀ᶠ (x : α) in 𝓝 1, ∀ (g : α), p (g * x * g⁻¹)

Tactic:
simpa using tendsto_conj_nhds_one.eventually hp

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 ↦ r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]

Goal state after:
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:
have : IsCompact (S ×ˢ S.op) := hS.prod (opHomeomorph.isCompact_preimage.mp hS)

Goal state after:
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
S : Submonoid α
hS : IsCompact ↑S
this : IsCompact (↑S ×ˢ ↑S.op)
⊢ IsCompact ↑S.units
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f g : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous[inst✝, inst✝³] fun x ↦ f x / g x

Tactic:
by
  simpa only [div_eq_mul_inv] using! hf.mul (hg.inv₀ h₀)

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

Goal state before:
pp: case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
h_nhds

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' ∅ = ∅

Tactic:
image_empty

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ∅ = ∅
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ((PartialEquiv.refl α).trans e).source = e.source

Tactic:
by simp [trans_source, preimage_id]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Tactic:
simp only [hx, mfld_simps]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ IsTopologicalBasis {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}

Tactic:
by
  refine IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_
  · rintro u ⟨f, g, hfc, hgc, hf_fin, hg_fin, rfl⟩
    apply IsOpen.inter
    · apply hf_fin.isOpen_biInter (fun i hi ↦ ?_)
      rw [h]
      exact isOpen_generateFrom_of_mem ⟨i, hfc hi, Or.inl rfl⟩
    · apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)
      rw [h]
      exact isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩
  simp only [exists_and_left, image_subset_iff, preimage_ofPred_eq, ofPred_subset_ofPred, and_imp]
  intro k k_fin hk
  let kl := {s ∈ k | ∃ a ∈ c, s = Ioi a}
  let kr := {s ∈ k | ∃ a ∈ c, s = Iio a}
  have k_eq : k = kl ∪ kr := by
    -- this `have` can be removed, but makes `grind` slower
    have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
    ext
    grind
  have : Finite kl := k_fin.subset (by simp [k_eq])
  have : Finite kr := k_fin.subset (by simp [k_eq])
  have Al : ∀ s : kl, ∃ a ∈ c, s = Ioi a := fun s ↦ s.2.2
  choose al alc hal using Al
  have Ar : ∀ s : kr, ∃ a ∈ c, s = Iio a := fun s ↦ s.2.2
  choose ar arc har using Ar
  refine ⟨range al, by simp [range_subset_iff, alc], range ar,
    by simp [range_subset_iff, arc], finite_range _, finite_range _, ?_⟩
  rw [k_eq, sInter_eq_biInter, biInter_union, biInter_range, biInter_range, biInter_eq_iInter,
    biInter_eq_iInter]
  simp [hal, har]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x - toIcoDiv hp a x • p ∈ Ico a (a + p)

Tactic:
← toIcoDiv_eq_iff

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIcoDiv ?hp a x = toIcoDiv hp a x

case hp
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ 0 < p
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case neg
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0

Tactic:
apply CharacterModule.int.divByNat_self

Goal state after:
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
this : s ⊆ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
⊢ (⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}).Countable

Tactic:
refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_

Goal state after:
α : 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
this : s ⊆ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen[inst✝³] a
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}
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

Tactic:
choose! z hz using this

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}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : CommMonCat
x y : ↑A
⊢ (hom
          ((β_ (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X
                (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X).hom ≫
            μ)).toFun
      (x, y) =
    (hom μ).toFun (x, y)

Tactic:
exact CommMonoid.mul_comm y x

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 β := ⋯
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
A : (f '' s).PairwiseDisjoint fun x ↦ Ioo x (z (invFunOn f s x))
⊢ ∀ x ∈ f '' s, x < z (invFunOn f s x)

Tactic:
rintro _ ⟨y, ys, rfl⟩

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}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
A : (f '' s).PairwiseDisjoint fun x ↦ Ioo x (z (invFunOn f s x))
y : β
ys : y ∈ s
⊢ f y < z (invFunOn f s (f y))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q.num / ↑q.den * p) = (Rat.divInt q.num ↑q.den).den

Tactic:
Rat.num_divInt_den,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q.num / ↑q.den * p) = q.den
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: A : CommGrpCat
x y : ↑A
⊢ (hom
          ((β_ (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X
                (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X).hom ≫
            μ)).toFun
      (x, y) =
    (hom μ).toFun (x, y)

Tactic:
exact CommMonoid.mul_comm y x

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ (β_ (F.obj M) (F.obj M)).hom ≫ LaxMonoidal.μ F M M ≫ F.map μ = LaxMonoidal.μ F M M ≫ F.map μ

Tactic:
rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidal.μ F A.X A.X ≫ F.map μ = LaxMonoidal.μ F A.X A.X ≫ F.map μ

Tactic:
rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ ↑(Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩).liftOn (fun x ↦ ↑↑x) ⋯))) = ↑⟨a, ⋯⟩

Tactic:
apply congr_arg Subtype.val
          ((equivIco p a).right_inv ⟨a, le_refl a, lt_add_of_pos_right a hp.out⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommGrp_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidal.μ F A.X A.X ≫ F.map μ = LaxMonoidal.μ F A.X A.X ≫ F.map μ

Tactic:
rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Goal state after:
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:
rw [isColimit_iff_bijective_desc, ← Function.Bijective.of_comp_iff _
          (quotQuotUliftAddEquiv F).bijective, ← AddEquiv.coe_toAddMonoidHom,
          ← AddMonoidHom.coe_comp, Quot.desc_quotQuotUliftAddEquiv]

Goal state after:
J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective ⇑(AddEquiv.ulift.symm.toAddMonoidHom.comp (Quot.desc F c))
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ f.f₂.τ₁ ≫ S₂.v₂₃.τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ

Tactic:
naturality_φ₁_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ functorP.map f ≫ S₂.φ₁ ≫ S₂.v₂₃.τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case neg
J : MultispanShape
a b : J.R
h : ¬a = b
⊢ Subsingleton (right a ⟶ right b)

Tactic:
have : IsEmpty (right a ⟶ right b) := ⟨by rintro ⟨⟩; simp at h⟩

Goal state after:
case neg
J : MultispanShape
a b : J.R
h : ¬a = b
this : IsEmpty (right a ⟶ right b)
⊢ Subsingleton (right a ⟶ right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case one
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.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one

Tactic:
· apply Fan.IsLimit.hom_ext hd
          simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.η.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
t.fac,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.η.app c.pt ≫ (newCone D c).π.app j = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

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

Tactic:
t.fac,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ (newCone D c).π.app j = s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

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

Tactic:
t.fac,

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.inv 0 ⋯ = α.inv ≫ F.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]
    dsimp
    rw [comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    (T.map (c.ι.app j) ≫ lambda c t) ≫ t.desc (T.forget.mapCocone s)

Tactic:
t.fac,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (T.map (c.ι.app j) ≫ lambda c t) ≫ t.desc (T.forget.mapCocone s)
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
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
A : PreservesLimit F R := preservesLimit_of_createsLimit_and_hasLimit F R
⊢ R.obj (limit.cone F).1 ≅ c.pt
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (c.ι.app j ≫ t.desc (newCocone D c)) ≫ T.map (t.desc (T.forget.mapCocone s)) =
    (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a

Tactic:
t.fac,

Goal state after:
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (newCocone D c).ι.app j ≫ T.map (t.desc (T.forget.mapCocone s)) = (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a