mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∈ liftsRing i

Tactic:
refine Subring.multiset_prod_mem _ _ fun g hg => ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
g : R[X]
hg : g ∈ Multiset.map (fun x ↦ X - C x) f.roots
⊢ g ∈ liftsRing i
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∉ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
Polynomial.notMem_support_iff

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
⊢ IsAlgebraic R z

Tactic:
have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
  have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
  rw [mul_right_comm, eq, ← Algebra.smul_def] at this
  exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ((Ideal.Quotient.mk (maximalIdeal S)).comp f) a = 0

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ (Ideal.Quotient.mk (maximalIdeal S)) (f a) = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
⊢ LinearMap.lTensor M LinearMap.id = 0

Tactic:
by ext; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
⊢ LinearMap.rTensor M LinearMap.id = 0

Tactic:
by ext; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
N : Type (max u_1 v)
x✝² : AddCommGroup N
x✝¹ : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x✝ : Module R N := compHom N (algebraMap R S)
this : IsScalarTower R S N
⊢ Subsingleton N

Tactic:
have := (AlgebraTensorModule.cancelBaseChange R S S N M).symm.subsingleton

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
N : Type (max u_1 v)
x✝² : AddCommGroup N
x✝¹ : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x✝ : Module R N := compHom N (algebraMap R S)
this✝ : IsScalarTower R S N
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).SurjectiveOnStalks

Tactic:
change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).SurjectiveOnStalks

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).SurjectiveOnStalks
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ { toFun := fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }
        a ≤
      { toFun := fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }
        b ↔
    a ≤ b

Tactic:
by
    change a.asIdeal.comap _ ≤ b.asIdeal.comap _ ↔ a ≤ b
    rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]

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

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ p.IsPrime

Tactic:
rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]

Goal state after:
case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ (Ideal.under R p).IsPrime ∧ p ≠ ⊤
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : OrderTop α
top : α
eq_top : top = ⊤
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ x✝ ≤ ⊤

Tactic:
by simp [eq_top, le_eq]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ x✝ ≤ ⊤

Tactic:
by simp [eq_top, le_eq]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)

Tactic:
RingEquiv.comp_symm,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization (RingHom.id S) ⋯ = RingHom.id (PiLocalization S)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a : α), bot ≤ a

Tactic:
by intros; simp +instances [eq_le, eq_bot]

Goal state after:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(U i)
⊢ x ∈ ⨆ V, (↑V).1

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]

Goal state after:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(U i)
⊢ ∃ i, x ∈ (↑i).1
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) = RingHom.id (PiLocalization S)

Tactic:
RingEquiv.comp_symm,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization (RingHom.id S) = RingHom.id (PiLocalization S)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst✝] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst✝] s ⊆ s
x : { x // x ∈ closure[inst✝] s }
⊢ x ∈ closure[inst✝] s ↓∩ s → x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h

Tactic:
exact (subset_iUnion₂ _ _ <| hxU x ·)

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
⊢ (irreducibleComponents α).Finite

Tactic:
obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
    NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)
  refine hSf.subset fun s hs => ?_
  lift S to Finset (Set α) using hSf
  rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩
  rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
s : Set X
⊢ s ∈ SetLike.coe '' {U | IsCompact ↑U} ↔ s ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}

Tactic:
exact ⟨fun ⟨V, hV, heq⟩ ↦ heq ▸ ⟨V.2, hV⟩, fun h ↦ ⟨⟨s, h.1⟩, h.2, rfl⟩⟩

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst✝²] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ ↑U
⊢ ∃ i, ∃ (_ : i ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }), x ∈ i.toOpens

Tactic:
exact ⟨⟨⟨_, h₂⟩, h₁⟩, hVU, hxV⟩

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ x ∈ ↑(sInf S) ↔ ∀ s ∈ S, x ∈ ↑s

Tactic:
coe_sInf,

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ x ∈ ⋂ s ∈ S, ↑s ↔ ∀ s ∈ S, x ∈ ↑s
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ ↑s ⊆ ↑(sInf S)

Tactic:
coe_sInf,

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ ↑s ⊆ ⋂ s ∈ S, ↑s
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) univ

Tactic:
simpa using! (IrreducibleSpace.isIrreducible_univ α).isGenericPoint_genericPoint_closure

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

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))

Tactic:
algebraize [f]
  change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B)
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
h : (fun D ↦ D.toFun) D1 = (fun D ↦ D.toFun) D2
⊢ D1 = D2

Tactic:
cases D1

Goal state after:
case mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2✝ : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } =
    (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } = D2
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosed (Set.range (comap (RingHom.fst R S)))

Tactic:
range_comap_fst,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosed (zeroLocus ↑(RingHom.ker (RingHom.fst R S)))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsInducing ⇑(primeSpectrumProd R S).symm

Tactic:
refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous ⇑(primeSpectrumProd R S).symm

case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case ge
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 1 ≤ exponent G

Tactic:
apply Nat.succ_le_of_lt

Goal state after:
case ge
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 0 < exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)

Goal state after:
case inl
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ ↑(basicOpen ↑a ⊓ basicOpen ↑b) = ↑⊥

Tactic:
TopologicalSpace.Opens.coe_inf,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ ↑(basicOpen ↑a) ∩ ↑(basicOpen ↑b) = ↑⊥
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ (p ^ j * p ^ k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
← pow_add

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
H : AddSubgroup G
hH : ∀ (x : G), n • x ∈ H
⊢ ∀ (x : G ⧸ H), n • x = 0

Tactic:
by simpa [QuotientAddGroup.forall_mk, ← QuotientAddGroup.mk_nsmul]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors, #{a | orderOf a = m} = ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m}

Tactic:
rw [eq_comm]

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m} = ∑ m ∈ c.divisors, #{a | orderOf a = m}
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)

Tactic:
mem_center_iff.1 hb

Goal state after:
G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx : sSup s ≤ a
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx⟩

Tactic:
sSup_le_iff

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx✝⟩
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
⊢ (↑P).Characteristic

Tactic:
by
  refine Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_
  have h := Subgroup.pointwise_smul_def (a := ϕ) (P : Subgroup G)
  rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ (eraseLast s).snoc (last s) ⋯

Tactic:
simp only [mem_snoc, mem_eraseLast h, ne_eq]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s