mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx : DFinsupp.coeFnAddMonoidHom x = 1
i : ι
hi : i ∉ x.support
⊢ False

Tactic:
simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x ∈ p.asIdeal

Tactic:
convert! p.asIdeal.mul_mem_left x hi

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x = x * e i
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J

Tactic:
· exact Ideal.map_le_of_le_comap e₂

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_2
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 → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : ι
hi : i ∈ ↑(Finset.image f' t)
⊢ b i ⊆ U

Tactic:
obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi

Goal state after:
case refine_2
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 → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ ↑(Finset.image f' t)
⊢ b (f' j) ⊆ U
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ I ≠ { asIdeal := J, isPrime := ⋯ }

Tactic:
intro eq; have : I.1 = J := congr_arg (·.1) eq; exact h (this ▸ max)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝² x✝¹ : Opens α
carrier✝¹ : Set α
is_open'✝¹ : IsOpen[inst✝²] carrier✝¹
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝²] carrier✝
x✝ : { carrier := carrier✝¹, is_open' := is_open'✝¹ }.carrier = { carrier := carrier✝, is_open' := is_open'✝ }.carrier
⊢ { carrier := carrier✝¹, is_open' := is_open'✝¹ } = { carrier := carrier✝, is_open' := is_open'✝ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ coborder s

Tactic:
rw [coborder, subset_compl_iff_disjoint_right]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint s (closure[inst✝] s \ s)
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
⊢ NoetherianSpace (CofiniteTopology α)

Tactic:
simp only [noetherianSpace_iff_isCompact, isCompact_iff_ultrafilter_le_nhds,
    CofiniteTopology.nhds_eq, Ultrafilter.le_sup_iff, Filter.le_principal_iff]

Goal state after:
α✝ : 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
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
⊢ x ∈ U →
    x ∈
      (fun I ↦ ⨆ U ∈ I, U.toOpens)
        ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)

Tactic:
hxU

Goal state after:
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
⊢ x ∈
    (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
x : X
⊢ x ∈ U → x ∈ V

Tactic:
hxU

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
x : X
hxU : x ∈ U
⊢ x ∈ V
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ ↑((fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun s ↦ ⋯.genericPoint) s)) = ↑s

Tactic:
simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
      closure_eq_iff_isClosed.mpr s.3]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ s.carrier = ↑s
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
⊢ IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)

Tactic:
simpa [← range_sdiff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Tactic:
rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff,
    (equivSubtype R).finite_iff, ← Set.coe_ofPred, Set.finite_coe_iff, Set.finite_coe_iff]
  refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
    fun ⟨fin, le⟩ ↦ ?_⟩
  have hpm (I : Ideal R) (hI : I.IsPrime) : I.IsMaximal := by
    replace le := le.trans (nilradical_le_prime I)
    rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
    have ⟨M, hM, hMI⟩ := le
    rw [fin.mem_toFinset] at hM
    rwa [← hM.eq_of_le hI.1 hMI]
  exact ⟨fin.subset hpm, hpm⟩

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
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
a b : A
⊢ (r • ↑D) (a * b) = a • (r • ↑D) b + b • (r • ↑D) a

Tactic:
simp only [LinearMap.smul_apply, coeFn_coe, leibniz, smul_add,
        smul_comm r (_ : A) (_ : M)]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
hI' : (zeroLocus ↑I)ᶜ = s
J : Ideal R
hJ : J.FG
hJ' : (zeroLocus ↑J)ᶜ = sᶜ
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
simp only [compl_eq_iff_isCompl, ← eq_compl_iff_isCompl, compl_compl] at hI' hJ'

Goal state after:
case inr
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
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
← QuotientGroup.ker_mk' K,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ (QuotientGroup.mk' K).ker)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
cases subsingleton_or_nontrivial R
  · refine ⟨0, 0, ?_, ?_, ?_, ?_⟩ <;> apply Subsingleton.elim
  obtain ⟨I, hI, hI'⟩ := isCompact_isOpen_iff_ideal.mp ⟨hs.1.isCompact, hs.2⟩
  obtain ⟨J, hJ, hJ'⟩ := isCompact_isOpen_iff_ideal.mp
    ⟨hs.2.isClosed_compl.isCompact, hs.1.isOpen_compl⟩
  simp only [compl_eq_iff_isCompl, ← eq_compl_iff_isCompl, compl_compl] at hI' hJ'
  have : I * J ≤ nilradical R := by
    refine Ideal.radical_le_radical_iff.mp (le_of_eq ?_)
    rw [← zeroLocus_eq_iff, Ideal.zero_eq_bot, zeroLocus_bot,
      zeroLocus_mul, hI', hJ', Set.compl_union_self]
  obtain ⟨n, hn⟩ := Ideal.exists_pow_le_of_le_radical_of_fg this (Submodule.FG.mul hI hJ)
  have hnz : n ≠ 0 := by rintro rfl; simp at hn
  rw [mul_pow, Ideal.zero_eq_bot] at hn
  have : I ^ n ⊔ J ^ n = ⊤ := by
    rw [eq_top_iff, ← Ideal.span_pow_eq_top (I ∪ J : Set R) _ n, Ideal.span_le, Set.image_union,
      Set.union_subset_iff]
    constructor
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)
    · rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_self]
  rw [Ideal.eq_top_iff_one, Submodule.mem_sup] at this
  obtain ⟨x, hx, y, hy, add⟩ := this
  have mul : x * y = 0 := hn (Ideal.mul_mem_mul hx hy)
  have : s = basicOpen x := by
    refine subset_antisymm ?_ ?_
    · rw [← hJ', basicOpen_eq_zeroLocus_of_mul_add _ _ mul add]
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)
    · rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)
  refine ⟨x, y, mul, add, this, ?_⟩
  rw [this, basicOpen_eq_zeroLocus_of_mul_add _ _ mul add, basicOpen_eq_zeroLocus_compl]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
this : ∃ g, g ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1

Tactic:
obtain ⟨m, hm⟩ := this

Goal state after:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime 0
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
Nat.coprime_zero_right,

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : Nat.card ↥H = 1
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p ↥ϕ.ker
h : ↑P ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup p ↥Q
hle : comap ϕ ↑P ≤ Q
⊢ Q = comap ϕ (map ϕ Q)

Tactic:
exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
⊢ rank G = 0 ↔ Subsingleton G

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rank_eq_zero G⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
h : rank G = 0
⊢ Subsingleton G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
refine Sylow.nonempty.elim fun P : Sylow p G => ?_

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ Nat.card ↥(Subgroup.zpowers ((powMonoidHom d) g)) = Nat.card G / (Nat.card G).gcd d

Tactic:
Nat.card_zpowers,

Goal state after:
G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ orderOf ((powMonoidHom d) g) = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
⊢ ∀ (x y : ↥(normalizer ↑H)), (leftRel (comap (normalizer ↑H).subtype H)) x y ↔ (leftRel H) ↑x ↑y

Tactic:
intros
      unfold_projs
      rw [leftRel_apply (α := normalizer (H : Set G)), leftRel_apply]
      rfl

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

Goal state before:
pp: α : Type u_1
G✝ : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst✝¹ : Group G
inst✝ : IsCyclic G
⊢ IsCyclic (WithZero G)ˣ

Tactic:
by
  apply isCyclic_of_injective (G := (WithZero G)ˣ) (WithZero.unitsWithZeroEquiv).toMonoidHom
  apply Equiv.injective

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j

Tactic:
have := Submodule.coe_mem (μ a)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
this : ↑(μ a) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b

Tactic:
have := Submodule.coe_mem (μ a)

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
this : ↑(μ a) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ I b
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ (a✝ * b✝).coeff i ∈ I ^ i

Tactic:
rw [coeff_mul]
    apply Ideal.sum_mem
    rintro ⟨j, k⟩ e
    rw [← Finset.mem_antidiagonal.mp e, pow_add]
    exact Ideal.mul_mem_mul (hf j) (hg k)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hM : IsTorsionBySet R M ↑I
b : R ⧸ I
⊢ Submodule.toAddSubgroup I ≤ (smulAddHom R M).ker

Tactic:
by rwa [isTorsionBySet_iff_subset_annihilator] at hM

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ ↑(torsion R M) = {x | (R ∙ x).annihilator ≠ ⊥}

Tactic:
by
  ext x; simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]
  exact
    ⟨fun ⟨a, hax⟩ =>
      ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero],
        nonZeroDivisors.coe_ne_zero _⟩,
      fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case succ
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
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I ^ (n✝ + 1) • F.N j ≤ F.N (n✝ + 1 + j)

Tactic:
rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]

Goal state after:
case succ
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
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I • I ^ n✝ • F.N j ≤ F.N (n✝ + j + 1)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ Submodule.restrictScalars R (I₁ • ⊤)
⊢ x ∈ Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))

Tactic:
rw [Submodule.restrictScalars_mem] at hx

Goal state after:
case refine_2
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
⊢ x ∈ Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))
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
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
x : ↥I
hx : x ∈ (I • ⊤).toAddSubgroup
⊢ x ∈ f.toAddMonoidHom.ker

Tactic:
simp only [Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker] at hx ⊢
    refine Submodule.smul_induction_on hx (fun r hr y _ ↦ hf ⟨r, hr⟩ y) fun x y hx hy ↦ ?_
    simp only [map_add, hx, hy, add_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = ResidueField R ∙ (maximalIdeal R).toCotangent x) ↔ ∃ a, maximalIdeal R = R ∙ a

Tactic:
← Set.image_singleton,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' {x})) ↔ ∃ a, maximalIdeal R = R ∙ a
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
this : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'
⊢ h₁ = h₂

Tactic:
by
        cases h₁
        cases h₂
        simp only [Universal.mk.injEq]
        ext : 2
        apply this

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

Goal state before:
pp: case refine_2.refine_1
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₂ * 0) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 +
      (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
· rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
⊢ g = h

Tactic:
ext i
    rw [← cancel_epi (φ.f i)]
    exact congr_hom eq i

Goal state after: