mathlib-initiative/mathlib-tactics huggingface dataset:
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 < ε
⊢ ∀ᵐ (ω : Ω),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        ε * ↑⌊c ^ n⌋₊

Tactic:
have c_pos : 0 < c := zero_lt_one.trans c_one

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
⊢ ∀ᵐ (ω : Ω),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        ε * ↑⌊c ^ n⌋₊
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g : G
⊢ f ((ρ g) x) = (σ g) (f x)

Tactic:
exact LinearMap.congr_fun (w g) x

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 (ρ.IntertwiningMap ρ) = 1

Tactic:
rw [LinearEquiv.finrank_eq (LinearEquiv.ofBijective (Algebra.linearMap k (IntertwiningMap ρ ρ))
      algebraMap_intertwiningMap_bijective_of_isAlgClosed).symm]

Goal state after:
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
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hindep
Ω : 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 := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on fun i ω ↦ ‖(X i - Y k i) ω‖)

Tactic:
unfold Function.onFun
      simp_rw [I]
      intro i j hij
      exact (hindep hij).comp (G_meas k) (G_meas k)

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
x✝¹ x✝ : H
⊢ (LinearMap.funLeft k B fun x ↦ x * (x✝¹ * x✝)).restrict ⋯ =
    (LinearMap.funLeft k B fun x ↦ x * x✝¹).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝).restrict ⋯

Tactic:
ext; simp [mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Semisimple

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule k[G] ρ.asModule

Tactic:
isSemisimpleModule_iff

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation ↔ ComplementedLattice (Submodule k[G] ρ.asModule)
Module: Mathlib.RepresentationTheory.Semisimple

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ IsSemisimpleModule k[G] M ↔ (ofModule M).IsSemisimpleRepresentation

Tactic:
isSemisimpleModule_iff

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ ComplementedLattice (Submodule k[G] M) ↔ (ofModule M).IsSemisimpleRepresentation
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
x✝¹ x✝ : G
⊢ { toFun := fun f ↦ (↑(π (x✝¹ * x✝))).comp (f.comp (ContinuousMap.mulLeft (x✝¹ * x✝)⁻¹)), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    { toFun := fun f ↦ (↑(π x✝¹)).comp (f.comp (ContinuousMap.mulLeft x✝¹⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ } *
      { toFun := fun f ↦ (↑(π x✝)).comp (f.comp (ContinuousMap.mulLeft x✝⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ }

Tactic:
ext; simp [mul_assoc]

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

Goal state before:
pp: case zero.left
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ ({
          X₁ :=
            ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
          X₂ :=
            ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
          X₃ :=
            ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
          f :=
            ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                ((chainComplexFunctor k g).obj (leftRegular k G))).f,
          g :=
            ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
                ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                  ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
          zero := ⋯ }.map
      (forget₂ (Rep k G) (ModuleCat k))).Exact

Tactic:
simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using!
          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
h : H
x✝ : G
⊢ LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹) ∘ₗ
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ =
    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ ∘ₗ
      LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹)

Tactic:
ext; simp [mul_assoc]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
f g : (Fin n → G) → ↑A
⊢ (fun g_1 ↦
      (A.ρ (g_1 0)) ((f + g) fun i ↦ g_1 i.succ) +
        ∑ j, (-1) ^ (↑j + 1) • (f + g) (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1)) =
    (fun g ↦ (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) +
      fun g_1 ↦
      (A.ρ (g_1 0)) (g fun i ↦ g_1 i.succ) + ∑ j, (-1) ^ (↑j + 1) • g (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1)

Tactic:
ext
      simp [Finset.sum_add_distrib, add_add_add_comm]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ d A n =
    (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom

Tactic:
by
  ext
  simp [d_hom_apply, map_add, barComplex.d_single (k := k), homEquiv]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ x ∈ cocycles₁ X.X₁

Tactic:
by
  apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
  have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH1, LinearMap.compLeft]

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

Goal state before:
pp: k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)

Tactic:
refine HomologicalComplex.Hom.isoOfComponents ?_ ?_

Goal state after:
case refine_1
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i

case refine_2
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Iso.hom (?refine_1 i) ≫ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d i j =
        (inhomogeneousChains A).d i j ≫ Iso.hom (?refine_1 j)
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ CompleteSpace R ↔ IsPrecomplete (Ideal.map e I) S

Tactic:
IsAdic.isPrecomplete_iff (by rfl)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ CompleteSpace R ↔ CompleteSpace S
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (n_1 : ℕ), IsOpen[inst✝¹] ↑((J ^ n) ^ n_1)

pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
· intro m
    rw [← pow_mul]
    apply h.left

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : CommRing R
inst✝ : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ (coeff x) (p * q) = MvPolynomial.coeff x ((truncTotal n) p * (truncTotal n) q)

Tactic:
coeff_truncTotal_mul_truncTotal_eq_coeff_mul _ _ hx

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : CommRing R
inst✝ : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ (coeff x) (p * q) = (coeff x) (p * q)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm :
  (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈
    Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R ^ 2)
⊢ m = 0

Tactic:
rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map,
      pow_smul_top_eq_ker_eval fg] at hm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
⊢ m = 0
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (Ideal.Quotient.mk (I ^ n)) ((liftRingHom I f ⋯) x) = (f n) x

Tactic:
simp only [liftRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm ((AdicCompletion.liftRingHom I f ⋯) x)) = (f n) x
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), (coeff x) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ x) = 0

Tactic:
simp only [MvPowerSeries.X_pow_eq, MvPowerSeries.coeff_monomial, smul_eq_mul, mul_ite, mul_one,
    mul_zero, ite_eq_right_iff]

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), d = single i x → (coeff x) f = 0
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
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : ι → R
i✝ : ι
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ (Ideal.Quotient.mk (I ^ n✝ • ⊤)) (f i✝) • Submodule.Quotient.mk (↑a✝ n✝) = f i✝ • Submodule.Quotient.mk (↑a✝ n✝)

Tactic:
rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]

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

Goal state before:
pp: case h
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
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
let v := x - (d₂₁ _).hom z

Goal state after:
case h
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
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Bialgebra R A
inst✝⁴ : Bialgebra R B
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid O
inst✝ : Subsingleton M
r : R[M]
⊢ (algebraMap R R[M]) ((counitBialgHom R R[M]).toFun r) = r

Tactic:
change (Algebra.ofId _ _).comp (Bialgebra.counitAlgHom R _) r = AlgHom.id R _ r
    congr 1
    ext g : 2
    simp [Subsingleton.elim g 1]

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
⊢ mapDomainBialgHom R (mapDomainOfBialgHom f) = f

Tactic:
ext x : 1

Goal state after:
case single_one_right
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
x : G
⊢ (mapDomainBialgHom R (mapDomainOfBialgHom f)) (single x 1) = f (single x 1)

case single_one_left
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
⊢ (↑(mapDomainBialgHom R (mapDomainOfBialgHom f))).comp singleOneAlgHom = (↑f).comp singleOneAlgHom
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : r ∈ annihilator R N
f : N →ₗ[R] M
x : N
⊢ r • f x = r • 0

Tactic:
smul_zero,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : r ∈ annihilator R N
f : N →ₗ[R] M
x : N
⊢ r • f x = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
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
⊢ #(∅.sym n) = 0

Tactic:
card_eq_zero,

Goal state after:
case neg
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
⊢ ∅.sym n = ∅
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 • ⊤ < ⊤
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE

Tactic:
by
  -- two main implications `3 → 4` and `4 → 1` are separated out, the rest are trivial
  have ntrQ : Nontrivial (R ⧸ I) := by
    apply Submodule.Quotient.nontrivial_iff.mpr
    by_contra eq
    simp [eq] at smul_lt
  have suppQ : Module.support R (Shrink.{v} (R ⧸ I)) = PrimeSpectrum.zeroLocus I := by
    rw [(Shrink.linearEquiv R _).support_eq, Module.support_eq_zeroLocus, annihilator_quotient]
  tfae_have 1 → 2 := fun h1 i hi ↦ h1 (ModuleCat.of R (Shrink.{v} (R ⧸ I)))
    inferInstance inferInstance suppQ.subset i hi
  tfae_have 2 → 3 := fun h2 ↦ ⟨(ModuleCat.of R (Shrink.{v} (R ⧸ I))),
    inferInstance, Module.Finite.equiv (Shrink.linearEquiv R (R ⧸ I)).symm, suppQ, h2⟩
  tfae_have 3 → 4 := fun ⟨N, _, _, h_supp, h_ext⟩ ↦
    exists_isRegular_of_exists_subsingleton_ext I n M smul_lt N h_supp h_ext
  tfae_have 4 → 1 := fun ⟨rs, len, mem, reg⟩ N Nntr Nfin Nsupp i hi ↦
    subsingleton_ext_of_exists_isRegular I N Nsupp M smul_lt rs mem reg i (hi.trans_eq len.symm)
  tfae_finish

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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]

Goal state after: