mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ cycles₁ A = ⊤

Tactic:
by
  rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤

Tactic:
simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤

Tactic:
suffices ∀ (a : R) (i : ℕ), ∃ j : ℕ, a • I ^ j ≤ I ^ i by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x

Tactic:
obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
    obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
    simp only [ncard_singleton, ncard_eq_one] at h
    obtain ⟨_, rfl⟩ := h
    exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

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
n : ℕ
⊢ map (g.comp f) (φ ≫ (resFunctor f).map ψ) n = map f φ n ≫ map g ψ n

Tactic:
simp [map, ← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]

Goal state after:
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
⊢ mapShortComplexH1 f 0 = 0

Tactic:
by
  refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
  all_goals
  { simp only [shortComplexH1]
    ext
    simp }

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 : ℕ
h : I.FG
⊢ I ^ n • ⊤ = (eval I M n).ker

Tactic:
classical
  refine le_antisymm (pow_smul_top_le_ker_eval ..) ?_
  replace h := Ideal.FG.pow (n := n) h
  rcases h with ⟨s, hs⟩
  simp only [← hs, span_smul_eq]
  rw [← restrictScalars_top R (AdicCompletion I R) (AdicCompletion I M),
    ← restrictScalars_image_smul_eq (R := AdicCompletion I R),
    ← restrictScalars_range_ofPowSMul_eq_ker_eval, restrictScalars_le,
    image_smul_top_eq_range_lsum]
  simp only [SetLike.coe_sort_coe]
  rw [← LinearMap.range_comp_of_range_eq_top (f := (finsuppLEquivDirectSum ..).symm.toLinearMap)
    _ (by simp), lsum_smul_comp_finsuppLEquivDirectSum_symm,
    LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range _),
    LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top_of_surjective _ <|
      Function.RightInverse.surjective (g := map I (finsuppLEquivDirectSum R M s)) (fun _ ↦ by
      simp [← LinearMap.comp_apply, map_comp]))]
  rintro _ ⟨x, rfl⟩
  have : Function.Surjective ((lsum R fun i : s ↦ i.val • (LinearMap.id : M →ₗ[R] M)).codRestrict
    (I ^ n • ⊤) (fun _ ↦ by simp [← hs, span_smul_eq, smul_top_eq_range_lsum])) := by
    rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]
    simp
  rcases map_surjective I this x with ⟨x, rfl⟩
  exact ⟨x, by rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]⟩

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDomain B
C : Type u_3
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
inst✝¹ : Module.IsTorsionFree B C
inst✝ : Module.IsTorsionFree A C
I : ↥(Ideal A)⁰
⊢ extendedIdeal B C (extendedIdeal A B I) = extendedIdeal A C I

Tactic:
simp [Ideal.map_map, IsScalarTower.algebraMap_eq A B C]

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

Goal state before:
pp: case h.refine_2
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)
⊢ IsLocalization.mk' R' r s ∈ p

Tactic:
rw [this]

Goal state after:
case h.refine_2
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)
⊢ IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: 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'
ass : Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M
⊢ p ∈ associatedPrimes R' M'

Tactic:
rcases ass with ⟨hp, x, hx⟩
  constructor
  · refine (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩
    by_contra eqtop
    simp [eqtop, Ideal.comap_top, Ideal.isPrime_iff] at hp
  · use f x
    ext t
    rcases IsLocalization.exists_mk'_eq S t with ⟨r, s, hrs⟩
    simp_rw [← hrs, Ideal.mem_radical_iff, mem_colon_singleton, ← IsLocalizedModule.mk'_one S f,
      ← IsLocalization.mk'_pow, IsLocalizedModule.mk'_smul_mk', mul_one, mem_bot,
      IsLocalizedModule.mk'_eq_zero']
    refine ⟨fun h ↦ exists_comm.mp ⟨1, ?_⟩, fun ⟨n, t, ht⟩ ↦ ?_⟩
    · simp only [← mem_colon_singleton, one_smul, ← mem_bot R, ← hx, ← Ideal.mem_radical_iff]
      exact hSR'.mk'_mem_iff.mp h
    · have : hSR'.mk' R' r s = hSR'.mk' R' (t.1 * r) 1 * hSR'.mk' R' 1 (t * s) := by
        rw [← hSR'.mk'_mul, mul_one, one_mul, ← sub_eq_zero, ← hSR'.mk'_sub, Submonoid.coe_mul]
        simp [← mul_assoc, mul_comm r t.1, IsLocalization.mk'_zero]
      rw [this]
      apply Ideal.IsTwoSided.mul_mem_of_left
      rw [IsLocalization.mk'_one, ← Ideal.mem_comap, hx]
      rcases eq_zero_or_pos n with rfl | hn
      · exact Ideal.IsTwoSided.mul_mem_of_left _ ⟨1, by simpa using! ht⟩
      · use n
        rw [mem_colon_singleton, mul_pow, mul_smul, ← mem_colon_singleton]
        exact Ideal.pow_mem_of_mem _ (by simpa using! ht) n hn

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this✝ : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
ann_le : annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q
this : Disjoint ↑p.primeCompl ↑(Ideal.under R q)
⊢ Ideal.comap (algebraMap R Rₚ) q ≤ p

Tactic:
simpa only [Ideal.primeCompl, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      Set.disjoint_compl_left_iff_subset] using! this

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (N : ModuleCat R),
      Nontrivial ↑N →
        Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i)) →
    ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE

Tactic:
tfae_have 2 → 3 := fun h2 ↦ ⟨(ModuleCat.of R (Shrink.{v} (R ⧸ I))),
    inferInstance, Module.Finite.equiv (Shrink.linearEquiv R (R ⧸ I)).symm, suppQ, h2⟩

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (N : ModuleCat R),
      Nontrivial ↑N →
        Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i)) →
    ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)
tfae_2_to_3 :
  (∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)) →
    ∃ N,
      Nontrivial ↑N ∧
        Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i)
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
a✝ : A
ha : a✝ ∈ I
⊢ hJ.dpow n (f a✝) = f (hI.dpow n a✝)

Tactic:
rw [hn, hI.dpow_zero ha, hJ.dpow_zero (hIJ (mem_map_of_mem f ha)), map_one]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
⊢ hI.IsDPMorphism hK (g.comp f)

Tactic:
by
  refine ⟨le_trans (map_map f g ▸ map_mono hf.1) hg.1, fun a ha ↦ ?_⟩
  simp only [RingHom.coe_comp, Function.comp_apply]
  rw [← hf.2 a ha, hg.2]
  exact hf.1 (mem_map_of_mem f ha)

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

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
⊢ 0 ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
simp only [mem_ofPred_eq, Submodule.zero_mem, map_zero, true_and]
    intro n
    induction n with
    | zero => rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]
    | succ n => rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]

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

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n✝ ((fromGens hI hJ hS h ⋯).toRingHom a) = (fromGens hI hJ hS h ⋯).toRingHom (hI.dpow n✝ a)

Tactic:
(fromGens hI hJ hS h hdp).dpow_comp a ha

Goal state after:
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
n✝ : ℕ
a : A
ha : a ∈ I
⊢ (fromGens hI hJ hS h ⋯).toRingHom (hI.dpow n✝ a) = (fromGens hI hJ hS h ⋯).toRingHom (hI.dpow n✝ a)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0) = 0

Tactic:
rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), mul_assoc, ← mul_assoc]

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ * (y ^ k.2 * x ^ k.1) = 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (iSup J)

Tactic:
rw [iSup_eq_span, span_isSubDPIdeal_iff (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)]

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ ⋃ i, ↑(J i), hI.dpow n s ∈ span (⋃ i, ↑(J i))
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
⊢ ⊤.carrier ⊓ ⨅ (_ : J ∈ S), J.carrier = I ⊓ ↑(⨅ (_ : J ∈ S), ⟨J.carrier, ⋯⟩)

Tactic:
rw [ciInf_pos hJ, ciInf_pos hJ]

Goal state after:
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
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑⟨J.carrier, ⋯⟩
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ (TensorProduct.lmul' T).Flat

Tactic:
rw [this]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ ((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e).Flat
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
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ Ideal.under R ⊤)
⊢ False

Tactic:
simp only [Ideal.comap_top] at h

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ ⊤)
⊢ False
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
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hζ : ζ ^ 0 = 1
hk' : ↑0 ∉ Q
⊢ False

Tactic:
exact hk' (by simp)

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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j + k * j) ∈ Q

Tactic:
pow_add,

Goal state after:
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
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j) * ζ ^ (k * j) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case inr
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
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k) = ζ ^ i
⊢ φ ζ = ζ ^ q

Tactic:
pow_add,

Goal state after:
case inr
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
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ q * ζ ^ k = ζ ^ i
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ invUnitsSub u * X = invUnitsSub u * C ↑u - 1

Tactic:
ext (_ | n)
  · simp
  · simp [pow_succ']

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

Goal state before:
pp: case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
n : ℕ
⊢ (coeff n) (mk 1 ^ (d + 1 + 1)) = (coeff n) (mk fun n ↦ ↑((d + 1 + n).choose (d + 1)))

Tactic:
pow_add,

Goal state after:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
n : ℕ
⊢ (coeff n) (mk 1 ^ (d + 1) * mk 1 ^ 1) = (coeff n) (mk fun n ↦ ↑((d + 1 + n).choose (d + 1)))
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
⊢ PowerSeries.subst (PowerSeries.subst F.zeroX F.zeroX) F.zeroX.substInv = PowerSeries.X

Tactic:
by
      rw [zeroX_subst_zeroX, F.zeroX.subst_substInv_left F.constantCoeff_zeroX]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![PowerSeries.X, 0] s)) F.toPowerSeries

Tactic:
congr! 2 with s
        fin_cases s
        · simp [PowerSeries.X, subst]
        · simp [subst, eval₂]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Tactic:
use Ideal.Quotient.mk _ b

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) b = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
this : x.order = 0
⊢ IsAddUnit x.order

Tactic:
rw [this]

Goal state after:
case inr.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
this : x.order = 0
⊢ IsAddUnit 0
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p : Ideal R
P : Ideal S
inst✝² : P.IsPrime
inst✝¹ : P.LiesOver p
inst✝ : p.IsPrime
hle : p ≤ p
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver p

Tactic:
use P

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
⊢ a = b

Tactic:
obtain ⟨c, _⟩ := exists_mul_sq_add_linear_part_eq_eval_add f a (b - a)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
⊢ a = b