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

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

Tactic:
by
        have := discreteTopology_bot α
        fun_prop

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ sSup (range fun a ↦ f (g a)) = sSup (range fun b ↦ f b)

Tactic:
csSup_of_not_bddAbove,

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ sSup ∅ = sSup (range fun b ↦ f b)

α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun a ↦ f (g a))
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p ↦ Ixx p.1 p.2) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (l₂ ⊓ l₂').smallSets

Tactic:
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1

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

Goal state before:
pp: case h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ m / a < b
⊢ a ^ m < b * a ∧ b < a ^ m

Tactic:
exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩

Goal state after:
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 : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
have := hf.atTop_mul_pos (neg_pos.2 hC) hg.neg

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x ↦ f x * -g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x : α
hx : x > 1
y : α
hy : y > 1
⊢ ∃ k > 1, {b | |b / a|ₘ < k} ⊆ {b | |b / a|ₘ < x} ∧ {b | |b / a|ₘ < k} ⊆ {b | |b / a|ₘ < y}

Tactic:
exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ Ioo (a / ε) (a * ε)

Tactic:
convert! nhds_basis_mabs_div_lt a
  simp only [Ioo, mabs_lt, ← div_lt_iff_lt_mul, inv_lt_div_iff_lt_mul, div_lt_comm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderTopology αᵒᵈ

Tactic:
constructor
  rcases t.topology_eq_generate_intervals with rfl
  simp_rw [Preorder.topology, or_comm]
  rfl

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

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]

Goal state after:
case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
this : Ico a b = Icc a a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
have ⟨m', hm⟩ := hx

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
hm : (fun x ↦ x • p) m' = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x ↦ Ioc (z x) x) x
ux' : u ∈ (fun x ↦ Ioc (z x) x) x'
H : x < y x'
⊢ False

Tactic:
exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ ∀ (x_1 : α), z x < x_1 ∧ x_1 < y x → z x < x_1 ∧ x_1 ≤ x

Tactic:
exact fun u hu ↦ ⟨hu.1, Hy _ _ hx.1 hu.2⟩

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f ↑↑((equivIco p a) x) = f ↑((equivIco p a) x)

Tactic:
exact liftIoc_coe_apply (by grind)

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

Goal state before:
pp: A : Type u
inst✝ : MonObj A
x y z : A
⊢ x * y * z = x * (y * z)

Tactic:
by convert! congr_hom (CC := fun X ↦ X) (mul_assoc A) ((x, y), z)

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

Goal state before:
pp: case a
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ sSup (f ⁻¹' Iic z) ≠ a

Tactic:
have : sSup (f '' f ⁻¹' Iic z) ≤ z := csSup_le (.image _ ne) fun _ ⟨b, hb, heq⟩ ↦ heq ▸ hb

Goal state after:
case a
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
this : sSup (f '' f ⁻¹' Iic z) ≤ z
⊢ sSup (f ⁻¹' Iic z) ≠ a
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
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ π ≫ a = x₁ ≫ S.toCycles

Tactic:
by simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]

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
inst✝ : Mono S.L₁.f
this : Mono (S.L₀.f ≫ S.v₀₁.τ₂)
⊢ Mono S.L₀.f

Tactic:
exact mono_of_mono _ S.v₀₁.τ₂

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₃ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
hx₃

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₂
hx₃ : x₃ ≫ S.L₁'.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ x = y

Tactic:
by
  apply Concrete.limit_ext
  rintro (_ | j)
  · exact h₀
  · apply h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
⊢ Function.LeftInverse
    (fun x ↦
      ⟨fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
        ⋯⟩)
    fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩

Tactic:
intro x; ext (a | b)
    · rfl
    · rw [← x.2 (WalkingMulticospan.Hom.fst b)]
      rfl

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

Goal state before:
pp: J : MultispanShape
a : WalkingMultispan J
⊢ ∀ (a_1 : a ⟶ a), a_1 = 𝟙 a

Tactic:
by rintro ⟨⟩; rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom S.g).ker = (ConcreteCategory.hom S.f).range
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(↑eN.symm ∘ₗ f) ⇑(↑eL.symm ∘ₗ g ∘ₗ ↑eN)

Tactic:
LinearEquiv.postcomp_exact_iff_exact,

Goal state after:
R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(↑eN.symm ∘ₗ f) ⇑(g ∘ₗ ↑eN)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero

Tactic:
apply Cofan.IsColimit.hom_ext hc
        simp

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ colimit.ι I.multispan (WalkingMultispan.left a) ≫ i = colimit.ι I.multispan (WalkingMultispan.left a) ≫ j

Tactic:
simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
N : Type u_4
inst✝¹ : Group N
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
m : ↥(MulAction.stabilizer M I)
x : R
⊢ (I.stabilizerEquiv e he) m • x = m • x

Tactic:
by
  simp [stabilizerEquiv, MulAction.subgroup_smul_def, ← he m x]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤

Tactic:
rw [P.over_def p]
  exact comap_eq_top_iff.symm

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Submodule R M
hI : S.IsPrimary
⊢ (S.colon Set.univ).radical.IsPrime

Tactic:
refine isPrime_iff.mpr <| hI.imp (by simp) fun h x y ⟨n, hn⟩ ↦ ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Submodule R M
hI : S.IsPrimary
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
x y : R
x✝ : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∈ S
⊢ (S.colon {m}).radical = ⊤

Tactic:
radical_eq_top,

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∈ S
⊢ S.colon {m} = ⊤
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ (f.restrict hf ^ n) m = 0 m

Tactic:
simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]; rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z) →
    ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

Tactic:
rintro ⟨x, hx, s, rfl⟩

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
hx : x ∈ I
s : ↥M
⊢ ∃ x_1, IsLocalizedModule.mk' (Algebra.linearMap R S) x s * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = 0
P : Ideal R
x✝ : P.IsMaximal
⊢ (f P) m = (f P) 0

Tactic:
rw [h, map_zero]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ (a * (algebraMap R A) a_1) ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p

Tactic:
← Algebra.commutes,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ ((algebraMap R A) a_1 * a) ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
⊢ ∀ (a b : S), a ∈ nonunits S → b ∈ nonunits S → a + b ∈ nonunits S

Tactic:
by
      intro x y hx hy hu
      obtain ⟨z, hxyz⟩ := isUnit_iff_exists_inv.1 hu
      have : ∀ {r : R} {s : P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P := fun {r s} =>
        not_imp_comm.1 fun nr => isUnit_iff_exists_inv.2 ⟨mk' S ↑s (⟨r, nr⟩ : P.primeCompl),
          mk'_mul_mk'_eq_one' _ _ <| show r ∈ P.primeCompl from nr⟩
      rcases exists_mk'_eq P.primeCompl x with ⟨rx, sx, hrx⟩
      rcases exists_mk'_eq P.primeCompl y with ⟨ry, sy, hry⟩
      rcases exists_mk'_eq P.primeCompl z with ⟨rz, sz, hrz⟩
      rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz
      rw [← hrx] at hx
      rw [← hry] at hy
      obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz
      simp only [mul_one, one_mul, Submonoid.coe_mul] at ht
      suffices (t : R) * (sx * sy * sz) ∈ P from
        not_or_intro (mt hp.mem_or_mem <| not_or_intro sx.2 sy.2) sz.2
          (hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)
      rw [← ht]
      exact
        P.mul_mem_left _ <| P.mul_mem_right _ <|
            P.add_mem (P.mul_mem_right _ <| this hx) <| P.mul_mem_right _ <| this hy

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x} ⊆ ↑(mapOfCompatibleSMul A R A M N).ker

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Tactic:
· rintro - ⟨a, m, n, rfl⟩
    simp [smul_tmul]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := e.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
convert! hP f 1 R T hf

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := e.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = IsLocalization.Away.map R T f 1
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝¹ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
convert! hP f 1 R T hf

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝¹ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P (algebraMap R S)

Tactic:
have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (algebraMap R S)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsSymm ↔ Aᵀ = A.map fun x ↦ xᵀ

Tactic:
rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i

Tactic:
rw [updateRow_self, updateRow_ne (Ne.symm h)]

Goal state after: