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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: case mpr
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
⊢ S.ShortExact → (S.map (resFunctor φ)).ShortExact

Tactic:
rintro @⟨_, mono_f, epi_g⟩
    exact {
      exact := by rwa [ShortComplex.exact_map_iff_of_faithful]
      mono_f := by simpa [mono_iff_injective] using! mono_f
      epi_g := by simpa [epi_iff_surjective] using! epi_g
    }

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Monoid G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ρ : Representation k G V
inst✝² : ρ.IsIrreducible
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
⊢ Module.finrank k k = 1

Tactic:
exact CommSemiring.finrank_self k

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inl
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : IsEmpty (σ.Equiv ρ)
⊢ ↑(finrank k (σ.IntertwiningMap ρ)) = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
simpa [finrank_eq_zero_of_subsingleton]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V := (↑k f).leftInverse
hφ : ∀ (x : V), φ (f x) = x
x✝ : Fintype G
⊢ ∀ (x : V), (LinearMap.equivariantProjection G φ ∘ₗ f) x = LinearMap.id x

Tactic:
exact φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| hφ

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

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ (ρ g - LinearMap.id).range ≤ Coinvariants.ker ρ

Tactic:
rintro x ⟨y, rfl⟩

Goal state after:
case refine_2
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
y : V
⊢ (ρ g - LinearMap.id) y ∈ Coinvariants.ker ρ
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ + f g = f (g * g⁻¹)

Tactic:
hf g g⁻¹

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ + f g = g • f g⁻¹ + f g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ * f g = f (g * g⁻¹)

Tactic:
hf g g⁻¹

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ * f g = g • f g⁻¹ * f g
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
hf : Function.Injective ⇑f
inst✝ : Epi φ
i : ℕ
⊢ Epi ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.epi_iff_surjective] using!
    ((Rep.epi_iff_surjective φ).1 inferInstance).comp_left.comp <|
    LinearMap.funLeft_surjective_of_injective k A _ hf.comp_left

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 1 → G
⊢ ((ConcreteCategory.hom ((chainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y)) x✝ =
    ((ConcreteCategory.hom (chainsIso₁ X.X₃).inv) ↑z) x✝

Tactic:
by simp [chainsIso₁, ← hy]

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:
refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ∀ ⦃x : MvPolynomial σ R⦄,
    x ∈ restrictSupport R (⇑degree ⁻¹' Set.Ici 1) → x ∈ Submodule.restrictScalars R (idealOfVars σ R)

Tactic:
← SetLike.le_def,

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupport R (⇑degree ⁻¹' Set.Ici 1) ≤ Submodule.restrictScalars R (idealOfVars σ R)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ x → (coeff b) p = 0

Tactic:
simpa using fun _ h h' ↦ by simp [← embDomain_eq_mapDomain, embDomain_inj, h'] at h

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

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun g z ↦ g • z - z) = a
⊢ IsBoundary₀ G a

Tactic:
use x.sum (fun g a => single g (-(g • a)))

Goal state after:
case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun g z ↦ g • z - z) = a
⊢ ((x.sum fun g a ↦ single g (-(g • a))).sum fun g z ↦ g⁻¹ • z - z) = a
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 i j : ℕ
hij : j + 1 = i
⊢ ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousChains B).d i j =
    (inhomogeneousChains A).d i j ≫
      ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)

Tactic:
by
    subst hij
    ext
    simp [Fin.comp_contractNth, map_add, inhomogeneousChains.d, Rep.hom_comm_apply φ]
    rfl

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n ≫
      map (↑e.symm) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n =
    𝟙 (groupHomology A n)

Tactic:
rw [← groupHomology.map_comp, ← groupHomology.map_id]

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ } ≫
        (resFunctor ↑e).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id G) (𝟙 A) n
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e.symm) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n ≫
      map (↑e) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n =
    𝟙 (groupHomology B n)

Tactic:
rw [← groupHomology.map_comp, ← groupHomology.map_id]

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ } ≫
        (resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id H) (𝟙 B) n
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
s : Finset A
hs : ↑s ⊆ {a | IsGroupLikeElem R a}
⊢ LinearIndepOn R id ↑s

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ Coalgebra R (C ⧸ I)

Tactic:
constructor <;> ext : 1 <;>
    simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]

Goal state after:
case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map counit I.mkQ ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
· apply subset_span
    simpa using coeff_mem_coeffs h

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]
⊢ ↑p.coeffs ⊆ ↑(span {p.content})

Tactic:
intro _ h1

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ ↑(span {p.content})
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✝¹ x✝ : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun (x✝¹ * x✝)) = ↑(v.valuationOfNeZeroToFun x✝¹) * ↑(v.valuationOfNeZeroToFun x✝)

Tactic:
simp only [valuationOfNeZeroToFun_eq]

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✝¹ x✝ : Kˣ
⊢ (valuation K v) ↑(x✝¹ * x✝) = (valuation K v) ↑x✝¹ * (valuation K v) ↑x✝
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✝¹ x✝ : Kˣ
⊢ v.valuationOfNeZeroToFun (x✝¹ * x✝) = v.valuationOfNeZeroToFun x✝¹ * v.valuationOfNeZeroToFun x✝

Tactic:
rw [← WithZero.coe_inj, WithZero.coe_mul]
    simp only [valuationOfNeZeroToFun_eq]; exact map_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 : Rˣ
⊢ v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1

Tactic:
rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]
  constructor
  · exact v.valuation_le_one x
  · obtain ⟨x, _, hx, _⟩ := x
    change ¬v.valuation K (algebraMap R K x) < 1
    apply_fun v.intValuation at hx
    rw [map_one, map_mul] at hx
    rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap]
    gcongr
    exact v.intValuation_le_one _

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
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
⊢ p ∈ associatedPrimes R M

Tactic:
have ann_le : Module.annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q :=
    le_of_eq_of_le Submodule.annihilator_top.symm (IsAssociatedPrime.annihilator_le hq)

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
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
ann_le : annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q
⊢ p ∈ associatedPrimes R M
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
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
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)
⊢ P f

Tactic:
induction f using Quot.induction_on with | _ F
  dsimp
  induction F using MvPolynomial.induction_on with
  | C a => exact h_C a
  | add g1 g2 hg1 hg2 =>
    rw [RingCon.coe_add]
    exact h_add _ _ hg1 hg2
  | mul_X g nm h =>
    rw [RingCon.coe_mul]
    exact h_dp _ _ _ h

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

Goal state before:
pp: case inr
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n (0 • 0) = 0

Tactic:
dp_smul

Goal state after:
case inr
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
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
hJ : DividedPowers J
⊢ ofRingEquiv h (ofRingEquiv ⋯ hJ) = hJ

Tactic:
ext n b; simp [ofRingEquiv]

Goal state after:
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
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
⊢ (dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)

Tactic:
by
  simpa only [isDPMorphism_iff, Ideal.map_id, RingHom.id_apply]
    using ⟨hJ.1, fun _ _ _ ha ↦ by rw [dpow_eq_of_mem _ _ ha]⟩

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬p = 0

Tactic:
exact Nat.Prime.ne_zero hp.elim

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

Goal state before:
pp: case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h✝ : Nonempty ι
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ {j : A}, j ∈ I ⊓ ⨅ i, J i → hI.dpow n j ∈ I ⊓ ⨅ i, J i

Tactic:
intro n hn x hx

Goal state after:
case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h✝ : Nonempty ι
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ⊓ ⨅ i, J i
⊢ hI.dpow n x ∈ I ⊓ ⨅ i, J i
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hK : K ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ K.carrier

Tactic:
have : S ≤ K := by
      simp only [Set.mem_insert_iff, Set.mem_ofPred_eq] at hK
      rcases hK with rfl | hKS
      exacts [hS, hKS]

Goal state after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hK : K ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
this : S ⊆ ↑K
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ K.carrier
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
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ H.localize ((algebraMap S (Localization.AtPrime Q)) x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)

Tactic:
← H'.localize_algebraMap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ H.localize ((algebraMap S (Localization.AtPrime Q)) x) = H'.localize ((algebraMap S (Localization.AtPrime Q)) x)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
g : Γ
⊢ ∑ᶠ (i : ℕ), ((powerSeriesFamily x f) i).coeff g = ∑ᶠ (n : ℕ), ((powerSeriesFamily x f).coeff g) n

Tactic:
exact rfl

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : (s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
exact smul_eq_zero_of_left hs ((t a.2).coeff gh.2)

Goal state after:
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 β
g : Γ
⊢ (s.mul t).hsum.coeff g = ∑ gh ∈ antidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2

Tactic:
simp_rw [← smul_eq_mul, mul_eq_smul]
  exact coeff_smul s t g

Goal state after:
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:
by
  rw [← smul_eq_mul, mul_eq_smul]
  exact smul_hsum s t

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

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h : g ∈ (if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0).support
hb : b ∉ Set.range ⇑f
⊢ g ∈ ⋃ a, (s a).support

Tactic:
· simp [-Set.mem_range, dif_neg hb] at h

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)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
n : ℕ
this : IsLocalHom (Ideal.Quotient.mk I)
⊢ (Ideal.Quotient.mk I) (Polynomial.eval (c n) f') = (Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f))

Tactic:
exact SModEq.def.mp ((hc_mod n).eval _)

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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingUp R S → SpecializingMap (PrimeSpectrum.comap (algebraMap R S))

pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
· intro h P q hq
    simp only [flip] at hq
    rw [← PrimeSpectrum.le_iff_specializes] at hq
    obtain ⟨Q, hle, hQ, h⟩ := P.asIdeal.exists_ideal_ge_liesOver_of_le (q := q.asIdeal)
      (p := P.asIdeal.under R) hq
    refine ⟨⟨Q, hQ⟩, (PrimeSpectrum.le_iff_specializes P _).mp hle, ?_⟩
    ext : 1
    exact h.over.symm

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q