mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U

case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U
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:
constructor

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

case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J
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
⊢ (∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n) ↔ CompleteSpace R

Tactic:
constructor

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
⊢ (∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n) → CompleteSpace R

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.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
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
⊢ (∀ (n : ℕ), IsOpen[J.adicTopology] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
constructor

Goal state after:
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := ⋯
⊢ ∀ (n : ℕ), IsOpen[J.adicTopology] ↑(J ^ n)

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 := ⋯
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
constructor

Goal state after:
case mpr.h.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := ⋯
⊢ s ∈ 𝓝 0 → ∃ i, True ∧ ↑(J ^ i) ⊆ s

case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := ⋯
⊢ (∃ i, True ∧ ↑(J ^ i) ⊆ s) → s ∈ 𝓝 0
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:
isAdicComplete_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
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 : σ →₀ ℕ
h3 : n = x none
h1 : ¬y = x.some
⊢ 0 = (coeff y) ((monomial x.some) r)

Tactic:
rw [coeff_monomial, if_neg h1]

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

Goal state before:
pp: 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)) ∧ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
constructor

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

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.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)

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

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

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s) ↔ DiscreteTopology A

Tactic:
constructor

Goal state after:
case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A

case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s

Tactic:
constructor

Goal state after:
case mpr.left
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)

case mpr.right
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
⊢ optionFunLeft σ R (p * q) = optionFunLeft σ R p * optionFunLeft σ R q

Tactic:
classical
  ext k x
  simp only [coeff_coeff_optionFunLeft, coeff_mul, PowerSeries.coeff_mul, map_sum, sum_sigma']
  refine sum_bij (fun y _ ↦ ⟨(y.1 none, y.2 none), (y.1.some, y.2.some)⟩) ?_ ?_ ?_ ?_
  · intros; simp_all [Finsupp.ext_iff]
  · intros; ext t <;> cases t
    all_goals simp_all [Finsupp.ext_iff]
  · rintro ⟨⟨m, n⟩, ⟨u, v⟩⟩ h
    suffices ∃ a b, (a none = m ∧ b none = n) ∧ a.some = u ∧ a + b = optionElim k x ∧
      b.some = v by simpa
    use u.optionElim m, v.optionElim n
    suffices optionElim m u + optionElim n v = optionElim k x by simp_all
    ext t; cases t <;> simp_all [Finsupp.ext_iff]
  · intros; simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
⊢ optionInvFunLeft σ R (optionFunLeft σ R x✝) = x✝

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
n✝ : Option σ →₀ ℕ
⊢ (coeff n✝) (optionInvFunLeft σ R (optionFunLeft σ R x✝)) = (coeff n✝) x✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
⊢ optionFunLeft σ R (optionInvFunLeft σ R x✝) = x✝

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (optionInvFunLeft σ R x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝¹ x✝ : MvPowerSeries (Option σ) R
⊢ optionFunLeft σ R (x✝¹ + x✝) = optionFunLeft σ R x✝¹ + optionFunLeft σ R x✝

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝¹ x✝ : MvPowerSeries (Option σ) R
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (x✝¹ + x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R x✝¹ + optionFunLeft σ R x✝))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
coeff_coeff_optionEquivLeft,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (optionElim k x)) ((rename ⇑(_root_.finSuccEquiv n).toEmbedding) p) = (coeff (Finsupp.cons k x)) p
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 j : ℕ
⊢ ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousChains B).d (j + 1) j =
    (inhomogeneousChains A).d (j + 1) j ≫
      ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
n j : ℕ
g✝ : Fin (j + 1) → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin j → H
⊢ ((ModuleCat.Hom.hom
          (ModuleCat.ofHom (lsingle g✝) ≫
            ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
              (inhomogeneousChains B).d (j + 1) j))
        x✝)
      a✝ =
    ((ModuleCat.Hom.hom
          (ModuleCat.ofHom (lsingle g✝) ≫
            (inhomogeneousChains A).d (j + 1) j ≫
              ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)))
        x✝)
      a✝
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
ext

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
f : G →* H
φ ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
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 : ℕ
x : Fin n → G
⊢ ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n = ModuleCat.ofHom (lsingle (⇑f ∘ x) ∘ₗ (Hom.hom φ).toLinearMap)

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : Fin n → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin n → H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle (⇑f ∘ x) ∘ₗ (Hom.hom φ).toLinearMap))) x✝) a✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ chainsMap (g.comp f) (φ ≫ (resFunctor f).map ψ) = chainsMap f φ ≫ chainsMap g ψ

Tactic:
ext

Goal state after:
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → K
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap (g.comp f) (φ ≫ (resFunctor f).map ψ)).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ ≫ chainsMap g ψ).f i✝)) x✝) a✝
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
⊢ chainsMap f 0 = 0

Tactic:
ext

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
f : G →* H
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f 0).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ HomologicalComplex.Hom.f 0 i✝)) x✝) a✝
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 ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
n : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
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
⊢ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
g✝ : Fin 0 → G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom)) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ)) x✝
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
⊢ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ chainsMap₂ f φ

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
g✝ : Fin 2 → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : H × H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsIso₂ A).hom ≫ chainsMap₂ f φ)) x✝) a✝
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
⊢ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom = (chainsIso₃ A).hom ≫ chainsMap₃ f φ

Tactic:
ext

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
f : G →* H
φ : A ⟶ res f B
g✝ : Fin 3 → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : H × H × H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsIso₃ A).hom ≫ chainsMap₃ f φ)) x✝) a✝
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)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
rw [IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg,
    IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg', eq_comm]

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)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R) =
    Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = H0π A ≫ (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom (H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom)) x✝ =
    (ModuleCat.Hom.hom (H0π A ≫ (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f)) x✝
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
x✝ : MvPowerSeries σ R
⊢ toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝) = x✝

Tactic:
ext

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
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝)) = (coeff n✝) x✝
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
⊢ (↑(ofAlgEquiv I)).comp (liftRingHom I f ⋯) = AdicCompletion.liftRingHom I f ⋯

Tactic:
ext

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
x✝ : R
n✝ : ℕ
⊢ ↑(((↑(ofAlgEquiv I)).comp (liftRingHom I f ⋯)) x✝) n✝ = ↑((AdicCompletion.liftRingHom I f ⋯) x✝) n✝
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 : ℕ
⊢ (Ideal.Quotient.mk (I ^ n)).comp (liftRingHom I f ⋯) = f n

Tactic:
ext

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)).comp (liftRingHom I f ⋯)) x✝ = (f n) x✝
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
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝) = x✝

Tactic:
ext

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
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
n✝ : ℕ
⊢ ↑((↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝)) n✝ = ↑x✝ n✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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
⊢ (mapShortComplexH1 f 0).τ₁ = Hom.τ₁ 0

Tactic:
ext

Goal state after:
case refine_1
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✝¹ : G × G
x✝ : ↑A
a✝ : H × H
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 f 0).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (Hom.τ₁ 0) ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
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
⊢ (mapShortComplexH1 f 0).τ₂ = Hom.τ₂ 0

Tactic:
ext

Goal state after:
case refine_2
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✝¹ : G
x✝ : ↑A
a✝ : H
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 f 0).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (Hom.τ₂ 0) ∘ₗ lsingle a✝¹) x✝) a✝