mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha :
  (Localization.localRingHom (Ideal.comap f P) P f ⋯)
      (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) =
    IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
rw [Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq,
      Submonoid.coe_one, one_mul, IsLocalization.eq_iff_exists P.primeCompl] at ha

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : ∃ c, ↑c * f a = ↑c * (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False

Tactic:
rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g ((algebraMap R T) r) * g t ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
Ring.KrullDimLE,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ Order.KrullDimLE 0 (PrimeSpectrum R) ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Tactic:
Ring.KrullDimLE,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ Order.KrullDimLE 1 (PrimeSpectrum R) ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
Ring.KrullDimLE,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ Order.KrullDimLE 1 (PrimeSpectrum R) ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ x ∈ Ideal.comap f q

Tactic:
hq

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ x ∈ p
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ (Ideal.map (algebraMap R A) I).radical = Ideal.map (algebraMap R A) q

Tactic:
rw [← Ideal.sInf_minimalPrimes, IsLocalization.minimalPrimes_map q.primeCompl A I]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ sInf (Ideal.under R ⁻¹' I.minimalPrimes) = Ideal.map (algebraMap R A) q
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
obtain ⟨Y, f, e, hf⟩ := hb.open_eq_iUnion hUo

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ i, f i
hf : ∀ (i : Y), f i ∈ range b
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
⊢ s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

Tactic:
hs

Goal state after:
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
⊢ ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ i, f i)

Tactic:
noetherianSpace_set_iff

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
⊢ ∀ t ⊆ ⋃ i, f i, IsCompact t
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ ⋃ i ∈ t, f '' ↑↑i = U

Tactic:
refine subset_antisymm (fun x ↦ ?_) ht
      simp_rw [Set.mem_iUnion]
      rintro ⟨i, hi, x, hx, rfl⟩
      have := heq ▸ mem_sSup.mpr ⟨i.1, i.2, hx⟩
      exact this

Goal state after:
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:
rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S

Tactic:
simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and, closure, subset_sInter_iff,
    mem_ofPred_eq, and_imp, singleton_subset_iff]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

Tactic:
rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) ↔ IsField R

Tactic:
refine ⟨?_, fun h => ?_⟩
  · intro h
    exact
      Classical.not_not.1
        (mt
          (Ring.ne_bot_of_isMaximal_of_not_isField <|
            (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, inferInstance⟩))
          (by simp))
  · refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
    by_cases hx : x.asIdeal = ⊥
    · let := h.toSemifield
      exact hx.symm ▸ Ideal.bot_isMaximal
    · exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
· simp_rw [← zeroLocus_inf, subset_zeroLocus_iff_le_vanishingIdeal,
        vanishingIdeal_zeroLocus_eq_radical, hI.radical]
      constructor
      · simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
          Ideal.span_singleton_mul_span_singleton]
        refine fun h x y h' => h _ _ ?_
        rw [← hI.radical_le_iff] at h' ⊢
        simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'
      · simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
        rintro h s t h' ⟨x, hx, hx'⟩ y hy
        exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u

Tactic:
rintro p U hp ⟨s, hs⟩

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ ∀ (x : α), x ∈ zpowers g

Tactic:
exact fun x ↦ Submonoid.powers_le_zpowers _ (hx _)

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
h : k.natAbs = 0
⊢ x = 1

Tactic:
by
          rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬orderOf g = 1
⊢ orderOf g = p

Tactic:
exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ ExponentExists G

Tactic:
by
  let _inst := Fintype.ofFinite G
  simp only [Monoid.ExponentExists]
  refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
  · simpa [pos_iff_ne_zero, Finset.lcm_eq_zero_iff] using fun x => (_root_.orderOf_pos x).ne'
  · rw [← orderOf_dvd_iff_pow_eq_one, lcm_orderOf_eq_exponent]
    exact order_dvd_exponent g

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ I ^ n ⊔ J ^ n = ⊤

Tactic:
rw [eq_top_iff, ← Ideal.span_pow_eq_top (I ∪ J : Set R) _ n, Ideal.span_le, Set.image_union,
      Set.union_subset_iff]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x ↦ x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n) ∧ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤
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
ϕ : G →* K
⊢ IsPGroup p ↥(ϕ.comp H.subtype).range

Tactic:
exact hH.of_surjective (ϕ.domRestrict H).rangeRestrict (ϕ.domRestrict H).rangeRestrict_surjective

Goal state after:
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
⊢ IsPGroup p ↥(Subgroup.comap ϕ H)

Tactic:
intro g
  obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
  rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj
  obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
  rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
  exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a, (∃ y, orderOf y = a) ∧ x < a

Tactic:
exists_exists_eq_and

Goal state after:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a, x < orderOf a
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 : ¬0 < #{a | orderOf a = d}
⊢ False

Tactic:
simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0

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} = ∅
⊢ False
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
⊢ rank ↥(closure ↑s) ≤ s.card

Tactic:
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s ∈ irreducibleComponents (PrimeSpectrum R) → ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s

Tactic:
hs

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu' : ∀ a ∈ u, IsAtom a
hu : f i = ↑(sSup u)
⊢ f i = sSup (Subtype.val '' u)

Tactic:
hu,

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu' : ∀ a ∈ u, IsAtom a
hu : f i = ↑(sSup u)
⊢ ↑(sSup u) = sSup (Subtype.val '' u)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1)

Tactic:
convert! hi

Goal state after:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
⊢ (Set.range fun i_1 ↦ v ↑i_1) = v '' (Set.univ \ {i})
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • span R s)

Tactic:
hs

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • N)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ span R s ≤ N

Tactic:
hs

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ N
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
⊢ s ∈ I ^ n → (monomial (n + 1)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
hs

Goal state after:
case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (n + 1)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial 1) r * (monomial n) s ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ a • (mk (R ∙ a * b)) x = 0

Tactic:
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]

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

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span ↥(reesAlgebra I) ↑(Submodule.map (lsingle R i) (Submodule.span R ↑s)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

Tactic:
hs

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span ↥(reesAlgebra I) ↑(Submodule.map (lsingle R i) (F.N i)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

Tactic:
← (Submodule.restrictScalars_injective R ..).eq_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.restrictScalars R (Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s)) =
      Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C f).obj X b = (comap C g).obj X b

Tactic:
by dsimp; simp only [h]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C g).obj X b = (comap C f).obj X b

Tactic:
by dsimp; simp only [h]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ : S
⊢ ∀ (y_1 : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] y_1)

Tactic:
x₂

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
      (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)