mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < ↑(u i) * ε

Tactic:
apply mul_pos (Nat.cast_pos.2 _) εpos

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < u i
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 1 ≤ u i

Tactic:
apply Nat.le_floor

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ ↑1 ≤ c ^ i
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ Monotone fun n ↦ ∑ i ∈ range n, X i ω

Tactic:
intro m n hmn

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ ∑ i ∈ range n, X i ω) m ≤ (fun n ↦ ∑ i ∈ range n, X i ω) n
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
⊢ ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto
        (fun n ↦
          (↑n)⁻¹ •
            ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
        atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))

Tactic:
intro c s hs

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto
      (fun n ↦
        (↑n)⁻¹ •
          ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
      atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ X.d (n + 1 + 1) = 0

Tactic:
| succ n ih =>

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯ ↔ ∀ x ∈ p.support, n ≤ degree x

Tactic:
simp [restrictSupportIdeal, mem_restrictSupport_iff, Set.subset_def]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x) → IsBoundary₁ x

Tactic:
rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (g.1 • a))
    simp_all [sum_sum_index]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x) →
    IsBoundary₂ x

Tactic:
rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (g.1 • a))
    simp_all [sum_sum_index]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span (insert X (⇑C '' S))

Tactic:
rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span {X} ⊔ Ideal.map (C.comp constantCoeff) I
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i = iCycles A 1 ≫ (chainsIso₁ A).hom

Tactic:
by
  simp [isoCycles₁, iCycles, HomologicalComplex.iCycles, ShortComplex.iCycles]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ↔ T2Space R

Tactic:
I.ringFilterBasis.t2Space_iff_sInter_subset hI.symm,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ↔ ⋂₀ I.ringFilterBasis.sets ⊆ {0}
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case none
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) none = (optionElim i x) none

Tactic:
simp [embDomain_eq_mapDomain]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case some
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
val✝ : Fin n
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) (Option.some val✝) = (optionElim i x) (Option.some val✝)

Tactic:
simp [embDomain_eq_mapDomain]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm :
  (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈
    Submodule.restrictScalars R (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R ^ 2))
⊢ m = 0

Tactic:
← Ideal.smul_top_eq_map,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ maximalIdeal R ^ 2 • ⊤
⊢ m = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ cyclesMap f φ 1 ≫ (isoCycles₁ B).hom = (isoCycles₁ A).hom ≫ mapCycles₁ f φ

Tactic:
by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapShortComplexH1,
    chainsMap_f_1_comp_chainsIso₁ f]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ comap (↑s • ⊤).subtype ((lsum R) fun i ↦ ↑i • LinearMap.id).range = ⊤

Tactic:
smul_top_eq_range_lsum

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ comap ((lsum R) fun i ↦ ↑i • LinearMap.id).range.subtype ((lsum R) fun i ↦ ↑i • LinearMap.id).range = ⊤
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
have := p.coeff_mem_contentIdeal n
  rw [Submodule.IsPrincipal.mem_iff_eq_smul_generator] at this
  obtain ⟨_, ha⟩ := this
  simp [ha]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
  all_goals
  { simp only [shortComplexH2]
    ext
    simp [Prod.map] }

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
hn : 0 < n
⊢ ↑t ^ n ∈ ⊥.colon {r ^ n • x}

Tactic:
exact Ideal.pow_mem_of_mem _ (by simpa using! ht) n hn

Goal state after:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
⊢ False

Tactic:
have hexist : ∃ p ∈ associatedPrimes R M, Module.annihilator R N ≤ p := by
      rcases associatedPrimes.nonempty R M with ⟨Ia, hIa⟩
      apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp
      · rw [biUnion_associatedPrimes_eq_compl_regular R M]
        exact fun r hr ↦ h r hr
      · exact fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
hexist : ∃ p ∈ associatedPrimes R M, annihilator R N ≤ p
⊢ False
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n + 1)! * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ ↑(X (n, m) * X (p, m)) = ↑((n + p).choose n • X (n + p, m))

Tactic:
exact Quotient.sound <| RingCon.le_ringConGen _ _ Rel.mul

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = n + 1
⊢ ∀ i < n + 1, Subsingleton (Ext N M i)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.zero
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k 0 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
rw [dp_null]; split_ifs <;> simp [hx]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.map Coe.ringHom (Ideal.span {↑p}) = ⊤

Tactic:
rw [Ideal.map_span, Set.image_singleton, map_natCast]
    simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]
    exact Nat.Prime.ne_zero hp.elim

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ↑(⨆ (_ : J ∈ S), ⟨J.carrier, ⋯⟩) = ⨆ (_ : J ∈ S), ↑⟨J.carrier, ⋯⟩

Tactic:
simp [ciSup_pos hJ]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· lift b to K[ε]ˣ using hb
    exact ⟨b⁻¹ * a, by simp⟩

Goal state after:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ hI.dpow n (a + b) = hI'.dpow n (a + b)

Tactic:
hI.dpow_add ha.1 hb.1,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 a * hI.dpow k.2 b = hI'.dpow n (a + b)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
⊢ φ.toRingHom a = 0

Tactic:
hφ,

Goal state after:
A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
⊢ (Ideal.Quotient.mk J) a = 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ dpow hI f n x = 0

Tactic:
rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]

Goal state after:
case hnc
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ ¬∃ a, f ↑a = x
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ : ζ ^ m = 1
hk' : ↑m ∉ Q
⊢ φ ζ = ζ ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
set q := Nat.card (R ⧸ Q.under R)
  have hm : m ≠ 0 := by rintro rfl; exact hk' (by simp)
  obtain ⟨k, hk, hζ⟩ := IsPrimitiveRoot.exists_pos hζ hm
  have hk' : ↑k ∉ Q := fun h ↦ hk' (Q.mem_of_dvd (Nat.cast_dvd_cast (hζ.2 m ‹_›)) h)
  have : NeZero k := ⟨hk.ne'⟩
  obtain ⟨i, hi, e⟩ := hζ.eq_pow_of_pow_eq_one (ξ := φ ζ) (by rw [← map_pow, hζ.1, map_one])
  have (j : _) : 1 - ζ ^ ((q + k - i) * j) ∈ Q := by
    rw [← Ideal.mul_unit_mem_iff_mem _ ((hζ.isUnit NeZero.out).pow (i * j)),
      sub_mul, one_mul, ← pow_add, ← add_mul, tsub_add_cancel_of_le (by linarith), add_mul,
        pow_add, pow_mul _ k, hζ.1, one_pow, mul_one, pow_mul, e, ← map_pow, mul_comm, pow_mul]
    exact H _
  have h₁ := sum_mem (t := Finset.range k) fun j _ ↦ this j
  have h₂ := geom_sum_mul (ζ ^ (q + k - i)) k
  rw [pow_right_comm, hζ.1, one_pow, sub_self, mul_eq_zero, sub_eq_zero] at h₂
  rcases h₂ with h₂ | h₂
  · simp [h₂, pow_mul, hk'] at h₁
  replace h₂ := congr($h₂ * ζ ^ i)
  rw [one_mul, ← pow_add, tsub_add_cancel_of_le (by linarith), pow_add, hζ.1, mul_one] at h₂
  rw [h₂, e]

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
⊢ σ * σ'⁻¹ ∈ Ideal.inertia G Q

Tactic:
intro x
  simpa [mul_smul] using sub_mem (H (σ'⁻¹ • x)) (H' (σ'⁻¹ • x))

Goal state after: