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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
⊢ ∃ x, F ≤ 𝓝 x

Tactic:
have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
      CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this✝ : F.NeBot
this : ∀ x ∈ ⋃₀ 𝔖, ∃ y, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 y)
⊢ ∃ x, F ≤ 𝓝 x
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0

Tactic:
by
    rw [pow_zero]
    exact one_mem_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
⊢ IsClosed[topologicalSpace α β 𝔖] {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_
  rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf
  exact (huf s hs).continuousOn <| Eventually.frequently <| hu fun _ ↦ Continuous.continuousOn

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)

Tactic:
Set.preimage_const_mul_Ioi₀ _ hb,

Goal state after:
case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ Ioi (aU / a) = Ioi (a⁻¹ * aU)
Module: Mathlib.Topology.Algebra.ConstMulAction

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

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

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

Goal state before:
pp: M : Type u
inst✝¹ : CommMonoid 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)
x₀ : M
⊢ 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

Tactic:
hleft x₀

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

Goal state before:
pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
by
  set l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β)) with l_def
  set K : Set (M × M) := (insert 0 (range f)) ×ˢ (insert 0 (range g))
  have K_compact : IsCompact K := .prod (hf.isCompact_insert_range_of_cocompact f_cont)
    (hg.isCompact_insert_range_of_cocompact g_cont)
  have K_mem_l : K ∈ l := eventually_map.mpr <| .of_forall fun ⟨x, y⟩ ↦
    ⟨mem_insert_of_mem _ (mem_range_self _), mem_insert_of_mem _ (mem_range_self _)⟩
  have l_compact : Disjoint l (cocompact (M × M)) := by
    rw [disjoint_cocompact_right]
    exact ⟨K, K_mem_l, K_compact⟩
  have l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0) := by
    rw [l_def, ← coprod_cocompact]
    exact hf.prodMap_coprod hg
  exact tendsto_mul_nhds_zero_of_disjoint_cocompact l_compact l_le_coprod |>.comp tendsto_map

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure[inst✝²] {1}
⊢ False

Tactic:
rw [ht] at this

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ f x ^ 0

Tactic:
simp_rw [pow_zero]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ 1
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
  convert! h.div_const' b⁻¹ with k <;> rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]

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 : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ Tendsto f l atBot

Tactic:
by
  simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr

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 : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atTop

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_neg, hr]

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

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

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

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

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
inst✝ : Preorder α
s : Set α
x✝ : α
x : s.Nonempty
h : IsLUB s x✝
⊢ IsLUB (id '' s) (id x✝)

Tactic:
simpa only [image_id] using! h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ (𝓝[>] 0)⁻¹ = atTop

Tactic:
← inv_atTop₀,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ atTop⁻¹⁻¹ = atTop
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y, y ∈ ↑e '' e.source ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)

Tactic:
exists_mem_image

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ x, x ∈ e.source ∧ p (↑e x)) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)

Tactic:
by
  rw [e.trans_source', e.symm_image_target_inter_eq]

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_1 : 𝕜) in 𝓝[>] x, x_1 ∈ Ioc (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)

Tactic:
apply Ioc_mem_nhdsGT_of_mem

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
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}
⊢ {x | ∃ y, x ⋖ y}.Countable

Tactic:
have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
this : ∀ x ∈ s, ∃ y, x ⋖ y
⊢ {x | ∃ y, x ⋖ y}.Countable
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ (Hom.hom (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit))) 1 = (Hom.hom (𝟙 (𝟙_ (ModuleCat R)))) 1

Tactic:
simp [free]

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 + 2)
⊢ S.Exact ↔ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
by
  constructor
  · intro h
    constructor
    · rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0
      exact h.exact 0 (by lia)
    · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
        (fun i hi => h.exact (i + 1))
  · rintro ⟨h, h₀⟩
    refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
    · obtain _ | i := i
      · exact h.toIsComplex.zero 0
      · exact h₀.toIsComplex.zero i
    · 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_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝ : i + 2 ≤ n + 2
hi : i ≤ n
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0

Tactic:
obtain hi | rfl := hi.lt_or_eq

Goal state after:
case mpr.refine_1.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝¹ = 0

case mpr.refine_1.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.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0
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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝ : i + 2 ≤ n + 2
hi : i ≤ n
⊢ (S.sc ⋯ i hi✝).Exact

Tactic:
obtain hi | rfl := hi.lt_or_eq

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

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
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
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
dsimp +instances [CategoryTheory.categoryFree]
    rw [Finsupp.sum_add_index'] <;> · simp [add_mul]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ

Tactic:
· intro h A γ
    obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_up_to_refinements γ
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ hy₂
    refine ⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ, ?_⟩
    simp only [assoc, fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements]
    exact ⟨A₂, 𝟙 _, inferInstance, y₁, by simpa only [id_comp] using hy₁⟩

Goal state after:
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 : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁

Tactic:
rw [H, ← assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (_root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)) p

Tactic:
suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom (pullback.fst f g)) ((hom h.isoPullback.hom) p)
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:
by simpa using hi

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.snd a)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
dsimp
      rw [id_comp]

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
T : Monad C
x✝¹ x✝ : T.Algebra
f : (Monad.comparison T.adj).obj x✝¹ ⟶ (Monad.comparison T.adj).obj x✝
⊢ T.map f.f ≫ x✝.a = x✝¹.a ≫ f.f

Tactic:
simpa using! f.h

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X✝ Y✝ : G.Coalgebra
f : (Comonad.comparison G.adj).obj X✝ ⟶ (Comonad.comparison G.adj).obj Y✝
⊢ X✝.a ≫ G.map f.f = f.f ≫ Y✝.a

Tactic:
simpa using! f.h

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
inst✝ : Coreflective R
⊢ (Comonad.comparison (coreflectorAdjunction R)).EssSurj

Tactic:
by
  refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩
  refine Comonad.Coalgebra.isoMk ?_ ?_
  · exact (asIso ((coreflectorAdjunction R).counit.app X.A))
  rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]
  simp only [Functor.comp_obj, Functor.id_obj,
    assoc]
  simpa using (coreflectorAdjunction R).counit.app X.A ≫= X.counit.symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    (limit.isoLimitCone
          { cone := I.multiforkEquivPiFork.inverse.obj (limit.cone (parallelPair I.fstPiMap I.sndPiMap)),
            isLimit :=
              IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.inverse
                (limit.isLimit (parallelPair I.fstPiMap I.sndPiMap)) }).inv ≫
      ι I a

Tactic:
simp only [limit.isoLimitCone_inv_π,
    limit.cone_x, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    Fork.ι (limit.cone (parallelPair I.fstPiMap I.sndPiMap)) ≫ Fan.proj (limit.cone (Discrete.functor I.left)) a
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
⊢ FaithfulSMul (A ⧸ p) (B ⧸ P)

Tactic:
by
  rw [faithfulSMul_iff_algebraMap_injective]
  rintro ⟨a⟩ ⟨b⟩ hab
  apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _)
  rw [map_sub]
  exact Quotient.eq.mp hab

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f a).colon Set.univ).radical = ((f y).colon Set.univ).radical

Tactic:
hs' (mem_insert_self _ _),

Goal state after:
case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f i).colon Set.univ).radical = ((f y).colon Set.univ).radical
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ ⊤.annihilator ↔ r ∈ N.colon Set.univ

Tactic:
htop,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ (map N.mkQ ⊤).annihilator ↔ r ∈ N.colon Set.univ
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ restrictScalars R (localized' S p f (I • M')) =
    restrictScalars R (localized' S p (Algebra.linearMap R S) I • localized' S p f M')

Tactic:
simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x₁✝ x₂✝ : ↥M'
e : (toLocalized₀ p f M') x₁✝ = (toLocalized₀ p f M') x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
by simpa [Subtype.ext_iff] using
      IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)

Goal state after: