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

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

pp: case hbc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ ∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹ ≤ 2 / (↑k + 1)

Tactic:
· refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
        simp

Goal state after:
case hbc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ ∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹ ≤ 2 / (↑k + 1)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ HasSubgaussianMGF (fun x ↦ 0) 0 μ

Tactic:
simp [HasSubgaussianMGF_iff_kernel]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
⊢ HasSubgaussianMGF (fun ω ↦ X ω + -Y ω) (cX + cY) μ

Tactic:
exact hX.add_of_indepFun hY.neg hindep.neg_right

Goal state after:
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 : ℕ → Ω → ℝ := 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)
N : ℕ
⊢ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j; ℙ] =
    ∑ i ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 * ((↑i ^ 2)⁻¹ * Var[Y i; ℙ])

Tactic:
div_eq_mul_inv,

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)
N : ℕ
⊢ ∑ x ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 * (↑x ^ 2)⁻¹ * Var[Y x; ℙ] =
    ∑ i ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 * ((↑i ^ 2)⁻¹ * Var[Y i; ℙ])
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (Rep.{w} k G)).map f)

Goal state after:
k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
i : (forget (Rep k G)).obj X ≅ (forget (Rep k G)).obj Y := asIso ((forget (Rep k G)).map f)
⊢ IsIso f
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: case insert
k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
a : ι
s : Finset ι
ha : a ∉ s
h : ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)
⊢ ofHom (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, ofHom (f i)

Tactic:
simp [Finset.sum_insert ha, ofHom_add, h]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
⊢ ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)

Tactic:
by
  classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
⊢ map (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 (continuousCohomology n X)

Tactic:
by
  simp [map]

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
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
γ : G
⊢ ((Representation.leftRegular k G) g) x = x

Tactic:
by simpa [sub_hom, sub_eq_zero] using! hx

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)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
⊢ (coindResAdjunction k S).unit.app A =
    (indResAdjunction k S.subtype).unit.app A ≫ (resFunctor S.subtype).map A.indCoindIso.hom

Tactic:
by
  ext
  simp [coindResAdjunction]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
have key₁ := Representation.linearizeMap_single (k := k)
        (Action.diagonalSuccIsoTensorTrivial G m).inv (g, f) ((1 : k) * r)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
key₁ :
  (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) (MonoidAlgebra.single (g, f) (1 * r)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r)
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
key₁ :
  (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) (MonoidAlgebra.single (g, f) (1 * r)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r)
key₂ :
  (Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
      (MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r) =
    MonoidAlgebra.single (g, f) (1 * r)
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
exact ((congrArg (fun z => (Representation.linearizeMap
        (Action.diagonalSuccIsoTensorTrivial G m).inv) z) key₂).trans key₁).trans (by simp)

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)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
have : Module.IsTorsionFree A L := by
    rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
  have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization A K L B
  let η' : Lˣ := Units.mk0 (algebraMap B L η) (fun h ↦ by simp [h] at hη)
  obtain ⟨ε, hε⟩ := exists_div_of_norm_eq_one hg hη
  obtain ⟨a, b, h⟩ := IsLocalization.exists_mk'_eq (Algebra.algebraMapSubmonoid B A⁰) ε.1
  obtain ⟨t, ht, ht'⟩ := b.prop
  have : t • IsLocalization.mk' L a b = algebraMap _ _ a := by
    rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
  refine ⟨a, ?_, ?_⟩
  · rintro rfl
    simp only [IsLocalization.mk'_zero, _root_.map_zero, div_zero, ← h] at hε
    rw [← hε, Algebra.norm_zero] at hη
    exact zero_ne_one hη
  · replace hε := hε.symm
    rw [← h, eq_div_iff_mul_eq] at hε
    · replace hε := congr_arg (t • ·) hε
      rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← g.toAlgHom_apply,
        ← AlgHom.map_smul_of_tower, this] at hε
      apply IsIntegralClosure.algebraMap_injective B A L
      rw [map_mul, ← hε]
      congr 1
      exact algebraMap_galRestrictHom_apply A K L B g a
    · intro e
      rw [(map_eq_zero _).mp e, zero_div] at hε
      rw [hε, Algebra.norm_zero] at hη
      exact zero_ne_one hη

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

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
⊢ d₃₂ A ≫ d₂₁ A = 0

Tactic:
by
  simp [← cancel_mono (chainsIso₁ A).inv, ← eq_d₂₁_comp_inv, ← eq_d₃₂_comp_inv_assoc,
    ChainComplex.of.d, inhomogeneousChains.d_comp_d]

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
⊢ π A 0 ≫ (H0IsoOfIsTrivial A).hom = (cyclesIso₀ A).hom

Tactic:
by
  simp [H0IsoOfIsTrivial]

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
x✝¹ : ↥(cycles₁ A).toAddSubgroup
y : G →₀ ↑A
hy : y ∈ (cycles₁ A).toAddSubgroup
x✝ : ⟨y, hy⟩ ∈ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
z : ↑(shortComplexH1 A).X₁
hz : (shortComplexH1 A).moduleCatToCycles z = ⟨y, hy⟩
⊢ ((Finsupp.liftAddHom fun g ↦
            ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
        (cycles₁ A).toAddSubgroup.subtype)
      ⟨y, hy⟩ =
    0

Tactic:
simp [← hz, d₂₁, sum_sum_index, sum_add_index', tmul_add, sum_sub_index, tmul_sub,
        shortComplexH1]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∈ P
T : Finset R⟦X⟧
hT : ↑T = insert X (⇑C '' ↑S)
H : P = span ↑T
⊢ P.FG

Tactic:
exact ⟨T, hT ▸ H.symm⟩

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

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

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

Tactic:
· intro H
    refine UniformSpace.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
    have : ∀ i, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → u n - u m ∈ I ^ i := by
      simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu
    choose N hN using this
    obtain ⟨L, hL⟩ := H (fun i ↦ u ((Finset.Iic i).sup N))
      fun _ ↦ hN _ _ (Finset.le_sup (by simpa)) _ (Finset.le_sup (by simp))
    use L
    suffices ∀ i, ∃ N, ∀ n, N ≤ n → u n - L ∈ I ^ i by
      simpa [(hI.hasBasis_nhds L).tendsto_right_iff, sub_eq_neg_add]
    refine fun i ↦ ⟨(Finset.Iic i).sup N, fun n hn ↦ ?_⟩
    have := Ideal.add_mem _ (hN i ((Finset.Iic i).sup N) (Finset.le_sup (by simp))
      n (.trans (Finset.le_sup (by simp)) hn)) (hL i)
    rwa [sub_add_sub_cancel] at this

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
⊢ CompleteSpace R → ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ 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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ (ModuleCat.Hom.hom (H1π B) ∘ₗ ModuleCat.Hom.hom (mapCycles₁ 1 φ)) x = (ModuleCat.Hom.hom 0) x

Tactic:
refine (H1π_eq_zero_iff _).2 ?_

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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ ↑((ModuleCat.Hom.hom (mapCycles₁ 1 φ)) x) ∈ boundaries₁ B
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x✝ : AdicCompletion I (↥s →₀ M)
⊢ (map I ↑(finsuppLEquivDirectSum R M ↥s).symm) ((map I ↑(finsuppLEquivDirectSum R M ↥s)) x✝) = x✝

Tactic:
by
      simp [← LinearMap.comp_apply, map_comp]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ single g (x.coeff g) ∈ span R (Set.range fun x ↦ single x 1)

Tactic:
← mul_one (x.coeff g),

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ single g (x.coeff g * 1) ∈ span R (Set.range fun x ↦ single x 1)
Module: Mathlib.RingTheory.DividedPowers.Basic

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

Tactic:
| smul a ha b hb =>

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

Goal state before:
pp: case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
h_ext' : ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
obtain ⟨rs, len, mem, reg⟩ := ih (ModuleCat.of R (QuotSMulTop (x ^ k) M))
      (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top hk smul_lt.ne).lt_top h_ext'

Goal state after:
case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
h_ext' : ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
rs : List R
len : rs.length = n
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑(of R (QuotSMulTop (x ^ k) ↑M))) rs
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
rs : List R
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
h₄ : IsWeaklyRegular M₄ rs
⊢ Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)

Tactic:
induction h₄ generalizing M M₂ M₃ with
  | nil =>
    apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
    any_goals exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
    all_goals exact quot_hom_ext _ _ _ fun _ => rfl
  | cons r rs h₄ _ ih =>
    specialize ih
      (map_first_exact_on_four_term_exact_of_isSMulRegular_last h₁₂ h₂₃ h₄)
      (map_exact r h₂₃ h₃) (map_surjective r h₃)
    have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁
    have H₂ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₂
    exact (Exact.iff_of_ladder_linearEquiv H₁.symm H₂.symm).mp ih

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ DividedPowers (Ideal.span {↑p})

Tactic:
refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.map Coe.ringHom (Ideal.span {↑p}) = ⊤

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ) {x : ℤ_[p]},
    x ∈ Ideal.span {↑p} →
      ∃ y, ∃ (_ : n ≠ 0 → y ∈ Ideal.span {↑p}), Coe.ringHom y = (RatAlgebra.dividedPowers ⊤).dpow n (Coe.ringHom x)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ hI.dpow m (a • b) ∈ I • J

Tactic:
| smul a ha b hb =>

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R

Tactic:
intro x (h6 : x ∈ { r | r ∈ rs })
    refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)
    exact h4 ∘ Eq.trans (top_smul _).symm ∘ Eq.symm ∘ congrArg (· • ⊤)

Goal state after: