mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this✝ : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun i ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : ∫ (x : Ω), X 0 x ∂μ = ∫ (x : Ω), Y 0 x ∂μ
n : ℕ
⊢ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω = (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω

Tactic:
congr with i

Goal state after:
case e_a.e_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this✝ : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun i ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : ∫ (x : Ω), X 0 x ∂μ = ∫ (x : Ω), Y 0 x ∂μ
n i : ℕ
⊢ Y i ω = X i ω
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Injective V

Tactic:
rw [← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff,
    ← Module.injective_iff_injective_object]
  exact Module.injective_of_isSemisimpleRing _ _

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).range = (Hom.hom (leftRegular k G).norm).ker

Tactic:
by
  simp [norm, ker_leftRegular_norm_eq, range_applyAsHom_sub_eq_ker_linearCombination k g hg]

Goal state after:
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
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
⊢ (fun f ↦
        ofHom
          {
            toLinearMap :=
              Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                (TensorProduct.lift
                  (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)))
                ⋯,
            isIntertwining' := ⋯ })
      ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ }) f) =
    f

Tactic:
ext h a
    simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm

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

Goal state before:
pp: 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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : (algebraMap K L) ((Algebra.norm K) ↑xu) = (algebraMap K L) 1
⊢ ∃ y, g ↑y / ↑y = x

Tactic:
rw [← norm_ofAlgebraAutOnUnits_eq xu, map_one] at hx'

Goal state after:
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
⊢ ∃ y, g ↑y / ↑y = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this✝ :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
y : ↑(ofAlgebraAutOnUnits K L)
hy :
  (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g -
            CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
      y =
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩
this : ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y - y)) = x
⊢ g ↑(toMul (toAdditive y)) / ↑(toMul (toAdditive y)) = ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y - y))

Tactic:
toMul_sub

Goal state after:
case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this✝ :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
y : ↑(ofAlgebraAutOnUnits K L)
hy :
  (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g -
            CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
      y =
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩
this : ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y - y)) = x
⊢ g ↑(toMul (toAdditive y)) / ↑(toMul (toAdditive y)) = ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y) / toMul y)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
key : (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0
⊢ (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv =
    0 ≫ (diagonalSuccIsoFree k G m).inv

Tactic:
simpa using key

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
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = ((RingHom.id k) r • fun g ↦ (A.ρ g) x - x) g

Tactic:
by dsimp; rw [map_smul, smul_sub]

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
x : Fin 0 → G
a : ↑A
y : G
⊢ (A.ρ y) (Pi.single x a default) - Pi.single x a default =
    (A.ρ y) (Pi.single x a fun i ↦ y) - Pi.single x a (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) (uniqueElim y))

Tactic:
rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
    (Fin.contractNth 0 _) default, Pi.default_def]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this : α (α_inv 1) = 1
⊢ α 1 = 1

Tactic:
have h := this

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this h : α (α_inv 1) = 1
⊢ α 1 = 1
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ (∀ (y : Fin w✝¹), p y ∈ ↑I) ∧ ∀ (y : Fin w✝), a * i y ∈ ↑I

Tactic:
exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩

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
g h : G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g⁻¹, g * h) ((A.ρ g⁻¹) a) + single (g, h) a) =
    single g⁻¹ ((A.ρ g⁻¹) a) + single g a

Tactic:
simp only [map_add, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel_left]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (g * h) a - single h ((A.ρ g⁻¹) a) + single g⁻¹ ((A.ρ g⁻¹) a) +
      (single h ((A.ρ g⁻¹) a) - single (g * h) a + single g a) =
    single g⁻¹ ((A.ρ g⁻¹) a) + single g a
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
⊢ killComplFun e ((monomial x) r) = 0

Tactic:
classical
  ext; simp [coeff_killComplFun, coeff_monomial]
  grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
hr : r ∈ S
⊢ r ∈ ⇑constantCoeff '' ↑I

Tactic:
simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr

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

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

Tactic:
apply ((IsLocalRing.local_hom_TFAE _).out 0 2).mpr

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
⊢ Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R) ≤
    maximalIdeal (AdicCompletion (maximalIdeal R) R)
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n ≡ f m [SMOD maximalIdeal A ^ n • ⊤]
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
rw [hn, zero_smul, Ideal.zero_eq_bot, SModEq.bot] at hf

Goal state after:
case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n = f m
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ comul (f a) = f a ⊗ₜ[R] f a

Tactic:
rw [← CoalgHomClass.map_comp_comul_apply, ha.comul_eq_tmul_self]; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ (d • a) ⊗ₜ[R] (d • a) = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y

Tactic:
simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
n : ℕ
left✝ : n ∈ p.support
h2 : a✝ = p.coeff n
⊢ p.content ∣ p.coeff n

Tactic:
exact content_dvd_coeff n

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case refine_1
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
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
⊢ ↑T ⊆ ↑(⊥.colon {↑(∏ a, g a) • m}).radical

Tactic:
intro a ha

Goal state after:
case refine_1
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
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
⊢ a ∈ ↑(⊥.colon {↑(∏ a, g a) • m}).radical
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
n : ℕ
⊢ (PowerSeries.coeff n) (PowerSeries.mk fun n ↦ dp n (a + b)) =
    (PowerSeries.coeff n) ((PowerSeries.mk fun n ↦ dp n a) * PowerSeries.mk fun n ↦ dp n b)

Tactic:
simp only [PowerSeries.coeff_mk, PowerSeries.coeff_mul, dp_add n,
    sum_antidiagonal_eq_sum_range_succ_mk]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ n • ↑(n - 1)! * hI.dpow n a = 0

Tactic:
smul_mul_assoc

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ n • (↑(n - 1)! * hI.dpow n a) = 0
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 : ℕ
x y : M
⊢ ↑(X (n, x + y)) = ∑ k ∈ antidiagonal n, ↑(X (k.1, x) * X (k.2, y))

Tactic:
← RingCon.coe_finsetSum

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ↑(X (n, x + y)) = ↑(∑ i ∈ antidiagonal n, X (i.1, x) * X (i.2, y))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.smul
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 : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
smul_mul_assoc

Goal state after:
case dp.mem.smul
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 : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • (x * dp R k (v i)) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case hdp
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = hK.dpow n ((g.comp f) a)

Tactic:
hh.2 a ha,

Goal state after:
case hdp
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = (g.comp f) (hI.dpow n a)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
m : ℕ
b : A
hb : b ∈ S
⊢ (RingHom.id A) (hI.dpow m b) = hI'.dpow m ((RingHom.id A) b)

Tactic:
simpa only [RingHom.id_apply] using (hdp b hb)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
⊢ (if hx : a * x ∈ I then ⋯.choose else 0) = a ^ n * if hx : x ∈ I then ⋯.choose else 0

Tactic:
have hax : a * x ∈ I := Ideal.mul_mem_left _ _ hx

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
hax : a * x ∈ I
⊢ (if hx : a * x ∈ I then ⋯.choose else 0) = a ^ n * if hx : x ∈ I then ⋯.choose else 0
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
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) =
    ∑ k ∈ Finset.antidiagonal n✝, (if x✝ ∈ J then hI.dpow k.1 x✝ else 0) * if y✝ ∈ J then hI.dpow k.2 y✝ else 0

Tactic:
simp_rw [if_pos hx, if_pos hy, if_pos (Ideal.add_mem J hx hy),
    hI.dpow_add (hJ.isSubideal hx) (hJ.isSubideal hy)]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ a ∈ I → (↑n !)⁻¹ʳ * a ^ n = 0

Tactic:
intro ha

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ (↑n !)⁻¹ʳ * a ^ n = 0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : IsNilpotent ↑p
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ a ∈ I → (↑n !)⁻¹ʳ * a ^ n = 0

Tactic:
intro ha

Goal state after:
A : Type u_1
inst✝² : CommRing A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : IsNilpotent ↑p
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
⊢ (↑n !)⁻¹ʳ * a ^ n = 0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : ℕ
inst✝² : CharP A p
inst✝¹ : Fact (Nat.Prime p)
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ a ∈ I → (↑n !)⁻¹ʳ * a ^ n = 0

Tactic:
intro ha

Goal state after:
A : Type u_1
inst✝³ : CommRing A
p : ℕ
inst✝² : CharP A p
inst✝¹ : Fact (Nat.Prime p)
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
⊢ (↑n !)⁻¹ʳ * a ^ n = 0
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ⋯.choose = ⟨dpow' p n ↑x, ⋯⟩

Tactic:
have hinj : Injective (PadicInt.Coe.ringHom (p := p)) :=
      (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hinj : Injective ⇑Coe.ringHom
⊢ ⋯.choose = ⟨dpow' p n ↑x, ⋯⟩
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ hJ.IsSubDPIdeal (Ideal.map f K)

Tactic:
rw [Ideal.map, span_isSubDPIdeal_iff]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ ⇑f '' ↑K, hJ.dpow n s ∈ span (⇑f '' ↑K)

A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
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
p : PrimeSpectrum R
⊢ RingHom.ker ((↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal)) =
    p.asIdeal

Tactic:
← AlgHom.comap_ker,

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
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) (RingHom.ker ↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm) =
    p.asIdeal