mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
g : G
⊢ TensorProduct.lift
        (((lift (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) k
              H)
            fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g =
    TensorProduct.lift
      (((lift (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) k H)
          fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
        ↑(MonoidAlgebra.coeffLinearEquiv k))

Tactic:
by ext; simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff]
        using! Coinvariants.sub_mem_ker _ _

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
this :
  (ConcreteCategory.hom ((shortComplexH1 X.1).g ≫ (mapShortComplexH1 (MonoidHom.id G) X.f).τ₃)) x =
    (ConcreteCategory.hom ((mapShortComplexH1 (MonoidHom.id G) X.f).τ₂ ≫ (shortComplexH1 X.X₂).g)) x
⊢ (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) ((ModuleCat.Hom.hom (d₁₂ X.X₁)) x) = (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) 0

Tactic:
simp_all [shortComplexH1, LinearMap.compLeft]

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ d A n =
    (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

Tactic:
ext : 3
  simp [d_single (k := k), TensorProduct.tmul_add, TensorProduct.tmul_sum,
    barComplex.d_single (k := k)]

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
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f (g * h) = f g + f h

Tactic:
(mem_cocycles₁_iff f).1 f.2,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ (A.ρ g) (f h) + f g = f g + f h
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
⊢ f 1 = 0

Tactic:
simpa only [mul_one, one_smul, left_eq_add] using hf 1 1

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range A.ρ.norm

Tactic:
by
  simp [groupHomologyπOdd, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    ShortComplex.moduleCatToCycles, -LinearMap.mem_range, Rep.norm, LinearMap.range_codRestrict]

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  (ConcreteCategory.hom (H1π (of A.ρ)))
      ((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x) =
    0
y : ↑(ModuleCat.of k ↑(of A.ρ))
hy :
  (ModuleCat.Hom.hom (d₀₁ (of A.ρ))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x)
g✝ : G ⧸ S
g : G
⊢ ↑((ModuleCat.Hom.hom (d₀₁ (A.quotientToInvariants S))) ⟨y, ⋯⟩ ↑g) = ↑(x ↑g)

Tactic:
simpa [-SetLike.coe_eq_coe] using! congr_fun hy g

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 (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s ↦ (monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
by
  refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_
  simp_rw [le_iff_exists_add, add_comm]
  rfl

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]
    exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f 0) = (coeff n✝) 0

Tactic:
simp [coeff_renameFun]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ spanFinrank (Ideal.span S) ≤ spanFinrank (Ideal.map constantCoeff (Ideal.span S))

Tactic:
refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ S.ncard ≤ spanFinrank (Ideal.map constantCoeff (Ideal.span S))
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
by_cases hP : X ∈ P

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
hP : X ∈ P
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
hP : X ∉ P
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := ⋯
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
intro s hs
      simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
⊢ 0 = (coeff y) ((monomial x.some) r)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0

Tactic:
· replace h1 : ¬ y = x.some := fun h ↦ by
      absurd h1; ext u
      cases u <;> simp_all
    rw [coeff_monomial, if_neg h1]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((finSuccEquiv R n) (X j.succ))) =
    (coeff x) ((PowerSeries.coeff k) (PowerSeries.C (X j)))

Tactic:
simp_rw [coeff_coeff_finSuccEquiv, PowerSeries.coeff_C, coeff_X, cons_eq_single_succ_iff]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (if x = single j 1 ∧ k = 0 then 1 else 0) = (coeff x) (if k = 0 then X j else 0)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
this : (Ideal.map (Ideal.Quotient.mk I) m).IsMaximal
⊢ (Ideal.map (algebraMap R (AdicCompletion I R)) m).IsMaximal

Tactic:
mapeq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
this : (Ideal.map (Ideal.Quotient.mk I) m).IsMaximal
⊢ (comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)).IsMaximal
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ IsLocalRing (AdicCompletion (maximalIdeal R) R)

Tactic:
by
  have := AdicCompletion.isMaximal_map_of_le _ _ (le_refl _) fg
  have := AdicCompletion.isAdicComplete_self _ fg
  exact isLocalRing_of_isAdicComplete_maximal
    ((maximalIdeal R).map (algebraMap R (AdicCompletion (maximalIdeal R) R)))

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
φ : A ⟶ res f B
n : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B

Tactic:
have := congr($((mapShortComplexH1 f φ).comm₂₃) x)

Goal state after:
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 : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
this :
  (ConcreteCategory.hom ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Tactic:
by_cases hp0 : p = 0
  · simp [hp0]
  have hsupp_nonempty : p.support.Nonempty := by grind [support_nonempty]
  simp only [gaussNorm, hsupp_nonempty, ↓reduceDIte, one_pow, mul_one, contentIdeal, Ideal.span_le,
    Set.subset_def, SetLike.mem_coe, ← v.intAdicAbv_lt_one_iff hb]
  constructor
  · contrapose!
    simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]
    intro _ h1 h2
    exact Finset.le_sup'_of_le (fun n ↦ (v.intAdicAbv hb) (p.coeff n)) (by simp [h1]) h2
  · intro h
    rw [Finset.sup'_lt_iff]
    intro n hn
    rw [mem_support_iff] at hn
    exact h _ <| p.coeff_mem_coeffs hn

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ mapDomainOfBialgHom (mapDomainBialgHom R f) = f

Tactic:
ext g; refine single_left_injective (R := R) one_ne_zero ?_; simp [single_mapDomainOfBialgHom]

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
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝¹ : HeightOneSpectrum R
x✝ : x✝¹ ∉ S
⊢ (x✝¹.valuationOfNeZeroMod n) 1 = 1

Tactic:
rw [map_one]

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

Goal state before:
pp: case empty
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n (∅.sum x) = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dpow (Multiset.count i ↑k) (x i)

Tactic:
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
    by_cases hn : n = 0
    · rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]
    · rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩

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

Goal state before:
pp: case insert.h
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

Tactic:
apply prod_congr rfl

Goal state after:
case insert.h
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = dpow (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)
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
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p : MvPolynomial (ℕ × M) R
⊢ (lift' hf_zero hf_smul hf_mul hf_add) ↑p = (aeval f) p

Tactic:
simp [lift', aeval_eq_eval₂Hom]

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

Goal state before:
pp: 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 (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs) ∧
        ¬restrictScalars R ⊤ = restrictScalars R (Ideal.map (algebraMap R (R ⧸ Ideal.span {r})) (Ideal.ofList rs) • ⊤)

Tactic:
Ideal.smul_restrictScalars,

Goal state after:
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 (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs) ∧
        ¬restrictScalars R ⊤ = Ideal.ofList rs • restrictScalars R ⊤
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
⊢ hI.dpow n x = (↑n !)⁻¹ʳ • x ^ n

Tactic:
rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc]

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
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr
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), Module.rankAtStalk (S × U) p = n + 1
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
simp_rw [Module.rankAtStalk_prod , Module.rankAtStalk_self, Pi.add_apply, Pi.one_apply] at this

Goal state after:
case succ.inr
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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
n : ℕ
hn : Module.rankAtStalk S = ↑n
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
induction n generalizing R S with

Goal state after:
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 : hI.IsDPMorphism hJ f
⊢ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f

Tactic:
simp only [isDPMorphism_def] at hf

Goal state after:
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}, a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose h) - a ∈ RingHom.ker f

Tactic:
RingHom.mem_ker,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f (↑(Classical.choose h) - a) = 0
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:
by
  ext (_ | n)
  · simp
  · simp [pow_succ']

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

Goal state before:
pp: case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose d) = ↑(Ring.choose (-1 + -↑d) n)

Tactic:
rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
      show (d : ℤ) + 1 + n - 1 = d + n by lia, ← Nat.cast_add, Ring.choose_natCast]

Goal state after:
case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • ↑((d + n).choose n))
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.mul t).hsum = s.hsum * t.hsum

Tactic:
rw [← smul_eq_mul, mul_eq_smul]
  exact smul_hsum s t

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by_cases hx : x = 0; · simp [hx]
    by_cases hy : y = 0; · simp [hy]
    rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
let f' := derivative f

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ (map f I).minimalPrimes

Tactic:
IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ under R ⁻¹' I.minimalPrimes