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)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ r • DFinsupp.coeFnAddMonoidHom x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier

Tactic:
refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if H : i ∈ x.support then (fun i ↦ r ↑i * x ↑i) ⟨i, H⟩ else 0) = (r • DFinsupp.coeFnAddMonoidHom x) i
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ x, x * a = 0 ∧ ¬x = 0

Tactic:
@and_comm (_ * _ = _),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ x, ¬x = 0 ∧ x * a = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
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
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J

Tactic:
rw [← IsLocalization.under_le_under_iff q.primeCompl A,
      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]
    apply hIq.2 hJ.1
    have := hJ.isPrime.ne_top
    rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this
    exact Set.disjoint_compl_left_iff_subset.mp this

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
f : BoundedLatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
by simp [h.range_eq]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)

Tactic:
| cons i s ih hi =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)

Tactic:
| cons i s ih hi =>

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case inr
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
hI : I.IsProper
J : Ideal P
hJ : IsCoatom J
hJ' : I ≤ J
⊢ ∃ J, I ≤ J ∧ J.IsMaximal

Tactic:
· exact ⟨J, hJ', isMaximal_iff_isCoatom.2 hJ⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)

Tactic:
| cons i s ih hi =>

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
intros; rw [pow_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset
hMI : id M ≤ I
⊢ I.IsMaximal

Tactic:
fin.mem_toFinset

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Set.range (comap (algebraMap R S)) = ↑(basicOpen r)

Tactic:
by
  rw [localization_comap_range S (Submonoid.powers r)]
  ext x
  simp only [mem_zeroLocus, basicOpen_eq_zeroLocus_compl, SetLike.mem_coe, Set.mem_ofPred_eq,
    Set.singleton_subset_iff, Set.mem_compl_iff, disjoint_iff_inf_le]
  constructor
  · intro h₁ h₂
    exact h₁ ⟨Submonoid.mem_powers r, h₂⟩
  · rintro h₁ _ ⟨⟨n, rfl⟩, h₃⟩
    exact h₁ (x.2.mem_of_pow_mem _ h₃)

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a =
    (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a

pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
· ring_nf

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
h' : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}.Nonempty
⊢ Nat.find h = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
Nat.sInf_def h'

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
h' : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}.Nonempty
⊢ Nat.find h = Nat.find h'
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : Nat.card ↥H ∣ Nat.card G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this

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

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

Tactic:
have := (zpowers g).eq_bot_or_eq_top_of_prime_card

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : zpowers g = ⊥ ∨ zpowers g = ⊤
⊢ zpowers g = ⊤
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ Fintype.card ↑(orbit (↥(zpowers a)) b) ≠ 0

Tactic:
exact Fintype.card_ne_zero

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(Nat.card G)]

Tactic:
hn,

Goal state after:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑n]
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), orderOf g ∣ p ^ k

Tactic:
refine isPGroup_iff_orderOf_dvd_pow.trans ⟨fun h ↦ ?_, fun ⟨k, hk⟩ ↦ fun g ↦ ⟨k, hk g⟩⟩

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : ∀ (g : G), ∃ k, orderOf g ∣ p ^ k
⊢ ∃ k, ∀ (g : G), orderOf g ∣ p ^ k
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p}) = ⊤

Tactic:
sup_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ Ideal.comap (mapRingHom f) (Ideal.span {p}) ⊔ Ideal.span {X} = ⊤
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
⊢ IsPGroup n (Multiplicative G)

Tactic:
by
  simpa [IsPGroup, Multiplicative.forall] using
    fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x

Tactic:
exact map_intCast_smul f _ _ (cast c) x

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) →
    vanishingIdeal (closure s) ∈ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ 1 = Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P))

Tactic:
← Nat.card_unique (α := ({⟨P, mem_orbit_self P⟩} : Set (orbit G P))),

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ Nat.card ↑{⟨P, ⋯⟩} = Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P))
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
⊢ (x ^ n)⁻¹ * f b = 1

Tactic:
hn,

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
⊢ (f b)⁻¹ * f b = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ (b ^ p ^ n) ^ p ^ m = 1

Tactic:
hn,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ 1 ^ p ^ m = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
    rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
    rwa [← Subgroup.topEquiv.isCyclic, ← h]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card G = s * p * p ^ n

Tactic:
hs,

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ s * p ^ (n + 1) = s * p * p ^ n
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card G = s * p * p ^ n

Tactic:
hs,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ s * p ^ (n + 1) = s * p * p ^ n
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 ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
rw [Finset.coe_cons, Set.pairwise_insert_of_symm]

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 ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M × Submodule R M
h✝ : Iso X Y
e : Submodule R M × Submodule R M → Submodule R M × Submodule R M → Prop :=
  fun X Y ↦ Nonempty ((↥X.2 ⧸ Submodule.comap X.2.subtype X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap Y.2.subtype Y.1)
x✝ y✝ : Submodule R M
h : IsMaximal x✝ (x✝ ⊔ y✝)
⊢ e (x✝, x✝ ⊔ y✝) (x✝ ⊓ y✝, y✝)

Tactic:
sup_comm,

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M × Submodule R M
h✝ : Iso X Y
e : Submodule R M × Submodule R M → Submodule R M × Submodule R M → Prop :=
  fun X Y ↦ Nonempty ((↥X.2 ⧸ Submodule.comap X.2.subtype X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap Y.2.subtype Y.1)
x✝ y✝ : Submodule R M
h : IsMaximal x✝ (x✝ ⊔ y✝)
⊢ e (x✝, y✝ ⊔ x✝) (x✝ ⊓ y✝, y✝)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
⊢ X • (of R M a) m = (of R M a) (a • m)

Tactic:
← of_aeval_smul,

Goal state after:
R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
⊢ (of R M a) ((aeval a) X • m) = (of R M a) (a • m)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ X ^ n • (of R M a) m = (of R M a) (a ^ n • m)

Tactic:
← of_aeval_smul,

Goal state after:
R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ (of R M a) ((aeval a) (X ^ n) • m) = (of R M a) (a ^ n • m)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ Iso ((eraseLast s).last, last s) ((snoc t (eraseLast s).last ⋯).last, last s)

Tactic:
simpa using iso_refl

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
r : R
hr : r ∈ I ^ n
⊢ (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
by
  induction n generalizing r with
  | zero => exact Subalgebra.algebraMap_mem _ _
  | succ n hn =>
    rw [pow_succ'] at hr
    refine Submodule.smul_induction_on hr ?_ ?_
    · intro r hr s hs
      rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]
      exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)
    · intro x y hx hy
      rw [map_add]
      exact Subalgebra.add_mem _ hx hy

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N = J • N' ⊔ N
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
sup_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N ⊔ N' = J • N' ⊔ N
⊢ N ⊔ N' = N ⊔ J • N'
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
N : Submodule R M
⊢ (I.stableFiltration N).Stable

Tactic:
use 0

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
⊢ ∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
Module: Mathlib.RingTheory.Nakayama

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
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N ≤ I • N ⊔ N'
⊢ N ≤ N' ⊔ I • N

Tactic:
sup_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N ≤ I • N ⊔ N'
⊢ N ≤ I • N ⊔ N'
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case h.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ Set.InjOn (⇑(I • N).mkQ) (Quotient.out '' s)

Tactic:
simp [Set.InjOn]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ f.range ⊔ I • ⊤ = ⊤

Tactic:
sup_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ I • ⊤ ⊔ f.range = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
refine Or.inl (eq_bot_iff.mpr ?_)

Goal state after:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ ⊥
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ j = k

Tactic:
exact c.next_eq rij rik

Goal state after:
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
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d : M.Derivation φ
X : Dᵒᵖ
⊢ d.d 1 = 0

Tactic:
simpa using d.d_mul (X := X) 1 1

Goal state after:
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
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom
        ((relativeDifferentials' φ').map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map (d'.app Y).desc))
      (CommRingCat.KaehlerDifferential.d b) =
    (ConcreteCategory.hom ((d'.app X).desc ≫ M'.map f)) (CommRingCat.KaehlerDifferential.d b)

Tactic:
by
          dsimp
          rw [ModuleCat.Derivation.desc_d, Derivation'.app_apply]
          erw [relativeDifferentials'_map_d φ' f]
          simp

Goal state after: