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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformSpace.comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₁)) (UniformFun.uniformSpace (↑i) β))) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformSpace.comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₂)) (UniformFun.uniformSpace (↑i) β)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β)) ⊓
      UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β))

Tactic:
← UniformSpace.comap_comap

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₁)) ∘ ⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₂)) ∘ ⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β) ≤
    UniformSpace.comap ((fun x ↦ x ∘ ψ₁ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
      UniformSpace.comap ((fun x ↦ x ∘ ψ₂ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ Ici a ^ (n + 2) = Ici (a ^ (n + 2))

Tactic:
simp [pow_succ _ n.succ, Ici_pow_eq, Ici_mul_Ici_eq]

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

Goal state before:
pp: case refine_2
α : 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)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i,
      ⨅ i_1 ∈ 𝔗 i,
        UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖))
          (UniformSpace.comap (⇑UniformFun.ofFun ∘ i_1.domRestrict ∘ ⇑(toFun (𝔗 i)))
            (UniformFun.uniformSpace (↑i_1) β)) ≤
    ⨅ i,
      UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β))

Tactic:
← UniformSpace.comap_comap

Goal state after:
case refine_2
α : 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)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i,
      ⨅ i_1 ∈ 𝔗 i,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i_1.domRestrict ∘ ⇑(toFun (𝔗 i))) ∘ ⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i_1) β) ≤
    ⨅ i,
      UniformSpace.comap ((fun x ↦ x ∘ ψ S i) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n x✝ : ℕ
ihn : (a ^ x✝) ⤳ (b ^ x✝)
⊢ (a ^ x✝.succ) ⤳ (b ^ x✝.succ)

Tactic:
simpa only [pow_succ] using ihn.mul h

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

Goal state before:
pp: G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.ofNat n) ⤳ (y ^ Int.ofNat n)

Tactic:
simpa using h.pow n

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
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
by
      intro K L hK hL
      have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
      rw [preimage_compl, compl_compl] at H
      convert! H
      ext x
      simp only [image_smul, mem_ofPred_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
      exact Set.smul_inter_nonempty_iff'

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x

Tactic:
simpa only [inv_inv] using! tendsto_inv₀ (inv_ne_zero hx)

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝ : Group α
_t : TopologicalSpace α := ⊥
⊢ Continuous[instTopologicalSpaceProd, _t] fun p ↦ p.1 * p.2

Tactic:
have := discreteTopology_bot α

Goal state after:
G : Type w
H : Type x
α : Type u
β : Type v
inst✝ : Group α
_t : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Continuous[instTopologicalSpaceProd, _t] fun p ↦ p.1 * p.2
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G)) (UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G))

Tactic:
← UniformSpace.comap_comap

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) ∘ ⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G)
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
n : ℕ
a : A
⊢ (f ^ n) a = f a ^ n

Tactic:
by
  induction n
  case zero => rw [pow_zero, pow_zero, one_toFun]
  case succ n ih => 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
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
⊢ ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) = ⇑e ∘ fun t ↦ t.2 / t.1

Tactic:
ext t

Goal state after:
α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
t : β × β
⊢ ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) t = (⇑e ∘ fun t ↦ t.2 / t.1) t
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := ⋯
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
⊢ s ∩ Ioo x y ⊆ u ∩ (s ∩ Ioi x)

Tactic:
intro z hz

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
hz : z ∈ s ∩ Ioo x y
⊢ z ∈ u ∩ (s ∩ Ioi x)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
have : IsTopologicalGroup.rightUniformSpace G = us := by
    ext : 1
    rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
  rw [← this] at hG
  infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)

Tactic:
by gcongr <;> apply min_le_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s :=
      exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Goal state after:
case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
l : α
lx : l < x
hl : Ioc l x ⊆ s
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
· obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s :=
      exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩

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

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : (↑n).den = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ a = 0

Tactic:
Rat.den_intCast,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 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
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable

Tactic:
have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
    intro x hx
    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
    simpa only [IsBot, not_forall, not_le] using hx.right.right.right

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
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
this : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
hy : n • y = ↑(f x) • p
y' : 𝕜
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'

Tactic:
rw [eq, ← hy', hn.eq_iff] at hy

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑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)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ico a (a + p)
⊢ ↑((equivIco p a) ↑y) = y

Tactic:
by
  have : equivIco p a y = ⟨y, hy⟩ := (equivIco p a).right_inv ⟨y, hy⟩
  simp [this]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ 0 ▷ X ≫ (fst X X + snd X X) = (λ_ X).hom

Tactic:
by simp [← leftUnitor_hom]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk ((ConcreteCategory.hom (α_ X Y Z).hom) ((((x, y), z).1.1, ((x, y), z).1.2), ((x, y), z).2)) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
CategoryTheory.associator_hom_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact

Tactic:
· obtain _ | i := i
      · exact h.exact 0
      · exact h₀.exact i

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ (S.sc ⋯ i hi✝).Exact

Tactic:
· exact h'.exact 0

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0

Tactic:
liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z = x₁ ≫ S₁.f
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext
    apply Comonad.right_counit

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.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
Functor.map_comp,

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.pt.a ≫ T.map s.ι.f ≫ T.map (T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
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 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
rw [← cancel_mono right.hom, assoc, assoc, w, right.inv_hom_id, left.inv_hom_id_assoc]
    apply comp_id

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) ≫ desc S = S.ι.app (WalkingMultispan.left a)

Tactic:
← K.w (WalkingMultispan.Hom.fst a),

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a))) ≫ desc S =
    S.ι.app (WalkingMultispan.left a)
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.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j) ≫ (D.obj j).a) ≫ (D.obj j).a

Tactic:
Functor.map_comp,

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.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    (T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a) ≫ (D.obj j).a
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : WalkingReflexivePair
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
cases f <;> cases g <;> cases h <;> rfl

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 : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)

Tactic:
Functor.map_comp,

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 : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
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
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map ((D.obj j).a ≫ c.ι.app j) ≫ lambda c t

Tactic:
Functor.map_comp,

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
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = (T.map (D.obj j).a ≫ T.map (c.ι.app j)) ≫ lambda c t