mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
i : σ
⊢ (killCompl e) (X (e i)) = X i

Tactic:
classical
  ext; simp [coeff_X, coeff_killCompl, ← embDomain_single]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R

Tactic:
refine UniqueFactorizationMonoid.of_exists_prime_factors fun a ha ↦ ?_

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Group G✝
A✝ : Rep k✝ G✝
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
hx : IsBoundary₀ G x
⊢ x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)

Tactic:
rcases (isBoundary₀_iff G x).1 hx with ⟨y, rfl⟩

Goal state after:
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Group G✝
A✝ : Rep k✝ G✝
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
y : G →₀ A
hx : IsBoundary₀ G (y.sum fun g z ↦ g • z - z)
⊢ (y.sum fun g z ↦ g • z - z) ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) = 0

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ModuleCat.Hom.hom (d₂₁ A ≫ (chainsIso₁ A).inv)) ↑x = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
h :
  (shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso.hom
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ↑x ∈ boundaries₂ A

Tactic:
simp only [H2π, isoCycles₂, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
h :
  (shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso.hom
⊢ (ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π) x = 0 ↔ ↑x ∈ boundaries₂ A
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : k = 0 ∧ x = 0
h2 : k = 0
⊢ r = (coeff x) (C r)

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : k = 0 ∧ x = 0
h2 : ¬k = 0
⊢ r = (coeff x) 0

pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ 0 = (coeff x) (C r)

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : ¬k = 0
⊢ 0 = (coeff x) 0

Tactic:
· simp [h1.right]

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : k = 0 ∧ x = 0
h2 : ¬k = 0
⊢ r = (coeff x) 0

case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ 0 = (coeff x) (C r)

case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : ¬k = 0
⊢ 0 = (coeff x) 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ MvPolynomial.coeff x ((truncTotal m) p) = MvPolynomial.coeff x ((truncTotal n) p)

Tactic:
coeff_truncTotal _ (by lia),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ (coeff x) p = MvPolynomial.coeff x ((truncTotal n) p)
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 : ℕ
⊢ Function.Injective ⇑(ofPowSMul I M n)

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
  intro x hx; ext i
  simp only [AdicCompletion.ext_iff, val_zero, Pi.zero_apply] at hx
  specialize hx (i + n)
  rw [ofPowSMul_val_apply I (by rw [add_comm]),
    LinearMap.map_eq_zero_iff _ (powSMulQuotInclusion_injective ..)] at hx
  simp [hx]

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ Antitone fun n ↦ I ^ a n

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ ∀ (m : ℕ), (f m) x = (Submodule.factor ⋯) ((f (m + 1)) x)

Tactic:
· exact fun _ _ le ↦ Ideal.pow_le_pow_right (ha.monotone le)

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ ∀ (m : ℕ), (f m) x = (Submodule.factor ⋯) ((f (m + 1)) x)
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
x y : G ⧸ S
h : s x = s y
⊢ x = y

Tactic:
rw [← hs x, ← hs y, h]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ Bialgebra R (A ⧸ I)

Tactic:
refine .ofAlgHom (comulAlgHom I) (counitAlgHom I) ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
      ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)) =
    (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm

case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:

Tactic:
⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul

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

Goal state before:
pp: 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 : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    (if (IsLocalization.sec R⁰ ↑x).1 = 0 then 0
      else
        exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).1})).factors))) *
      (if (SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).2 = 0 then 0
        else
          exp
            (-↑((Associates.mk v.asIdeal).count
                  (Associates.mk (Ideal.span {(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).2})).factors)))⁻¹

Tactic:
SubmonoidClass.coe_subtype,

Goal state after:
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 : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    (if (IsLocalization.sec R⁰ ↑x).1 = 0 then 0
      else
        exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).1})).factors))) *
      (if ↑(IsLocalization.sec R⁰ ↑x).2 = 0 then 0
        else
          exp
            (-↑((Associates.mk v.asIdeal).count
                  (Associates.mk (Ideal.span {↑(IsLocalization.sec R⁰ ↑x).2})).factors)))⁻¹
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N

Tactic:
by
  convert! map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2
  exact Eq.trans (congrArg (· ⊓ N) (map_top _)) (map_comap_eq _ _).symm

Goal state after:
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'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
a : ↥T
⊢ (algebraMap R R') ↑a ∈ p

Tactic:
simpa [← Ideal.mem_comap, ← hT] using Ideal.subset_span a.2

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
⊢ (annihilator R M).minimalPrimes ⊆ associatedPrimes R M

Tactic:
intro p hp

Goal state after:
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
⊢ p ∈ associatedPrimes R M
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: 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
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
⊢ Nontrivial (Dual p.ResidueField Nₚ')

Tactic:
simpa using ntr

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'

Tactic:
by
  obtain ⟨hI, h₀, _⟩ := hI
  obtain ⟨hI', h₀', _⟩ := hI'
  simp only [mk.injEq]
  grind

Goal state after:
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
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial (ℕ × M) R
⊢ P ↑F

Tactic:
induction F using MvPolynomial.induction_on with

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
⊢ dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m

Tactic:
simp only [dp_def, ← RingCon.coe_mul, ← RingCon.coe_nsmul]
  exact Quotient.sound <| RingCon.le_ringConGen _ _ Rel.mul

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

Goal state before:
pp: 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) = ⊤
⊢ ⊤ ≤ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
intro p hp

Goal state after:
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) = ⊤
p : DividedPowerAlgebra R M
hp : p ∈ ⊤
⊢ p ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (Ideal.span {r} • ⊤ ⊔ Ideal.ofList l₁✝ • ⊤).toAddSubgroup

Tactic:
sup_toAddSubgroup,

Goal state after:
case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f ((Ideal.span {r} • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)
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:
dp_null

Goal state after:
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 * if k = 0 then 1 else 0) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| (Ideal.span {s} • ⊤ ⊔ Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
sup_toAddSubgroup,

Goal state after:
case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| (Ideal.span {s} • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
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
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
p : MvPolynomial (ℕ × M) R
⊢ (map S f) ↑p = (aeval fun nm ↦ dp S nm.1 (f nm.2)) p

Tactic:
by
  rw [map, lift'_apply]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
⊢ ε ∣ x

Tactic:
rcases isUnit_or_isNilpotent x with hx | hx

Goal state after:
case inl
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsUnit x
⊢ ε ∣ x

case inr
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
⊢ ε ∣ x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I • J
⊢ hI.dpow m x ∈ I • J

Tactic:
induction hx using Submodule.smul_induction_on' generalizing m with

Goal state after:
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
k : Type u
inst✝⁶ : Field k
Ω : Type w
inst✝⁵ : Field Ω
inst✝⁴ : Algebra R Ω
S : Type w
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra S Ω
inst✝ : IsScalarTower R S Ω
A B : FiniteEtale R
f : A ⟶ B
⊢ (baseChange R R).map f ≫ (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom =
    (isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ (𝟭 (FiniteEtale R)).map f

Tactic:
by
    dsimp [baseChange]
    ext
    simp

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

Goal state before:
pp: case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
⊢ ∀ (x y : A),
    x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} →
      y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} →
        (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
          (∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
            ∀ (n : ℕ), n ≠ 0 → hI.dpow n (x + y) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
intro x y hx hy hx_pow hy_pow n hn
      rw [hI.dpow_add' (hSI hx) (hSI hy)]
      apply Submodule.sum_mem (span _)
      intro m _
      by_cases hm0 : m = 0
      · rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn)
      · exact (span _).mul_mem_right _ (hx_pow m hm0)

Goal state after:
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 h1Cotangentι (map (defaultHom R S P)).range = Submodule.map h1Cotangentι ⊤

Tactic:
← LinearMap.range_comp,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (h1Cotangentι ∘ₗ map (defaultHom R S P)).range = Submodule.map h1Cotangentι ⊤
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
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)

Tactic:
exact congr_arg _

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✝ : Q.IsPrime
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Tactic:
by
  have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
      Nat.card (R ⧸ Q.under R) := by
    congr 2
    rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
  intro x
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq Q.primeCompl x
  simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h,
    ← IsLocalization.mk'_pow]
  rw [← IsLocalization.mk'_sub,
    IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]
  simp only [SubmonoidClass.coe_pow, ← Ideal.Quotient.eq_zero_iff_mem]
  simp [H.mk_apply]

Goal state after: