mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) ∈ cocycles₁ (A.quotientToInvariants S)

Tactic:
rw [mem_cocycles₁_iff]

Goal state after:
case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ ∀ (g h : G ⧸ S),
    Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
      ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f (t * (x✝¹ * x✝)), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (t * x✝¹), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (t * x✝), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp [mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f ((x✝¹ * x✝)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (x✝¹⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (x✝⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp [mul_assoc]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
le_iff_exists_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := I.adicTopology
this : (Filter.map (fun y ↦ x + y) (𝓝 0)).HasBasis (fun _n ↦ True) fun i ↦ (fun y ↦ x + y) '' ↑(I ^ i)
⊢ (𝓝 x).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ x + y) '' ↑(I ^ n)

Tactic:
map_add_left_nhds_zero x

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := I.adicTopology
this : (𝓝 x).HasBasis (fun _n ↦ True) fun i ↦ (fun y ↦ x + y) '' ↑(I ^ i)
⊢ (𝓝 x).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ x + y) '' ↑(I ^ n)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
⊢ ModuleCat.Hom.hom ((chainsMap (MonoidHom.id G) φ).f i) = mapRange.linearMap (Hom.hom φ).toLinearMap

Tactic:
by
  refine lhom_ext fun _ _ => ?_
  simp [chainsMap_f, MonoidHom.coe_id]

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
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f 0).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ HomologicalComplex.Hom.f 0 i✝)) x✝) a✝

Tactic:
simp [chainsMap_f, LinearMap.zero_apply (M₂ := B)]

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)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ ∃ a, f a = m

Tactic:
use (maximalIdeal R).toCotangent ⟨l, lmem⟩

Goal state after:
case h
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 := ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ f ((maximalIdeal R).toCotangent ⟨l, lmem⟩) = m
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
⊢ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ

Tactic:
by
  ext x
  simp [chainsMap_f, chainsIso₁]

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤

Tactic:
← Ideal.Quotient.eq

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f (degree x + 1))) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
⊢ p.IsPrimitive ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
isPrimitive_iff_contentIdeal_eq_top,

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
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
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ n, IsLocalizedModule.mk' f (r ^ n • x) (s ^ n) ∈ ⊥

Tactic:
mem_bot,

Goal state after:
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
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ n, IsLocalizedModule.mk' f (r ^ n • x) (s ^ n) = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
⊢ (if n✝ = 0 then 1 else 0) = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : n✝ = 0
⊢ 1 = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ 0 = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0
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
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n✝ (g (f a)) = g (hJ.dpow n✝ (f a))

Tactic:
hg.2

Goal state after:
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
n✝ : ℕ
a : A
ha : a ∈ I
⊢ g (hJ.dpow n✝ (f a)) = g (hJ.dpow n✝ (f a))

case a
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
n✝ : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsRegular M as ↔ IsRegular M₂ bs

Tactic:
by
  conv => congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
  let e' := QuotientAddGroup.congr _ _ e <|
    AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective h
  exact and_congr (e.isWeaklyRegular_congr h) e'.nontrivial_congr

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤

Tactic:
ne_eq

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧
    IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
      ⊤ ≠ Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤

Tactic:
ne_eq

Goal state after:
case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧
    IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
      ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
n : ℕ
l : M
⊢ (map R f) (dp R n l) = ↑(X (n, f l))

Tactic:
rw [map_apply_dp, dp]

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

Goal state before:
pp: A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
by_cases ha : a ∈ I

Goal state after:
case pos
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

case neg
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ : a ∈ I
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e (hI.dpow m✝ (hI.dpow n✝ (e.symm x✝))) = ↑(m✝.uniformBell n✝) * e (hI.dpow (m✝ * n✝) (e.symm x✝))

Tactic:
rw [hI.dpow_comp hn]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e (↑(m✝.uniformBell n✝) * hI.dpow (m✝ * n✝) (e.symm x✝)) = ↑(m✝.uniformBell n✝) * e (hI.dpow (m✝ * n✝) (e.symm x✝))

A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ ↑n ! = ↑n ! • 1

Tactic:
cast_smul_eq_nsmul,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ ↑n ! = n ! • 1
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
⊢ ↑n ! ≠ ↑0

Tactic:
ne_eq

Goal state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x✝ x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
a✝ : k ∈ Finset.range (m + 1)
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
by_cases hk0 : k = 0

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x✝ x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
a✝ : k ∈ Finset.range (m + 1)
hk0 : k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x✝ x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
a✝ : k ∈ Finset.range (m + 1)
hk0 : ¬k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⟨(sSup S).carrier, ⋯⟩ = ⨆ a ∈ S, ⟨a.carrier, ⋯⟩

Tactic:
conv_rhs => rw [iSup]

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⟨(sSup S).carrier, ⋯⟩ = sSup (Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
⊢ I = ⊥ ∨ I = Ideal.span {ε} ∨ I = ⊤

Tactic:
by
  refine (eq_or_ne I ⊥).imp_right fun hb ↦ ?_
  refine (eq_or_ne I ⊤).symm.imp_left fun ht ↦ ?_
  have hd : ∀ x ∈ I, ε ∣ x := by
    intro x hxI
    rcases isUnit_or_isNilpotent x with hx | hx
    · exact absurd (Ideal.eq_top_of_isUnit_mem _ hxI hx) ht
    · rwa [← isNilpotent_iff_eps_dvd]
  have hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x := by
    intro x hxI hx0
    obtain ⟨r, rfl⟩ := hd _ hxI
    have : ε * r = (fst r) • ε := by ext <;> simp
    rw [this] at hxI hx0 ⊢
    have hr : fst r ≠ 0 := by
      contrapose hx0
      simp [hx0]
    refine ⟨r⁻¹, ?_⟩
    simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr]
  refine le_antisymm ?_ ?_ <;> intro x <;>
    simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]
  · intro hx
    simp_rw [hd _ hx]
  · intro hx
    obtain ⟨p, rfl⟩ := hx
    obtain ⟨y, hyI, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb
    obtain ⟨r, hr⟩ := hd' _ hyI hy0
    rw [(commute_eps_left _).eq, hr, ← mul_assoc]
    exact Ideal.mul_mem_left _ _ hyI

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
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
⊢ φ = ψ

Tactic:
have : H.localize = H'.localize := by
    apply Algebra.FormallyUnramified.ext_of_iInf _
      (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')
    intro x
    rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]
  ext x
  apply IsLocalization.injective (Localization.AtPrime Q) hQ
  rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]

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
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
⊢ φ = ψ

Tactic:
by
  have : H.localize = H'.localize := by
    apply Algebra.FormallyUnramified.ext_of_iInf _
      (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')
    intro x
    rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]
  ext x
  apply IsLocalization.injective (Localization.AtPrime Q) hQ
  rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]

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

Goal state before:
pp: case pos
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

Tactic:
simp [invOneSubPow, Ring.choose_zero_ite, hn]

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

Goal state before:
pp: case neg
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : ¬n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

Tactic:
simp [invOneSubPow, Ring.choose_zero_ite, hn]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingUp R S ↔ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
refine ⟨?_, fun h ↦ ⟨fun {q} hq P hP hlt ↦ ?_⟩⟩
  · intro h P q hq
    simp only [flip] at hq
    rw [← PrimeSpectrum.le_iff_specializes] at hq
    obtain ⟨Q, hle, hQ, h⟩ := P.asIdeal.exists_ideal_ge_liesOver_of_le (q := q.asIdeal)
      (p := P.asIdeal.under R) hq
    refine ⟨⟨Q, hQ⟩, (PrimeSpectrum.le_iff_specializes P _).mp hle, ?_⟩
    ext : 1
    exact h.over.symm
  · have : PrimeSpectrum.comap (algebraMap R S) ⟨P, hP⟩ ⤳ (⟨q, hq⟩ : PrimeSpectrum R) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
    obtain ⟨Q, hs, heq⟩ := h this
    refine ⟨Q.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, Q.2, ⟨?_⟩⟩
    simpa [PrimeSpectrum.ext_iff] using heq.symm

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
I : Ideal R
hIn : I ≠ ⊥
a✝ : I.IsPrime
x : R
hxI : x ∈ I
hx0 : x ≠ 0
⊢ ∃ x ∈ I, Prime x

Tactic:
rcases Ideal.exists_minimalPrimes_le (I.span_singleton_le_iff_mem.mpr hxI) with ⟨p, hpmin, hpl⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
I : Ideal R
hIn : I ≠ ⊥
a✝ : I.IsPrime
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : Ideal R
hpmin : p ∈ (Ideal.span {x}).minimalPrimes
hpl : p ≤ I
⊢ ∃ x ∈ I, Prime x
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
⊢ UniqueFactorizationMonoid R

Tactic:
rw [iff_exists_prime_mem_of_isPrime]
  intro I hIn _
  rcases I.ne_bot_iff.mp hIn with ⟨x, hxI, hx0⟩
  rcases Ideal.exists_minimalPrimes_le (I.span_singleton_le_iff_mem.mpr hxI) with ⟨p, hpmin, hpl⟩
  have : p.IsPrime := hpmin.isPrime
  have hpn : p ≠ ⊥ := fun hpb ↦ hx0 <|
    Ideal.span_singleton_eq_bot.mp <| bot_unique (hpmin.le.trans_eq hpb)
  have hpp : p.IsPrincipal := h p <| le_antisymm
    (Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes _ p hpmin)
      (by simpa [Order.one_le_iff_ne_zero])
  exact ⟨hpp.generator p, hpl (hpp.generator_mem p), hpp.prime_generator_of_isPrime p hpn⟩

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

Goal state before:
pp: case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊥

pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤

Tactic:
· exact WithBot.coe_ne_bot

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤