mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ UniqueFactorizationMonoid R

Tactic:
by

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
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by

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

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

Tactic:
by

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
⊢ (inhomogeneousChains A).d 1 0 = 0

Tactic:
by

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

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
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J
⊢ I = J

Tactic:
by

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
⊢ SurjOn (⇑constantCoeff) (↑I) S

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = (ConcreteCategory.hom (H1π A)) y ↔ ↑x - ↑y ∈ boundaries₁ A

Tactic:
by

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ constantCoeff 0 = 0

Tactic:
by

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 : ↑(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:
by

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
⊢ π A 1 ≫ (H1Iso A).hom = (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (single (g, h) a) =
    ↑((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv) (single g a + single h a)) -
      ↑((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv) (single (g * h) a))

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g 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:
by

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:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1ToTensorOfIsTrivial A)
      ((ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
by

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
⊢ ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ
        (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom =
    ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ LinearMap.id).toAddMonoidHom

Tactic:
by

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
hr₁ : r₁ ∈ Submodule.span R S
hr₂ : r₂ ∈ Submodule.span R S
s₁ : R⟦X⟧
hs₁mem : s₁ ∈ span T
hs₁ : constantCoeff s₁ = r₁
s₂ : R⟦X⟧
hs₂mem : s₂ ∈ span T
hs₂ : constantCoeff s₂ = r₂
⊢ constantCoeff (s₁ + s₂) = r₁ + r₂

Tactic:
by

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
⊢ (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv)
            (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) =
    (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv) LinearMap.id.toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1AddEquivOfIsTrivial A)
      ((ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) =
    (ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))

Tactic:
by

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f✝ : R⟦X⟧
hf✝ : constantCoeff f✝ ∈ span S
r₁ r₂ : R
hr₁ : r₂ ∈ Submodule.span R S
f : R⟦X⟧
hfmem : f ∈ span T
hf : constantCoeff f = r₂
⊢ constantCoeff (r₁ • f) = r₁ • r₂

Tactic:
by

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
⊢ ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ↑x ∈ boundaries₂ A

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = (ConcreteCategory.hom (H2π A)) y ↔ ↑x - ↑y ∈ boundaries₂ A

Tactic:
by

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:
by

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
⊢ π A 2 ≫ (H2Iso A).hom = (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
by

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
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I = spanFinrank (Ideal.map constantCoeff I)

Tactic:
by

Goal state after:
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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
by

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:
by

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 : ↑(I ^ i) ⊆ U
⊢ ↑(I ^ i) = ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ P.FG ↔ (Ideal.map constantCoeff P).FG

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
⊢ (𝓝 x).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ x + y) '' ↑(I ^ n)

Tactic:
by

Goal state after:
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 : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 ∈ (fun x ↦ x • m) ⁻¹' ↑(I ^ i • ⊤)

Tactic:
by

Goal state after:
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
n : ℕ
⊢ OpenAddSubgroup R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst✝² : P.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
⊢ UniqueFactorizationMonoid R⟦X⟧

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ↔ T2Space R

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m✝ n✝ : ℕ
x✝ : m✝ ≤ n✝
⊢ m✝ ∈ Finset.Iic n✝

Tactic:
by

Goal state after:
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m✝ n✝ : ℕ
x✝ : m✝ ≤ n✝
⊢ m✝ ∈ Finset.Iic m✝

Tactic:
by

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
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
obtain ⟨L, hL⟩ := H (fun i ↦ u ((Finset.Iic i).sup N))
      fun _ ↦ hN _ _ (Finset.le_sup (by simpa)) _ (Finset.le_sup (by simp))

Goal state after:
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
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
this : ∀ (i : ℕ), ∃ N, ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i
⊢ Filter.Tendsto u Filter.atTop (𝓝 L)

Tactic:
by

Goal state after:
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
⊢ i ∈ Finset.Iic i

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
⊢ C ((↑↑constantCoeff).toFun x✝) = x✝

Tactic:
ext x; simp [Subsingleton.eq_zero x]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
⊢ C ((↑↑constantCoeff).toFun x✝) = x✝

Tactic:
by

Goal state after:
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
⊢ IsPrecomplete I R ↔ CompleteSpace R

Tactic:
by

Goal state after:
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
⊢ IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff n) (optionFunLeft σ R p)) = (coeff (optionElim n x)) p

Tactic:
by

Goal state after:
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 }
⊢ IsAdic I

Tactic:
by

Goal state after:
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 }
⊢ IsAdic (Ideal.map e I)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R

Tactic:
by

Goal state after:
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
⊢ IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R

Tactic:
by

Goal state after:
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
⊢ IsAdicComplete (Ideal.map e I) S ↔ IsAdicComplete I R

Tactic:
by

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

Goal state before:
pp: σ : 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
h : y = x.some
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ IsAdic J ↔ (∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
⊢ optionFunLeft σ R ((monomial x) r) = (PowerSeries.monomial (x none)) ((monomial x.some) r)

Tactic:
by

Goal state after: