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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
key,

Goal state after:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))
Module: Mathlib.Topology.Algebra.Monoid

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

Tactic:
by
  obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one
  obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)
  by_cases H : ∃ x ≠ 0, x ∈ W
  · obtain ⟨x, hx, hxW⟩ := H
    cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))
  · obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
    simpa [isOpen_iff_mem_nhds]

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 (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
nhds_eq_comap_uniformity,

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

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

Tactic:
nhds_eq_comap_uniformity,

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ⇑f
⊢ IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f

Tactic:
· apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (fun p ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
by
  simp [Cauchy, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x ↦ a * x) (𝓝 1) = 𝓝 a

Tactic:
map_mul_left_nhds₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 (a * 1) = 𝓝 a
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case refine_1
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.toFun

pp: case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun

Tactic:
· simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace]

Goal state after:
case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a / F m.1 a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a * (F m.1 a)⁻¹ ∈ u_1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a * (f a)⁻¹ ∈ u_1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Group G
u : UniformSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ u_1 ∈ 𝓝 1, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (Filter.map mk (𝓝 1)).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
⊢ CompleteSpace (G ⧸ N)

Tactic:
rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
⊢ CompleteSpace (G ⧸ N)
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 : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * (g x)⁻¹) l (𝓝 0)
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 : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * (g x)⁻¹) l (𝓝 0)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * (g x)⁻¹) l (𝓝 0)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
    exact isOpen_iUnion fun i => isOpen_Ioo

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ inst✝³ = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_2
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

Tactic:
set c' : Cocone F :=
      { pt := AddCommGrpCat.of (ULift (AddCircle (1 : ℚ)))
        ι :=
          { app j := AddCommGrpCat.ofHom (((@AddEquiv.ulift _ _).symm.toAddMonoidHom.comp χ).comp
                       (Quot.ι F j))
            naturality {j j'} u := by
              ext
              dsimp
              rw [Quot.map_ι F (f := u)] } }
    use AddEquiv.ulift.toAddMonoidHom.comp (hc.desc c').hom
    refine Quot.addMonoidHom_ext _ (fun j x ↦ ?_)
    dsimp
    rw [Quot.ι_desc]
    change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') x) = _
    rw [hc.fac]
    dsimp [c']
    rw [AddEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : MonCat
⊢ (MonoidalCategoryStruct.whiskerRight (↾fun x ↦ 1) ↑A ≫ ↾fun p ↦ p.1 * p.2) =
    (MonoidalCategoryStruct.leftUnitor ↑A).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : MonCat
⊢ (MonoidalCategoryStruct.whiskerLeft (↑A) (↾fun x ↦ 1) ≫ ↾fun p ↦ p.1 * p.2) =
    (MonoidalCategoryStruct.rightUnitor ↑A).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ (↾fun x ↦ 1) ≫ ↾⇑(hom f) = ↾fun x ↦ 1

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: X✝ Y✝ : MonCat
f : X✝ ⟶ Y✝
⊢ (↾fun p ↦ p.1 * p.2) ≫ ↾⇑(hom f) = MonoidalCategoryStruct.tensorHom (↾⇑(hom f)) (↾⇑(hom f)) ≫ ↾fun p ↦ p.1 * p.2

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : MonCat} (f : X ⟶ Y),
    (inverse ⋙ functor).map f ≫
        (let __src := Equiv.refl (inverse.obj Y).X;
            { toEquiv := __src, map_mul' := ⋯ }).toMonCatIso.hom =
      (let __src := Equiv.refl (inverse.obj X).X;
            { toEquiv := __src, map_mul' := ⋯ }).toMonCatIso.hom ≫
        (𝟭 MonCat).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : Mon (Type u)} (f : X ⟶ Y),
    (functor ⋙ forget MonCat).map f ≫ (Iso.refl ((functor ⋙ forget MonCat).obj Y)).hom =
      (Iso.refl ((functor ⋙ forget MonCat).obj X)).hom ≫ (Mon.forget (Type u)).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : CommMonCat} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        (let __src := Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj Y).X;
            { toEquiv := __src, map_mul' := ⋯ }).toCommMonCatIso.hom =
      (let __src := Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj X).X;
            { toEquiv := __src, map_mul' := ⋯ }).toCommMonCatIso.hom ≫
        (𝟭 CommMonCat).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp

Goal state before:
pp: ⊢ ∀ {X Y : GrpCat} (f : X ⟶ Y),
    (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).map f ≫
        (let __src := Equiv.refl ↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj Y);
            { toEquiv := __src, map_mul' := ⋯ }).toGrpIso.hom =
      (let __src := Equiv.refl ↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj X);
            { toEquiv := __src, map_mul' := ⋯ }).toGrpIso.hom ≫
        (𝟭 GrpCat).map f

Tactic:
cat_disch

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

Goal state before:
pp: case ofNat
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.ofNat a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.natAbs_natCast] at h ⊢
    exact addOrderOf_div_of_gcd_eq_one hn h

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

Goal state before:
pp: ⊢ ∀ {X Y : CommGrpCat} (f : X ⟶ Y),
    (CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).map f ≫
        (let __src :=
              Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj Y);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom =
      (let __src := Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj X);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom ≫
        (𝟭 CommGrpCat).map f

Tactic:
cat_disch

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2
          exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ η ≫ Multiplicative.toAdd.toIso.hom =
    Functor.LaxMonoidal.ε (F ⋙ forget AddCommGrpCat) ≫ (F ⋙ forget AddCommGrpCat).map η

Tactic:
cat_disch

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

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x

pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x

Tactic:
on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f

Tactic:
cat_disch

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝] (liftIoc p a f)

Tactic:
rw [liftIoc_eq_lift_Icc hf]
  refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun
  exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_domRestrict.mp hc)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ : ShortComplex C
⊢ mapToComposableArrows (𝟙 S₁) = 𝟙 S₁.toComposableArrows

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
ψ : S₂ ⟶ S₃
⊢ mapToComposableArrows (φ ≫ ψ) = mapToComposableArrows φ ≫ mapToComposableArrows ψ

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ S.map' i j ⋯ ⋯ ≫ S.map' j k ⋯ hk = 0

Tactic:
subst hij hjk

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.IsComplex
i : ℕ
hk : i + 1 + 1 ≤ n
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (S.sc' ⋯ i j k hij hjk hk).Exact

Tactic:
subst hij hjk

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
i : ℕ
hk : i + 1 + 1 ≤ n
⊢ (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ hk).Exact