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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
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) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ =
    ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω) +
          ((↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ) +
        (∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ)‖

Tactic:
congr
      simp only [sum_sub_distrib, smul_sub]
      abel

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
⊢ X.d n ≫ X.d (n + 1) = 0

Tactic:
induction n with

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

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ QuasiIsoAt (resolution.π k g) (m + 1)

Tactic:
quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ HomologicalComplex.ExactAt ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 1)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : 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
⊢ (MvPolynomial.monomial (m.degree p)) 1 = MvPolynomial.C 1 * (MvPolynomial.monomial (m.degree p)) 1

Tactic:
MvPolynomial.C_1,

Goal state after:
σ : 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
⊢ (MvPolynomial.monomial (m.degree p)) 1 = 1 * (MvPolynomial.monomial (m.degree p)) 1
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
e✝ e : σ ↪ τ
⊢ ∀ (r : R), killComplFun e ((algebraMap R (MvPowerSeries τ R)) r) = (algebraMap R (MvPowerSeries σ R)) r

Tactic:
simpa using! killComplFun_monomial_embDomain 0

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 : G →₀ ↑A
⊢ (x.sum fun g a ↦ (A.ρ g⁻¹) a - a) = 0 ↔ (x.sum fun g a ↦ (A.ρ g⁻¹) a) = x.sum fun x a ↦ a

Tactic:
rw [sum_sub, sub_eq_zero]

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

Goal state before:
pp: case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₃₂ A)) (single (g, 1, h) ((A.ρ g) (-a))) = single (g, 1) ((A.ρ g) a) - single (1, h) a

Tactic:
simp [d₃₂_single (G := G)]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
⊢ (rename f) p = subst (X ∘ f) p

Tactic:
ext n

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ (coeff n) ((rename f) p) = (coeff n) (subst (X ∘ f) p)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n✝ : ℕ
F : Fin n✝ → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
n : ℕ
⊢ g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n

Tactic:
induction n with

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
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
⊢ g = ∑ i, H i * F i

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n✝ : ℕ
F : Fin n✝ → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n : ℕ), g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
n : ℕ
⊢ (coeff n) g = (coeff n) (∑ i, H i * F i)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g✝ : Fin 1 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (inhomogeneousChains A).d 1 0)) x✝) default =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ 0)) x✝) default

Tactic:
simp [inhomogeneousChains.d_single (G := G), ChainComplex.of.d,
       Unique.eq_default (α := Fin 0 → G)]

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
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1ToTensorOfIsTrivial A)
      ((ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
simp only [H1ToTensorOfIsTrivial, H1π, AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_comp]
  -- todo: change this proof so that we don't need `change` that abuses defeq.
  change QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _) = _
  simp [π_comp_H1Iso_hom_apply, ← Submodule.Quotient.quotientAddGroupMk_eq_mk, Submodule.mkQ,
    AddSubgroup.subtype, cycles₁IsoOfIsTrivial]

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

Goal state before:
pp: S : Type u_3
inst✝¹ : CommRing S
inst✝ : IsNoetherianRing S
n : ℕ
⊢ IsNoetherianRing (MvPowerSeries (Fin n) S)

Tactic:
induction n with

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R)

Tactic:
maximalIdeal_eq_map_of_fg fg,

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈
    Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p = (toAdicCompletion σ R) ↑p

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
n : ℕ
⊢ ↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p) n = ↑((toAdicCompletion σ R) ↑p) n
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case w
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
this : v + (ConcreteCategory.hom (d₂₁ A)) ve ∈ cycles₁ A
⊢ comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯ ∈ cycles₁ (res S.subtype A)

Tactic:
rw [mem_cycles₁_iff] at this ⊢

Goal state after:
case w
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
this :
  ((v + (ConcreteCategory.hom (d₂₁ A)) ve).sum fun g a ↦ (A.ρ g⁻¹) a) =
    (v + (ConcreteCategory.hom (d₂₁ A)) ve).sum fun x a ↦ a
⊢ ((comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯).sum fun g a ↦ ((res S.subtype A).ρ g⁻¹) a) =
    (comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯).sum fun x a ↦ a
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (∀ x ∈ ↑p.coeffs, x = 0) ↔ p = 0

Tactic:
refine ⟨?_, fun h ↦ by simp [h]⟩

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (∀ x ∈ ↑p.coeffs, x = 0) → p = 0
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} → C r ∣ p

pp: case mpr
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → p.contentIdeal ≤ span {r}

Tactic:
· rw [← p.contentIdeal.span_singleton_generator]
    intro _
    calc
    C r ∣ C h_prin.generator := by
      apply _root_.map_dvd C
      rwa [← span_singleton_le_span_singleton]
     _ ∣ p := h_prin.contentIdeal_generator_dvd

Goal state after:
case mpr
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → p.contentIdeal ≤ span {r}
Module: Mathlib.RingTheory.DedekindDomain.SInteger

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : (↥(S.integer K))ˣ
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (HeightOneSpectrum.valuation K v) ↑(Units.mk0 ↑↑x ⋯) * (HeightOneSpectrum.valuation K v) ↑x.inv = 1

Tactic:
rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M), r • N.mkQ x = 0 → N.mkQ x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N

Tactic:
simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
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
⊢ (PowerSeries.mk fun n ↦ dp n (a + b)) = (PowerSeries.mk fun n ↦ dp n a) * PowerSeries.mk fun n ↦ dp n b

Tactic:
ext n

Goal state after:
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)
Module: Mathlib.RingTheory.DividedPowers.Basic

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

Tactic:
induction n with

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
⊢ hI.dpow n a = hJ.dpow n a

Tactic:
induction ha using Submodule.smul_induction_on' generalizing n with
  | smul a ha b hb =>
    rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
    ring
  | add x hx y hy hx' hy' =>
    rw [hI.dpow_add (mul_le_left hx) (mul_le_left hy),
      hJ.dpow_add (mul_le_right hx) (mul_le_right hy)]
    apply sum_congr rfl
    intro k _
    rw [hx', hy']

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : M
⊢ ↑n ! * dp R n x = dp R 1 x ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
eq : I = ⊤
⊢ False

Tactic:
simp [eq] at smul_lt

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

Goal state before:
pp: case dp.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
i : ι
⊢ x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
induction hx using span_induction with
      | zero => simp
      | mem x hx =>
        obtain ⟨n, rfl⟩ := hx
        simp only
        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i)), mul_comm,
          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
        simp only
        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
        simp
      | add x y hxmem hymem hx hy =>
        rw [add_mul]
        exact Submodule.add_mem _ hx hy
      | smul r x hxmem hx =>
        rw [smul_mul_assoc]
        exact smul_mem _ _ hx

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

Goal state before:
pp: 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 : ℕ
⊢ f (hI.dpow n 0) = hJ.dpow n 0

Tactic:
induction n with

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

Goal state before:
pp: 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
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : S ⊆ ↑(hI.ideal_from_ringHom hJ hf)
⊢ hJ.dpow n (f x) = f (hI.dpow n x)

Tactic:
rw [← span_le, ← hS] at hS'

Goal state after:
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
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : I ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n (f x) = f (hI.dpow n x)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
x✝ : A
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow 0 x✝ else 0) = 1

Tactic:
by simp [if_pos hx, hI.dpow_zero (hJ.isSubideal hx)]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hinj : Injective ⇑Coe.ringHom
⊢ Coe.ringHom ⟨dpow' p n ↑x, ⋯⟩ = (↑n !)⁻¹ʳ * Coe.ringHom x ^ n

Tactic:
simp [dpow', inverse_eq_inv', Coe.ringHom_apply]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
⊢ fst r ≠ 0

Tactic:
contrapose hx0

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
this : ε * r = fst r • ε
hx0 : fst r = 0
⊢ fst r • ε = 0
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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
have : Nontrivial S := by
      apply Module.nontrivial_of_rankAtStalk_pos (R := R)
      simp [hn]

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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (Cotangent.map P.toExtendScalars ∘ₗ h1Cotangentι) ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)

Tactic:
Cotangent.map_comp_h1Cotangentι,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑S h1Cotangentι ∘ₗ H1Cotangent.map P.toExtendScalars) ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
⊢ mk 1 ^ (d + 1 + 1) = mk fun n ↦ ↑((d + 1 + n).choose (d + 1))

Tactic:
ext n

Goal state after:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)
n : ℕ
⊢ (coeff n) (mk 1 ^ (d + 1 + 1)) = (coeff n) (mk fun n ↦ ↑((d + 1 + n).choose (d + 1)))