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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

Tactic:
← notMem_mulSupport,

Goal state after:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map (fun p ↦ m p.1 p.2) ((f₁ ⊔ f₂) ×ˢ g) = map (fun p ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun p ↦ m p.1 p.2) (f₂ ×ˢ g)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ (g₁ ⊔ g₂)) = map (fun p ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun p ↦ m p.1 p.2) (f ×ˢ g₂)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map₂ m (pure a) g = map (m a) g

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map (fun p ↦ m p.1 p.2) (pure a ×ˢ g) = map (m a) g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map₂ m f (pure b) = map (fun x ↦ m x b) f

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ pure b) = map (fun x ↦ m x b) f
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = map₂ (fun a b ↦ m b a) g f

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ g) = map₂ (fun a b ↦ m b a) g f
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map ((fun p ↦ m p.1 p.2) ∘ Prod.swap) (g ×ˢ f) = map₂ (fun a b ↦ m b a) g f

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map ((fun p ↦ m p.1 p.2) ∘ Prod.swap) (g ×ˢ f) = map (fun p ↦ m p.2 p.1) (g ×ˢ f)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map₂ (fun x x_1 ↦ x) f g = f

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map (fun p ↦ p.1) (f ×ˢ g) = f
Module: Mathlib.Order.Filter.NAry

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

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map (fun p ↦ m p.1 p.2) (f ×ˢ g)) = map₂ (fun a b ↦ n (m a b)) f g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map (fun p ↦ m p.1 p.2) (f ×ˢ g)) = map₂ (fun a b ↦ n (m a b)) f g

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map (fun p ↦ m p.1 p.2) (f ×ˢ g)) = map (fun p ↦ n (m p.1 p.2)) (f ×ˢ g)
Module: Mathlib.Order.Filter.NAry

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

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map (fun p ↦ m p.1 p.2) (map n f ×ˢ g) = map₂ (fun a b ↦ m (n a) b) f g
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map (fun p ↦ m p.1 p.2) (map n f ×ˢ g) = map₂ (fun a b ↦ m (n a) b) f g

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map (fun p ↦ m p.1 p.2) (map n f ×ˢ g) = map (fun p ↦ m (n p.1) p.2) (f ×ˢ g)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ (fun a b ↦ m (n a.1 a.2) b) (f ×ˢ g) h = map₂ (fun a b ↦ m' a (n' b.1 b.2)) f (g ×ˢ h)

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) = map₂ (fun a b ↦ m' a (n' b.1 b.2)) f (g ×ˢ h)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) = map₂ (fun a b ↦ m' a (n' b.1 b.2)) f (g ×ˢ h)

Tactic:
← map_prod_eq_map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) = map (fun p ↦ m' p.1 (n' p.2.1 p.2.2)) (f ×ˢ g ×ˢ h)
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_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)

Tactic:
by
  simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]

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
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)

Tactic:
exact (UniformOnFun.mono (uniformContinuous_iff_le_comap.mp hf)
    subset_rfl).trans_eq UniformOnFun.comap_eq

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

Goal state before:
pp: case h
α : 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
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ F ≤
    ⨅ s ∈ 𝔖,
      ⨅ i,
        ⨅ (_ : i ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i),
          𝓟 {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i}

Tactic:
le_iInf₂_iff,

Goal state after:
case h
α : 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
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ ∀ i ∈ 𝔖,
    ∀ (i_1 : SetRel β β),
      i_1 ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i_1 →
        F ≤ 𝓟 {g_1 | ∀ x ∈ i, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i_1}
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a * x) '' Iic b = Iic (a * b)

Tactic:
simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a * x) '' Iio b = Iio (a * b)

Tactic:
simp [mul_comm]

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

Goal state before:
pp: G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
s : Set X
hs : s ∈ 𝓝 0
x : X
this : Tendsto (fun x_1 ↦ x_1 • x) (𝓝 0) (𝓝 0)
⊢ x ∈ univ • s

Tactic:
rcases Filter.nonempty_of_mem (inter_mem_nhdsWithin {0}ᶜ <| mem_map.1 <| this hs)
    with ⟨c, hc₀, hc⟩

Goal state after:
G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
s : Set X
hs : s ∈ 𝓝 0
x : X
this : Tendsto (fun x_1 ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc₀ : c ∈ {0}ᶜ
hc : c ∈ (fun x_1 ↦ x_1 • x) ⁻¹' s
⊢ x ∈ univ • s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Goal state after:
case inl.inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure[inst✝²] (0 • ∅) = 0 • closure[inst✝²] ∅

case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun x ↦ f (x.1 / x.2)

Tactic:
map_div

Goal state after:
G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun x ↦ f x.1 / f x.2
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Ioi (c * a) = ⇑(Homeomorph.mulLeft c) '' Ioi a

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Iio (c * a) = ⇑(Homeomorph.mulLeft c) '' Iio a

Tactic:
simp [mul_comm]

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

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

Tactic:
by
  rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def]
  simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
hfg : Tendsto (fun x ↦ f x * g x) l atTop
⊢ Tendsto g l atTop

Tactic:
by
  obtain ⟨C, hC⟩ := hf
  refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg
  exact (eventually_map.mp hC).mono fun _ _ ↦ by dsimp; gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
a : α
b : β
a' : α
ha' : a' ∈ {a}
⊢ const β a (const α b a') = a'

Tactic:
by rw [eq_of_mem_singleton ha', const_apply]

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

Goal state before:
pp: n : ℕ
⊢ (int.divByNat n) ↑n = 0

Tactic:
by
  obtain rfl | h0 := eq_or_ne n 0
  · apply map_zero
  exact (AddCircle.coe_eq_zero_iff _).mpr
    ⟨1, by simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]⟩

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 : ℕ
h : 0 < n
⊢ addOrderOf ↑(p / ↑n) = n

Tactic:
rw [addOrderOf_eq_iff h]
  replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
  refine ⟨?_, fun m hn h0 => ?_⟩ <;> simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
  · rw [mul_div_cancel₀ _ h.ne', coe_period]
  rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]
  rintro ⟨k, hk⟩
  rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul,
    (mul_left_injective₀ hp.out.ne').eq_iff, Nat.cast_inj, mul_comm] at hk
  exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ (x₂ - x₂') ≫ S.g = 0

Tactic:
simp [hx₂, hx₂']

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: case e_a
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.φ₁ = x₁

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, lift_φ₂, h₁]

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
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

Tactic:
apply Fan.IsLimit.hom_ext hd

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
⊢ ∀ (i : J.R),
    (Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd) ≫ d.proj i =
      (Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd) ≫ d.proj i
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one

Tactic:
apply Fan.IsLimit.hom_ext hd

Goal state after:
case one
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (i : J.R),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one) ≫ d.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one ≫ d.proj i
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
      R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    X.a ≫ (reflectorAdjunction R).unit.app X.A

Tactic:
← cancel_epi ((reflectorAdjunction R).unit.app X.A)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : I.fst (y, x) ≫ c.π y = I.snd (y, x) ≫ c.π x
⊢ I.fst (x, y) ≫ c.π x = I.snd (x, y) ≫ c.π y

Tactic:
rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)

Tactic:
← t.fac,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (t.lift c ≫ c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (t.lift c ≫ c.π.app j)
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I.IsPrimary

Tactic:
isPrimary_iff

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
hI : I.IsPrimary
φ : R →+* S
⊢ (Ideal.comap φ I).IsPrimary

Tactic:
isPrimary_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
⊢ Ideal.comap φ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ Ideal.comap φ I → x ∈ Ideal.comap φ I ∨ y ∈ (Ideal.comap φ I).radical
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M), S.mkQ x ≠ 0 → r • S.mkQ x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
← map_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M), S.mkQ x ≠ 0 → S.mkQ (r • x) = 0 → ∃ n, r ^ n • ⊤ = ⊥
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A))

Tactic:
LinearMap.isNilpotent_toMatrix_iff

Goal state after:
R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent (toLin' A)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ I ⊔ J ≤ p

pp: case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q

Tactic:
· rw [sup_le_iff]
    refine ⟨hle, by simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) h.le⟩

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q