mathlib-initiative/mathlib-tactics huggingface dataset:
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 : G → ↑X.X₂
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ x ∈ cocycles₂ X.X₁

Tactic:
apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
  have := congr($((mapShortComplexH2 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH2, LinearMap.compLeft]

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

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) g) a) = (algebraMap B L) η * ↑g ((algebraMap B L) a)

Tactic:
congr 1

Goal state after:
case refine_2.e_a
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) (((galRestrict A K L B) g) a) = ↑g ((algebraMap B L) a)
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
⊢ H1π A ≫ map f φ 1 = mapCocycles₁ f φ ≫ H1π B

Tactic:
by
  simp [H1π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₁_hom_assoc]

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✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ HomologicalComplex.cyclesMap
        (cochainsMap ((MonoidHom.id (G ⧸ S)).comp (QuotientGroup.mk' S))
          (resMap (QuotientGroup.mk' S) ((quotientToInvariantsFunctor k S).map φ) ≫
            ofHom (Y.ρ.quotientToInvariants_lift S)))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of Y.ρ)) n =
    HomologicalComplex.cyclesMap
        (cochainsMap ((QuotientGroup.mk' S).comp (MonoidHom.id G))
          (resMap (MonoidHom.id G) (ofHom (X.ρ.quotientToInvariants_lift S)) ≫ φ))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains Y) n

Tactic:
congr 1

Goal state after:
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 (iCycles A 1))
      (cyclesMk 1 0 cyclesMk₁_eq._proof_1 ((ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) ⋯) =
    (ConcreteCategory.hom (iCycles A 1)) ((ConcreteCategory.hom (isoCycles₁ A).inv) x)

Tactic:
rw [iCycles_mk]
    simp only [ChainComplex.of_X, isoCycles₁_inv_comp_iCycles_apply]
    rfl

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

Goal state before:
pp: case one
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod 1

Tactic:
| one =>

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
⊢ ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
refine ⟨L, fun i ↦ ?_⟩

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ f i - L ∈ I ^ i
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff n) (optionFunLeft σ R p)) = (coeff (optionElim n x)) p

Tactic:
optionFunLeft,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff n) (PowerSeries.mk fun n x ↦ (coeff (optionElim n x)) p)) = (coeff (optionElim n x)) p
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ ∃ a b, (a none = m ∧ b none = n) ∧ a.some = u ∧ a + b = optionElim k x ∧ b.some = v

Tactic:
use u.optionElim m, v.optionElim n

Goal state after:
case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ ((optionElim m u) none = m ∧ (optionElim n v) none = n) ∧
    (optionElim m u).some = u ∧ optionElim m u + optionElim n v = optionElim k x ∧ (optionElim n v).some = v
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ ((optionElim m u) none = m ∧ (optionElim n v) none = n) ∧
    (optionElim m u).some = u ∧ optionElim m u + optionElim n v = optionElim k x ∧ (optionElim n v).some = v

Tactic:
suffices optionElim m u + optionElim n v = optionElim k x by simp_all

Goal state after:
case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ optionElim m u + optionElim n v = optionElim k x
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
⊢ (finSuccEquiv R n) (C r) = PowerSeries.C (C r)

Tactic:
ext k x
  simp_rw [coeff_coeff_finSuccEquiv, PowerSeries.coeff_C, coeff_C, ← cons_zero_zero,
    cons_injective2.eq_iff]
  split_ifs with h1 h2 h3
  · simp [h1.right]
  · tauto
  · rw [coeff_C, if_neg (by tauto)]
  · rw [coeff_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑((ofPowSMul I M n) x) (i + n) = 0
⊢ i + n = ?m.71 + n

Tactic:
by rw [add_comm]

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

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ (MvPowerSeries.coeff d) (subst (MvPowerSeries.X i) f) = 0

Tactic:
coeff_subst (HasSubst.X _),

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∑ᶠ (d_1 : ℕ), (coeff d_1) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ d_1) = 0
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
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ IsAdicComplete (Ideal.span (Set.range X)) (MvPowerSeries σ R)

Tactic:
have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    (MvPolynomial.idealOfVars σ R).map (algebraMap ..) := by
    simp_rw [Ideal.map_span, ← Set.range_comp]
    congr 2; ext1
    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete (Ideal.span (Set.range X)) (MvPowerSeries σ R)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ span (↑(map f p).coeffs ∪ {0}) = span (⇑f '' ↑p.coeffs ∪ {0})

Tactic:
congr 1

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ ↑(map f p).coeffs ∪ {0} = ⇑f '' ↑p.coeffs ∪ {0}
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Bialgebra R A
inst✝⁴ : Bialgebra R B
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid O
inst✝ : Subsingleton M
r : R[M]
⊢ ((Algebra.ofId R R[M]).comp (counitAlgHom R R[M])) r = (AlgHom.id R R[M]) r

Tactic:
congr 1

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Bialgebra R A
inst✝⁴ : Bialgebra R B
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid O
inst✝ : Subsingleton M
r : R[M]
⊢ (Algebra.ofId R R[M]).comp (counitAlgHom R R[M]) = AlgHom.id R R[M]
Module: Mathlib.RingTheory.Regular.Category

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ (r • ⊤).mkQ x = 0 ↔ x ∈ Set.range ⇑((lsmul R M) r)

Tactic:
simp [Submodule.mem_smul_pointwise_iff_exists, Submodule.mem_smul_pointwise_iff_exists]

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✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ HomologicalComplex.cyclesMap
        (chainsMap ((QuotientGroup.mk' S).comp (MonoidHom.id G)) (φ ≫ resMap (MonoidHom.id G) (Y.toCoinvariantsMkQ S)))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains ((quotientToCoinvariantsFunctor k S).obj Y)) n =
    HomologicalComplex.cyclesMap
        (chainsMap ((MonoidHom.id (G ⧸ S)).comp (QuotientGroup.mk' S))
          (X.toCoinvariantsMkQ S ≫ resMap (QuotientGroup.mk' S) ((quotientToCoinvariantsFunctor k S).map φ)))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains ((quotientToCoinvariantsFunctor k S).obj Y)) n

Tactic:
congr 1

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
a : A
hn : n ≠ 0
x✝ : a ∈ ⊥
⊢ (if a = 0 ∧ n = 0 then 1 else 0) ∈ ⊥

Tactic:
simp only [mem_bot, ite_eq_right_iff, and_imp]
    exact fun _ a ↦ False.elim (hn a)

Goal state after:
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 0 + 0 = 0 ∧ n✝ = 0 then 1 else 0) =
    ∑ k ∈ antidiagonal n✝, (if 0 = 0 ∧ k.1 = 0 then 1 else 0) * if 0 = 0 ∧ k.2 = 0 then 1 else 0

Tactic:
add_zero

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
⊢ (if 0 = 0 ∧ n✝ = 0 then 1 else 0) =
    ∑ k ∈ antidiagonal n✝, (if 0 = 0 ∧ k.1 = 0 then 1 else 0) * if 0 = 0 ∧ k.2 = 0 then 1 else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0

Tactic:
rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n + 1)! * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
rw [factorial_succ, mul_comm (n + 1)]

Goal state after:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1)) * hI.dpow (n + 1) a = a ^ (n + 1)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * dp R (∑ x ∈ insert a✝ s✝, n x) m =
    ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m

Tactic:
congr 1

Goal state after:
case insert.e_a
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(multinomial (insert a✝ s✝) n)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case add
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) = ⊤
x y : DividedPowerAlgebra R M
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hy : y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x + y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case succ
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
a✝ : f (hI.dpow n 0) = hJ.dpow n 0
⊢ f (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0

Tactic:
hI.dpow_eval_zero n.succ_ne_zero,

Goal state after:
case succ
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
a✝ : f (hI.dpow n 0) = hJ.dpow n 0
⊢ f 0 = hJ.dpow (n + 1) 0
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₂
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
| IsWeaklyRegular M as ∧ Ideal.ofList as • ⊤ ≠ ⊤

Tactic:
← Quotient.nontrivial_iff

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₂
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
| IsWeaklyRegular M as ∧ Nontrivial (M ⧸ Ideal.ofList as • ⊤)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
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
| IsWeaklyRegular M₂ bs ∧ Ideal.ofList bs • ⊤ ≠ ⊤

Tactic:
← Quotient.nontrivial_iff

Goal state after:
case b
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
| IsWeaklyRegular M₂ bs ∧ Nontrivial (M₂ ⧸ Ideal.ofList bs • ⊤)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧
      IsWeaklyRegular (QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤) rs₂ ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
← e.isWeaklyRegular_congr rs₂

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂ ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂
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
n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ hI.dpow n✝ (e.symm x✝) ∈ I

Tactic:
apply hI.dpow_mem 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
n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I
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:
← cast_zero,

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 neg
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:
simp [hJ, iInf_neg, le_top, inf_of_le_left, Set.Iic.coe_top]

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ ⊤.carrier = I
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
lift b to K[ε]ˣ using hb

Goal state after:
case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ ∃ c, a * c = ↑b ∨ ↑b * c = a
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
x✝ : R
this : (RingHom.ker f).IsPrime
⊢ (Ideal.Quotient.mk (RingHom.ker f)) x✝ = (AlgEquiv.ofBijective (ofId k (R ⧸ RingHom.ker f)) ⋯) (f x✝)

Tactic:
AlgEquiv.coe_ofBijective,

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
x✝ : R
this : (RingHom.ker f).IsPrime
⊢ (Ideal.Quotient.mk (RingHom.ker f)) x✝ = (ofId k (R ⧸ RingHom.ker f)) (f x✝)
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 : hI.DPMorphism hJ
x✝ : ℕ
hn : x✝ ≠ 0
a : A
ha : f.toRingHom a = 0
ha' : a ∈ I
⊢ f.toRingHom (hI.dpow x✝ a) = 0 ∧ hI.dpow x✝ a ∈ I

Tactic:
rw [← f.isDPMorphism.2 a ha', ha]

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 : hI.DPMorphism hJ
x✝ : ℕ
hn : x✝ ≠ 0
a : A
ha : f.toRingHom a = 0
ha' : a ∈ I
⊢ hJ.dpow x✝ 0 = 0 ∧ hI.dpow x✝ a ∈ I
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case one
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x : A
i : ι
⊢ ↑(((decompose 𝒜) 1) i) ∈ Subsemiring.closure s

Tactic:
| one =>

Goal state after: