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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : Additive G →+ ↑A
g h : G
⊢ (⇑f ∘ ⇑Additive.ofMul) (g * h) = (A.ρ g) ((⇑f ∘ ⇑Additive.ofMul) h) + (⇑f ∘ ⇑Additive.ofMul) g

Tactic:
simp only [Function.comp_apply, ofMul_mul, map_add,
      isTrivial_apply A.ρ g (f (Additive.ofMul h)), add_comm (f (Additive.ofMul g))]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
by
  have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g
  simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g]
    at this
  exact sub_eq_sub_iff_add_eq_add.2 this.symm

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 (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, False ∨ si ≤ xi

Tactic:
false_or

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g • a = a

Tactic:
by
  rw [← (MulAction.bijective g⁻¹).1.eq_iff]
  simp [IsCycle₁, eq_comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
⊢ optionInvFunLeft σ R (optionFunLeft σ R x✝) = x✝

Tactic:
by ext; simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
⊢ optionFunLeft σ R (optionInvFunLeft σ R x✝) = x✝

Tactic:
by ext; simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ mapShortComplexH1 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH1 A)

Tactic:
ext <;> simp [shortComplexH1]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
x : S
hx : IsAlgebraic ℤ x
⊢ Algebra.natDenominator x ≠ 0

Tactic:
Algebra.natDenominator_def,

Goal state after:
S : Type u_2
inst✝ : CommRing S
x : S
hx : IsAlgebraic ℤ x
⊢ (Algebra.denominator ℤ x).natAbs ≠ 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
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨mapDomain s x, ?m.110⟩) =
    ↑⟨x, hx⟩

Tactic:
simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
g : G
⊢ (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ((↑x + (ConcreteCategory.hom (d₂₁ A)) W) g) =
    (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) (((lmapDomain (↑A) k ⇑S.subtype) Z) g)

Tactic:
by
      have := Finsupp.ext_iff.1 (congr($((mapShortComplexH1 (B := toCoinvariants A S)
        (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₁₂.symm) W)) g
      simp only [shortComplexH1, mapShortComplexH1_τ₂, ModuleCat.ofHom_comp, MonoidHom.coe_id,
        lmapDomain_id, ModuleCat.ofHom_id, res_obj_ρ, hom_ofHom, Category.id_comp,
        mapShortComplexH1_τ₁, Prod.map_id, ModuleCat.hom_comp, ModuleCat.hom_ofHom,
        LinearMap.coe_comp, Function.comp_apply, mapRange.linearMap_apply, mapRange_apply] at this
      simp only [← mapRange_apply (f := Coinvariants.mk <| A.ρ.comp S.subtype)
        (hf := map_zero _) (a := g), ← mapRange.linearMap_apply (R := k)]
      simp [← mapDomain_mapRange, hZ, this, hW, hzw, coe_mapCycles₁ S.subtype,
        coe_mapCycles₁ (MonoidHom.id G)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p q : R[X]
hpq : p ∣ q
⊢ q.contentIdeal ≤ p.contentIdeal

Tactic:
by
  obtain ⟨p', rfl⟩ := hpq
  exact le_trans (p.contentIdeal_mul_le_mul_contentIdeal p') mul_le_left

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case left
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) ≤ ↑1

pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1

Tactic:
· exact v.valuation_le_one x

Goal state after:
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1
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 : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
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)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
⊢ i < n + 1

Tactic:
omega

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 : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
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)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
⊢ i + 1 < n + 1

Tactic:
omega

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 : 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
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
⊢ i < n

Tactic:
omega

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

Goal state before:
pp: case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N

Goal state after:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
e : M₂ ⊗[R] QuotSMulTop r N ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')
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]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} = ⊤
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ I = Ideal.span {ε}

Tactic:
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]

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
⊢ I = Ideal.span {ε}
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]; rfl

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr.refine_1
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)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
⊢ Module.FaithfullyFlat R V

Tactic:
have : Module.FaithfullyFlat R S := by
        apply Module.FaithfullyFlat.of_comap_surjective
        rw [← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
        intro p
        simp [hn]
      exact Module.FaithfullyFlat.trans R S V

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
this : Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R))
φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
  (map (Submonoid.powers a)) φ
m : Ideal (Localization.Away a)
x✝ : m.IsMaximal
⊢ rankAtStalk (LocalizedModule.Away a (Fin n →₀ R)) { asIdeal := m, isPrime := ⋯ } =
    rankAtStalk (LocalizedModule.Away a M) { asIdeal := m, isPrime := ⋯ }

Tactic:
obtain ⟨𝔪, _, hm𝔪⟩ : ∃ 𝔪 : Ideal R, 𝔪.IsMaximal ∧ PrimeSpectrum.comap
        (algebraMap R (Localization (Submonoid.powers a))) ⟨m, inferInstance⟩ ≤ 𝔪 :=
      (m.comap (algebraMap R (Localization.Away a))).exists_le_maximal Ideal.IsPrime.ne_top'

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
this : Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R))
φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
  (map (Submonoid.powers a)) φ
m : Ideal (Localization.Away a)
x✝ : m.IsMaximal
𝔪 : Ideal R
left✝ : 𝔪.IsMaximal
hm𝔪 :
  (PrimeSpectrum.comap (algebraMap R (Localization (Submonoid.powers a))) { asIdeal := m, isPrime := ⋯ }).asIdeal ≤ 𝔪
⊢ rankAtStalk (LocalizedModule.Away a (Fin n →₀ R)) { asIdeal := m, isPrime := ⋯ } =
    rankAtStalk (LocalizedModule.Away a M) { asIdeal := m, isPrime := ⋯ }
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.map (↑P.h1CotangentEquivCotangent) (Algebra.H1Cotangent.map R P.Ring S S).range =
    Submodule.map h1Cotangentι ⊤

Tactic:
← (Algebra.H1Cotangent.exact_map_δ R P.Ring S).linearMap_ker_eq,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.map (↑P.h1CotangentEquivCotangent) (H1Cotangent.δ R P.Ring S).ker = Submodule.map h1Cotangentι ⊤
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 = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
⊢ φ ζ = ζ ^ q

Tactic:
have h₂ := geom_sum_mul (ζ ^ (q + k - i)) k

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 = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) * (ζ ^ (q + k - i) - 1) = (ζ ^ (q + k - i)) ^ k - 1
⊢ φ ζ = ζ ^ q
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
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
obtain ⟨σ, hσ⟩ := exists_of_isInvariant R G Q

Goal state after:
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
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
a b : R⟦X⟧
⊢ (powerSeriesFamily x (a + b)).hsum = (powerSeriesFamily x a).hsum + (powerSeriesFamily x b).hsum

Tactic:
by
    simp only [powerSeriesFamily_add, hsum_add]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
n : ℕ
⊢ ((x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) (n + 1) =
    (powers x - ofFinsupp (Finsupp.single 0 1)) (n + 1)

Tactic:
simp [embDomain_apply, of_symm_smul_of_eq_mul, powers_of_orderTop_pos hx, pow_succ',
      -smul_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (powers x - x • powers x).hsum = 1

Tactic:
hsum_sub,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (powers x).hsum - (x • powers x).hsum = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
hrx : (single oinv) r * x = 1
⊢ 0 < (1 - (single oinv) r * x).orderTop

Tactic:
simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < 0 + y.order

Tactic:
zero_add

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < y.order
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
F : IdealFilter A
inst✝ : F.IsUniform
⊢ ∀ (x₀ : A) {U : Set A}, U ∈ F.addGroupFilterBasis.sets → ∃ V ∈ F.addGroupFilterBasis.sets, V ⊆ (fun x ↦ x * x₀) ⁻¹' U

Tactic:
by
    rintro x₀ U ⟨I, hI, rfl⟩
    refine ⟨I.colon {x₀}, ⟨I.colon {x₀}, IsUniform.colon_mem hI x₀, rfl⟩,
      fun a ha ↦ Set.mem_preimage.mpr (Submodule.mem_colon_singleton.mp ha)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
h' : IsIdempotentElem I
⊢ I.Pure

Tactic:
Ideal.isIdempotentElem_iff_of_fg _ h

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
h' : ∃ e, IsIdempotentElem e ∧ I = R ∙ e
⊢ I.Pure