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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S✝ : Submonoid A
hS : S✝ ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
S : Subalgebra A K
⊢ IsFractionRing (↥S) K

Tactic:
refine IsFractionRing.of_field S K fun z ↦ ?_

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S✝ : Submonoid A
hS : S✝ ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
S : Subalgebra A K
z : K
⊢ ∃ x y, z = (algebraMap (↥S) K) x / (algebraMap (↥S) K) y
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : PrimeSpectrum R
⊢ {comap (algebraMap R I.asIdeal.ResidueField) default} = {I}

Tactic:
Set.singleton_eq_singleton_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : PrimeSpectrum R
⊢ comap (algebraMap R I.asIdeal.ResidueField) default = I
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
⊢ (Ideal.map (algebraMap R A) I).radical = Ideal.map (algebraMap R A) q

Tactic:
have : IsLocalRing A := AtPrime.isLocalRing A q

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
⊢ (Ideal.map (algebraMap R A) I).radical = Ideal.map (algebraMap R A) q
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑↑((piLocalizationToMaximal ((i : ι) → R i)).comp (toPiLocalization ((i : ι) → R i)))

Tactic:
exact (piLocalizationToMaximal_surjective _).comp surj

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

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

Tactic:
exact ⟨a, hs, Or.inl le_rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = {x}.compl

Tactic:
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (toDual s.compl.compl) ↔ ∃ x, s.compl.compl = {x}.compl
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ⊥ ∈ ⋂ i ∈ S, ↑i.toLowerSet

Tactic:
Set.mem_iInter₂

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

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : a ∈ ⋂ i ∈ S, ↑i.toLowerSet
b : P
hb : b ∈ ⋂ i ∈ S, ↑i.toLowerSet
⊢ a ⊔ b ∈ ⋂ i ∈ S, ↑i.toLowerSet

Tactic:
Set.mem_iInter₂

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : ∀ i ∈ S, a ∈ ↑i.toLowerSet
b : P
hb : ∀ i ∈ S, b ∈ ↑i.toLowerSet
⊢ ∀ i ∈ S, a ⊔ b ∈ ↑i.toLowerSet
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
by
  refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩
  calc
    x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
    _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left _ _ _

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

Tactic:
by
  dsimp only [sequenceOfCofinals, Nat.add]
  rw [Encodable.encodek]
  apply Cofinal.above_mem

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case refine_1
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ I ∈ SetLike.coe '' S, IsIdeal I

Tactic:
simp [Ideal.isIdeal]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
⊢ K ∈ range toCompacts ↔ (↑K).Nonempty

Tactic:
refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
⊢ K ∈ range toCompacts → (↑K).Nonempty
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ PrimeSpectrum.comap (id R) p = p

Tactic:
PrimeSpectrum.comap_id

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ (fun x ↦ x) p = p
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
refine Module.flat_of_isLocalized_span _ _ s hsp _
    (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_

Goal state after:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus s

Tactic:
← isOpen_compl_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsOpen Zᶜ ↔ ∃ s, Z = zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ IsClosed (zeroLocus s)

Tactic:
rw [isClosed_iff_zeroLocus]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

Tactic:
rintro h x y

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ I, z₁ = zeroLocus ↑I) → (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
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), x ⊓ y ≤ I.radical → x ≤ I.radical ∨ y ≤ I.radical) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
hI.radical

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
· simp [mul_smul, ← Nat.cast_smul_eq_nsmul A]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (Set.range (comap f))

Tactic:
range_comap_of_surjective _ f hf

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (zeroLocus ↑(ker f))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Submonoid.powers g = ⊤

Tactic:
by
  ext x
  simp [mem_powers_of_prime_card h hg]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
h : H ≤ zpowers g
⊢ ∃ n, H = zpowers (g ^ n)

pp: case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g

Tactic:
· obtain ⟨x, rfl⟩ := (H.isCyclic_iff_exists_zpowers_eq_top).mp (isCyclic_of_le h)
    obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp <| h (mem_zpowers x)
    obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k
    · exact ⟨n, by rw [zpow_natCast]⟩
    · exact ⟨n, by simp⟩

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ IsClopen ↑(basicOpen e)

Tactic:
exact isClopen_basicOpen_of_mul_add e f mul add

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ ¬Subsingleton G

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ Nontrivial G
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 α
hpos : 0 < #{a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d

Tactic:
by
  induction d using Nat.strong_induction_on with | _ d IH
  rcases Decidable.eq_or_ne d 0 with (rfl | hd0)
  · cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)
  rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩
  have ha : orderOf a = d := (mem_filter.1 ha').2
  have h1 :
    (∑ m ∈ d.properDivisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.properDivisors, φ m := by
    refine Finset.sum_congr rfl fun m hm => ?_
    simp only [mem_properDivisors] at hm
    refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
    rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
  have h2 :
    (∑ m ∈ d.divisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.divisors, φ m := by
    rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
  simpa [← cons_self_properDivisors hd0, ← h1] using h2

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

Goal state before:
pp: case h
α : 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 : ℕ
hm : m ∈ c.divisors.erase d
⊢ #{a | orderOf a = m} ≤ φ m

Tactic:
have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto

Goal state after:
case h
α : 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 : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
⊢ #{a | orderOf a = m} ≤ φ 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
⊢ y ^ (-n) * b ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ g ^ (ngn * nn) = 1

Tactic:
rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  (normalizer ↑((↑P).subgroupOf (normalizer ↑(normalizer ↑↑P)))).Normal →
    ((↑P).subgroupOf (normalizer ↑(normalizer ↑↑P))).Normal
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P

Tactic:
normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer),

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  (normalizer ↑((↑P).subgroupOf (normalizer ↑(normalizer ↑↑P)))).Normal → normalizer ↑(normalizer ↑↑P) ≤ normalizer ↑↑P
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsCoatom f.ker

Tactic:
rw [← isSimpleModule_iff_isCoatom]

Goal state after:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsSimpleModule R (M ⧸ f.ker)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n + 1]
        (single R j m) =
    single R (n + 1 + j) (r • m)

Tactic:
rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
    congr 2
    rw [Nat.one_add]
    exact congr(ofCoeff R $(Finsupp.mapDomain_single))

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

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
⊢ ↑(μ i) • x ∈ torsionBySet R M ↑(p i)

Tactic:
rw [mem_torsionBySet_iff] at hx ⊢
      rintro ⟨a, ha⟩
      rw [smul_smul]
      suffices a * μ i ∈ ⨅ i ∈ S, p i from hx ⟨_, this⟩
      rw [mem_iInf]
      intro j
      rw [mem_iInf]
      intro hj
      by_cases ij : j = i
      · rw [ij]
        exact Ideal.mul_mem_right _ _ ha
      · have := coe_mem (μ i)
        simp only [mem_iInf] at this
        exact Ideal.mul_mem_left _ _ (this j hj ij)

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (comp p) (single R i m) = p ^ i • single R 0 m

Tactic:
comp_apply,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (eval p) ((map R[X] (lsingle R 0)) (single R i m)) = p ^ i • single R 0 m
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ (comp p) (p' • q) = p'.comp p • (comp p) q

Tactic:
comp_apply,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ (eval p) ((map R[X] (lsingle R 0)) (p' • q)) = p'.comp p • (comp p) q
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsAddTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0

Tactic:
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩

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
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
⊢ (if n' ≤ n + 1 then (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m else 0) ∈ I • F.N n

Tactic:
if_pos (show n' ≤ n + 1 by lia)

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
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
⊢ (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ I.toCotangent.ker ↔ ↑x ∈ I ^ 2

Tactic:
rw [← I.map_toCotangent_ker]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ I.toCotangent.ker ↔ ↑x ∈ Submodule.map (Submodule.subtype I) I.toCotangent.ker
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
x✝ : (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal
y : R
hy : y ∈ ↑I
e : (Quotient.mk (I ^ 2)).toSemilinearMap y = (Quotient.mk (I ^ 2)) x
⊢ x ∈ I

Tactic:
simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero
    ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp e))

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : R
hr₁ : r ∈ I
hr₂ : ∀ n ∈ N, r • n = n
H : x ∈ ⨅ i, I ^ i • ⊤
⊢ ∃ r, ↑r • x = x

Tactic:
exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom
inst✝ : F.Monoidal
X : C
⊢ (F.obj m).map ((unitOfTensorIsoUnit F m n h₁).symm.hom.app X) ≫
      (unitOfTensorIsoUnit F n m h₂).hom.app ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)

Tactic:
dsimp
    simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, η_app_obj, Category.assoc,
      obj_μ_inv_app, Functor.map_comp, δ_μ_app_assoc, obj_ε_app,
      unitOfTensorIsoUnit_inv_app]
    simp only [← NatTrans.comp_app, ← F.map_comp, ← H, inv_hom_whiskerRight_assoc,
      Iso.inv_hom_id, Functor.map_id, NatTrans.id_app]

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 ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Tactic:
C.dFrom_eq r

Goal state after:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (0 + 2) (0 + 1) =
    (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} ↦ succ') 0).hom ≫ (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (0 + 1) 0)).snd.fst

Tactic:
dsimp [mk'XIso, mk']
    rw [mk_d_2_1]
    apply mk'_congr_succ'_d
    rw [mk_d_1_0]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm.hom = (shiftComm X j i).hom

Tactic:
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

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

Goal state before:
pp: case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.Exact → ∀ (i : ι), (S.map (eval C c i)).Exact

Tactic:
intro hS

Goal state after:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
⊢ ∀ (i : ι), (S.map (eval C c i)).Exact
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact → ∀ (i : ι), (S.map (eval C c i)).ShortExact

Tactic:
intro hS

Goal state after:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
⊢ ∀ (i : ι), (S.map (eval C c i)).ShortExact