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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ s

Tactic:
refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
k : ℕ
⊢ u k ∈ s
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
by
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i ↦ UniformOnFun.gen 𝔖 S (s i)

Tactic:
simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (comap (Prod.map S.domRestrict S.domRestrict) (𝓤 (↑S → β))).HasBasis p fun i ↦
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ (fun a b ↦ m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
exact map_map₂_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
uniformContinuous_iff_le_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun x2 ↦ 1 • x2) f = f

Tactic:
simp_rw [one_smul, map_id']

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (𝓝 0 ×ˢ map Prod.snd l) (𝓝 0)

pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (map Prod.fst l ×ˢ 𝓝 0) (𝓝 0)

Tactic:
· apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_snd hl

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (map Prod.fst l ×ˢ 𝓝 0) (𝓝 0)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : x ∈ closure[inst✝²] U
⊢ x ∈ U * U

Tactic:
rw [mem_closure_iff_nhds] at hx

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ x ∈ U * U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hg : Tendsto g l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto f l (𝓤 α)

Tactic:
simpa using hfg.uniformity_mul hg.uniformity_inv

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.1⁻¹ * x.2) (𝓝 1)

Tactic:
rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap,
      ← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_right, ← 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.Topology.Algebra.Group.Basic

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

Tactic:
rw [← hconj x₀]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x ↦ x * x₀) (map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1))
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
h : Tendsto f l atBot
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ 0 < r

Tactic:
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]

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₀ : α
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

Tactic:
have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) =
      e ∘ fun t : β × β => t.2 / t.1 := by
    ext t
    simp
  have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
    simpa using! (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)
  simpa using! de.tendsto_comap_nhds_nhds lim comm

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

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

Tactic:
ofPred_true,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ (univ ∩ univ.pi fun i ↦ Ioc (x i) (y i)) = univ.pi fun i ↦ Ioc (x i) (y i)
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
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
rw [← IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace] at hG ⊢

Goal state after:
G : Type u
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
e' : β ≃ γ
f'' : PartialEquiv γ δ
⊢ (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Tactic:
by
  simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc, trans_toPartialEquiv]

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

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
x₂ : ↑S.X₂
x₁ : ↑S.X₁
hx₁ : (ConcreteCategory.hom S.f) x₁ = x₂ - s ((ConcreteCategory.hom S.g) x₂)
⊢ (fun x ↦
        match x with
        | (x₁, x₃) => (ConcreteCategory.hom S.f) x₁ + s x₃)
      (x₁, (ConcreteCategory.hom S.g) x₂) =
    x₂

Tactic:
by simp [hx₁]

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

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
hφ :
  Function.Surjective fun x ↦
    match x with
    | (x₁, x₃) => (ConcreteCategory.hom S.f) x₁ + s x₃
⊢ Finite ↑S.X₂

Tactic:
exact Finite.of_surjective _ hφ

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

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Ioi '' s ∪ Iio '' s ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
simp only [union_subset_iff, image_subset_iff]
    exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩

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

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∀ (c : CharacterModule A), c a = 0
⊢ a = 0

Tactic:
by
  contrapose! h; exact exists_character_apply_ne_zero_of_ne_zero h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * addOrderOf (m • ↑(p / ↑n)) = n

Tactic:
IsOfFinAddOrder.addOrderOf_nsmul

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * (addOrderOf ↑(p / ↑n) / (addOrderOf ↑(p / ↑n)).gcd m) = n

case h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)
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 = (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫ μ

Tactic:
dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]

Goal state after:
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
⊢ (𝟙
          ((MonTypeEquivalenceMon.inverse.obj
                ((forget₂ GrpCat MonCat).obj ((forget₂ CommGrpCat GrpCat).obj (toCommGrp.obj (F.obj X))))).X ⊗
            (MonTypeEquivalenceMon.inverse.obj
                ((forget₂ GrpCat MonCat).obj ((forget₂ CommGrpCat GrpCat).obj (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫ μ
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 𝕜
x : Quot (EndpointIdent p a)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b

Tactic:
rintro _ _ ⟨_⟩
      exact (coe_add_period p a).symm

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 𝕜
x : Quot (EndpointIdent p a)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b

Tactic:
by
      rintro _ _ ⟨_⟩
      exact (coe_add_period p a).symm

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
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      (Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
          (forget AddCommGrpCat).map (Functor.LaxMonoidal.μ F X X)) ≫
        (forget AddCommGrpCat).map
          (F.map (SemiCartesianMonoidalCategory.fst X X) + F.map (SemiCartesianMonoidalCategory.snd X X))

Tactic:
Category.assoc,

Goal state after:
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
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map (Functor.LaxMonoidal.μ F X X) ≫
          (forget AddCommGrpCat).map
            (F.map (SemiCartesianMonoidalCategory.fst X X) + F.map (SemiCartesianMonoidalCategory.snd X X))
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

Tactic:
revert x

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
          ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨x, hx⟩)) =
        Quot.mk (EndpointIdent p a) ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this : S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
⊢ ∀ {X Y : Free R C} (f : X ⟶ Y), F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f

Tactic:
by
      intro X Y f
      induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']

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.ε.app X.A) ≫ X.a

Tactic:
Category.assoc,

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 ≫ X.a
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_1
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
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ ((Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f) ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
Category.assoc,

Goal state after:
case refine_1
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
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_2
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
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ ((Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g) ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
Category.assoc,

Goal state after:
case refine_2
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
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
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 = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
i : ℕ
hi : i < 1
⊢ i = 0

Tactic:
simpa using hi

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
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ adj.unit ≫ i.hom ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)

Tactic:
rw [← assoc]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)