mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_2
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})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
· rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
r : R
⊢ (killCompl e) (C r) = C r

Tactic:
simpa using

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
r : R
⊢ (killCompl e) (C r) = C r
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ (∀ b ∈ ∅, Prime b) ∧ Associated ∅.prod z

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ Associated 1 z
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
n : ℕ
H : G n ∈ I
⊢ G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)

Tactic:
simpa using

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
n : ℕ
H : G n ∈ I
⊢ G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case succ
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 : ℕ
IH : g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
⊢ g - ∑ i, ↑((trunc (n + 1)) (H i)) * F i = X ^ (n + 1) * G (n + 1)

Tactic:
simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]

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
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↑A), C ((ConcreteCategory.hom (H0π A)) x)
y : ↑(cycles A 0)
⊢ C ((ConcreteCategory.hom (π A 0)) y)

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↑A), C ((ConcreteCategory.hom (H0π A)) x)
y : ↑(cycles A 0)
⊢ C ((ConcreteCategory.hom (π A 0)) y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
this : a ∈ closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
induction this using closure_induction 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 : ℕ), 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)

Tactic:
simpa using

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 = ∑ x, (coeff n) (H x * F x)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
hr : r ∈ S
⊢ r ∈ ⇑constantCoeff '' ↑I

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
hr : r ∈ S
⊢ ∃ x ∈ I, constantCoeff x = r
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H1 A) → Prop
x : ↑(H1 A)
h : ∀ (x : ↥(cycles₁ A)), C ((ConcreteCategory.hom (H1π A)) x)
y : ↑(cycles A 1)
⊢ C ((ConcreteCategory.hom (π A 1)) y)

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H1 A) → Prop
x : ↑(H1 A)
h : ∀ (x : ↥(cycles₁ A)), C ((ConcreteCategory.hom (H1π A)) x)
y : ↑(cycles A 1)
⊢ C ((ConcreteCategory.hom (π A 1)) y)
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 h : G
a : ↑A
⊢ (Multiplicative.toAdd
        (Multiplicative.ofAdd
          (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle (g * h))).toIntLinearMap))
      a =
    (Multiplicative.toAdd
        (Multiplicative.ofAdd
            (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                  ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle g)).toIntLinearMap *
          Multiplicative.ofAdd
            (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ
                  ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle h)).toIntLinearMap))
      a

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (H1π A)) ((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv) (single (g * h) a)) =
    (ModuleCat.Hom.hom (H1π A)) ((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv) (single g a + single h a))
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 y : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = (ConcreteCategory.hom (H2π A)) y ↔ ↑x - ↑y ∈ boundaries₂ A

Tactic:
rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]
  rfl

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
C : ↑(H2 A) → Prop
x : ↑(H2 A)
h : ∀ (x : ↥(cycles₂ A)), C ((ConcreteCategory.hom (H2π A)) x)
y : ↑(cycles A 2)
⊢ C ((ConcreteCategory.hom (π A 2)) y)

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H2 A) → Prop
x : ↑(H2 A)
h : ∀ (x : ↥(cycles₂ A)), C ((ConcreteCategory.hom (H2π A)) x)
y : ↑(cycles A 2)
⊢ C ((ConcreteCategory.hom (π A 2)) y)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤

Tactic:
by
        simpa only [smul_eq_mul, mul_top, Algebra.algebraMap_self, map_id, le_inf_iff] using! this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ↑(I ^ i) ⊆ U

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ↑(I ^ i) ⊆ U
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

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
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: 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
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∀ (i : ℕ), ∃ N, ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i

Tactic:
simpa using

Goal state after:
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
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∀ (i : ℕ), ∃ N, ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
s : Set R
hs : s ∈ 𝓝 0
⊢ ∃ n, ↑(J ^ n) ⊆ s

Tactic:
simpa using

Goal state after:
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
s : Set R
hs : s ∈ 𝓝 0
⊢ ∃ n, ↑(J ^ n) ⊆ s
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: 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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
i : ℕ
x✝ : True
m : ℕ
hm : i ≤ m
n : ℕ
hn : i ≤ n
⊢ (f m, f n) ∈ {x | x.2 - x.1 ∈ ↑(I ^ i)}

Tactic:
simpa using

Goal state after:
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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
i : ℕ
x✝ : True
m : ℕ
hm : i ≤ m
n : ℕ
hn : i ≤ n
⊢ f n - f m ∈ I ^ i
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: 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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i

Tactic:
simpa using

Goal state after:
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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → -L + f n ∈ I ^ i
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i N : ℕ
hN : ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i
⊢ f i - L ∈ I ^ i

Tactic:
simpa using

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
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i N : ℕ
hN : ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i
⊢ f i - L ∈ I ^ i
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 }
⊢ IsUniformEmbedding ⇑↑(WithIdeal.uniformEquiv e ⋯)

Tactic:
simpa using

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 }
⊢ IsUniformEmbedding ⇑(WithIdeal.uniformEquiv e ⋯)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : n = x none
⊢ r = (coeff y) ((monomial x.some) r)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ r = (coeff y) 0

pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
⊢ 0 = (coeff y) ((monomial x.some) r)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0

Tactic:
· simp [← h1]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ r = (coeff y) 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
⊢ 0 = (coeff y) ((monomial x.some) r)

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)
_h' : ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen[inst✝¹] {0}

Tactic:
simpa using

Goal state after:
case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)
_h' : ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen[inst✝¹] {0}
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
f : R →+* S
hf : Ideal.map f i ≤ i
n : ℕ
x✝ : True
⊢ Ideal.map f (i ^ n) ≤ i ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
f : R →+* S
hf : Ideal.map f i ≤ i
n : ℕ
x✝ : True
⊢ Ideal.map f i ^ n ≤ i ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (r : R),
    optionFunLeft σ R ((algebraMap R (MvPowerSeries (Option σ) R)) r) =
      (algebraMap R (PowerSeries (MvPowerSeries σ R))) r

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (r : R), optionFunLeft σ R (C r) = C (C r)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
this : optionElim 0 (single i 1) = single (Option.some i) 1
⊢ (optionEquivLeft σ R) (X (Option.some i)) = PowerSeries.C (X i)

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
this : optionElim 0 (single i 1) = single (Option.some i) 1
⊢ (optionEquivLeft σ R) (X (Option.some i)) = PowerSeries.C (X i)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ (optionEquivLeft σ R) (X none) = PowerSeries.X

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ (optionEquivLeft σ R) (X none) = PowerSeries.X
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (optionEquivLeft σ R) (C r) = PowerSeries.C (C r)

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (optionEquivLeft σ R) (C r) = PowerSeries.C (C r)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
⊢ RingHom.ker (Ideal.Quotient.mk I) ≤ m

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
⊢ I ≤ m
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ↔ ↑x 1 = 0

Tactic:
maximalIdeal_eq_map,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R) ↔ ↑x 1 = 0
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: 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
⊢ (of (maximalIdeal R) R) ((algebraMap R R) z) - y ∈ (eval (maximalIdeal R) R 1).ker

Tactic:
simpa using

Goal state after:
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
⊢ (Ideal.Quotient.mk (maximalIdeal R ^ 1 * ⊤)) z = ↑y 1
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
m✝ n✝ : ℕ
h : m✝ ≤ n✝
x✝ : MvPowerSeries σ R
⊢ ((Ideal.Quotient.factorₐ (MvPolynomial σ R) ⋯).comp (truncTotalAlgHom σ R n✝)) x✝ = (truncTotalAlgHom σ R m✝) x✝

Tactic:
simpa using

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
m✝ n✝ : ℕ
h : m✝ ≤ n✝
x✝ : MvPowerSeries σ R
⊢ (truncTotal n✝) x✝ - (truncTotal m✝) x✝ ∈ MvPolynomial.idealOfVars σ R ^ m✝
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
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
hm : ↑m' ∈ maximalIdeal R ^ 2 * ⊤
⊢ m = 0

Tactic:
simpa using

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
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
hm : ↑m' ∈ maximalIdeal R ^ 2 * ⊤
⊢ ↑m' ∈ maximalIdeal R ^ 2
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
⊢ π A n ≫ map f φ n = cyclesMap f φ n ≫ π B n

Tactic:
by
  simp [map, cyclesMap]

Goal state after: