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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) 2 (⇑κ ∘ₘ ν)
⊢ ⇑κ ∘ₘ ν = Measure.map Prod.fst (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∑ k ∈ range K, ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ

Tactic:
gcongr with k
      have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
      rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]
      refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · calc
          2 / (↑k + 1) * x ^ 2 = x / (k + 1) * (2 * x) := by ring
          _ ≤ 1 * (2 * x) := by
              have : 0 < x := k.cast_nonneg.trans_lt hx.1
              gcongr
              exact (div_le_one <| by positivity).2 <| mod_cast hx.2
          _ = 2 * x := by rw [one_mul]

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ cgf X μ t ≤ (↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2

Tactic:
h2

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2 ≤ (↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ i ∈ range N, Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2 ≤ ε⁻¹ ^ 2 * C

Tactic:
simp_rw [div_eq_inv_mul, ← inv_pow, mul_inv, mul_comm _ (ε⁻¹), mul_pow, mul_assoc,
          ← mul_sum]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ε⁻¹ ^ 2 * ∑ i ∈ range N, (↑(u i))⁻¹ ^ 2 * Var[S (u i); ℙ] ≤ ε⁻¹ ^ 2 * C
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
r : k
x : ↑V
⊢ (RestrictScalars.addEquiv k k[G] V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm (r • x)) =
    (RingHom.id k) r • unitIsoAddEquiv.toFun x

Tactic:
simp only [Representation.asModuleEquiv_symm_map_smul]
      rfl

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

Goal state before:
pp: case succ
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 : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0

Tactic:
Preadditive.sub_comp,

Goal state after:
case succ
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 : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1)) -
        (coind₁Functor k G).map (X.d n) ≫ (coind₁Functor k G).map (X.d (n + 1))) =
    0
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
y : V
⊢ (ρ g - LinearMap.id) y ∈ Coinvariants.ker ρ

Tactic:
simpa using Coinvariants.sub_mem_ker g y

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
⊢ (indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom = X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f

Tactic:
simp only [indFunctor_obj, coindFunctor_obj]

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
⊢ (indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom = X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x✝¹ : ↑A
x✝ : ↑(res φ B)
⊢ (((A.coinvariantsTensorMk (res φ B)).compr₂
          (ModuleCat.Hom.hom (coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B)))
        x✝¹)
      x✝ =
    (((A.coinvariantsTensorMk (res φ B)).compr₂
          (ModuleCat.Hom.hom (𝟙 (((coinvariantsTensor k G).obj A).obj (res φ B)))))
        x✝¹)
      x✝

Tactic:
simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: 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})
k : Fin w✝¹
⊢ f k ∈ span {a} ⊔ I

Tactic:
rw [sup_comm, ← hf]

Goal state after:
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})
k : Fin w✝¹
⊢ f k ∈ span (Set.range f)
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
n : τ →₀ ℕ
d : σ →₀ ℕ
hd : (coeff d) p * (coeff n) ((monomial (mapDomain f d)) 1) ≠ 0
⊢ mapDomain f d = n

Tactic:
exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
a : R
ha : a ∈ i
this : ∀ (m : ℕ), ∃ n₀, ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ i ^ m
⊢ IsTopologicallyNilpotent a

Tactic:
simpa [IsTopologicallyNilpotent, i.hasBasis_nhds_zero_adic.tendsto_right_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (embDomain (_root_.finSuccEquiv n).toEmbedding (Finsupp.cons k x)))
      ((rename ⇑(_root_.finSuccEquiv n).toEmbedding) p) =
    (coeff (Finsupp.cons k x)) p

Tactic:
coeff_embDomain_rename

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
have fg : (maximalIdeal R).FG := fg_of_isNoetherianRing (maximalIdeal R)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ cyclesMap (MonoidHom.id G) (𝟙 A) n = 𝟙 (cycles A n)

Tactic:
by
  simp [cyclesMap]

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

Goal state before:
pp: case cons
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 = 0

Tactic:
have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]

Goal state after:
case cons
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
key : ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y
⊢ d = 0
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ C (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p

Tactic:
by
  rw [C_dvd_iff_dvd_coeff]
  exact fun i ↦ h_prin.contentIdeal_generator_dvd_coeff i

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

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

Tactic:
apply _root_.map_dvd C

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
a✝ : span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r}
⊢ r ∣ Submodule.IsPrincipal.generator p.contentIdeal
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
⊢ 1 ≤ (v.intAdicAbv hb) (p.coeff x✝) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)

Tactic:
h2

Goal state after:
case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
h2 : 1 ≤ (v.intAdicAbv hb) (p.coeff x✝)
⊢ 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)
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:
by
          rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
intro hx

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range
Module: Mathlib.RingTheory.DividedPowers.Basic

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

Tactic:
rw [dpow_zero I.zero_mem]

Goal state after:
case pos
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ 1 = ↑(#(∅.sym 0))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = ↑(n ! * (n + 1).choose n) * dp R (n + 1) x

Tactic:
simp [mul_comm _ (n + 1), Nat.factorial_succ]

Goal state after:
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (Ideal.ofList (r :: l₁✝) • ⊤).toAddSubgroup

Tactic:
Ideal.ofList_cons,

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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f ((Ideal.span {r} ⊔ Ideal.ofList l₁✝) • ⊤).toAddSubgroup
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| (Ideal.ofList (s :: l₂✝) • ⊤).toAddSubgroup

Tactic:
Ideal.ofList_cons,

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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| ((Ideal.span {s} ⊔ Ideal.ofList l₂✝) • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case a
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
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J

Tactic:
exact hf.1 (mem_map_of_mem f ha)

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
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
m : M
⊢ (map S f) ((embed R M) m) = (embed S N) (f m)

Tactic:
by
  simp [embed_def, map_apply_dp]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ Ideal.ofList (r :: rs) • ⊤ < ⊤
⊢ r :: rs = []

Tactic:
Ideal.ofList_cons,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ (Ideal.span {r} ⊔ Ideal.ofList rs) • ⊤ < ⊤
⊢ r :: rs = []
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case nil
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsWeaklyRegular (N ⊗[R] M₂) []

Tactic:
exact nil R (N ⊗[R] M₂)

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
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
have hm : m < n := lt_of_le_of_lt le_self_add hkm

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J

pp: case refine_2
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.IsSubDPIdeal (J ⊓ I)

Tactic:
· have hab' : a - b ∈ I := I.sub_mem ha hb
    rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_add_one, sum_insert notMem_range_self,
      tsub_self, hI.dpow_zero hab', mul_one, add_sub_cancel_left]
    exact J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
      (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.IsSubDPIdeal (J ⊓ I)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ε ∣ x

Tactic:
intro hx

Goal state after:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : x ∈ I
⊢ ε ∣ x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ ε ∣ x → x ∈ I

Tactic:
intro hx

Goal state after:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
hx : ε ∣ x
⊢ x ∈ I
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ dpow hI f n✝ (x✝ + y✝) = ∑ k ∈ Finset.antidiagonal n✝, dpow hI f k.1 x✝ * dpow hI f k.2 y✝

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)
    rw [← map_add, dpow_apply' hI hIf (I.add_mem ha hb), hI.dpow_add ha hb, map_sum,
      Finset.sum_congr rfl]
    exact fun k _ ↦ by rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]

Goal state after: