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

Goal state before:
pp: case refine_1
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
⊢ span ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) ≤ I

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 ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ)

Tactic:
<;>

Goal state after:
case refine_1
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
⊢ span ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) ≤ I

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 ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
y : G × G →₀ A
hy : (y.sum fun g a ↦ single g.2 (g.1⁻¹ • a) - single (g.1 * g.2) a + single g.1 a) = x
⊢ ((y.sum fun g a ↦ single g (g.1⁻¹ • a)).sum fun g a ↦
      single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) =
    x

Tactic:
simp_all [sum_sum_index]

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

Goal state before:
pp: case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x✝ : G →₀ A
x : G × G →₀ A
hx : (x.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x✝
⊢ ((x.sum fun g a ↦ single g (g.1 • a)).sum fun g a ↦ single g.2 (g.1⁻¹ • a) - single (g.1 * g.2) a + single g.1 a) = x✝

Tactic:
simp_all [sum_sum_index]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = ∑ i ∈ Set.Finite.toFinset ⋯, (coeff i) p • (coeff n) (i.prod fun s e ↦ (X ∘ f) s ^ e)

Tactic:
have (d : σ →₀ ℕ) (hd : (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0) :
      mapDomain f d = n := by
    simp_rw [← monomial_mapDomain_apply_one] at hd
    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = ∑ i ∈ Set.Finite.toFinset ⋯, (coeff i) p • (coeff n) (i.prod fun s e ↦ (X ∘ f) s ^ e)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
y : G × G × G →₀ A
hy :
  (y.sum fun g a ↦
      single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
⊢ ((y.sum fun g a ↦ single g (g.1⁻¹ • a)).sum fun g a ↦
      single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x

Tactic:
simp_all [sum_sum_index]

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

Goal state before:
pp: case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x✝ : G × G →₀ A
x : G × G × G →₀ A
hx :
  (x.sum fun g a ↦
      single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x✝
⊢ ((x.sum fun g a ↦ single g (g.1 • a)).sum fun g a ↦
      single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x✝

Tactic:
simp_all [sum_sum_index]

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
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ span {X} ⊔ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem]

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:
suffices ∀ i : ℕ, ∃ j : ℕ, (↑(I ^ j) * ↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R) by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: 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

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

Tactic:
<;>

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
⊢ T2Space R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R

Tactic:
hI.isPrecomplete_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ T2Space R ∧ CompleteSpace R ↔ CompleteSpace R ∧ T2Space R
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
  rw [optionFunLeft, PowerSeries.coeff_mk]
  exact LinearMap.proj_apply ..

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

Goal state before:
pp: case none
σ : 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
⊢ (optionElim n y) none = x none

pp: case some
σ : 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
val✝ : σ
⊢ (optionElim n y) (Option.some val✝) = x (Option.some val✝)

Tactic:
<;>

Goal state after:
case none
σ : 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
⊢ (optionElim n y) none = x none

case some
σ : 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
val✝ : σ
⊢ (optionElim n y) (Option.some val✝) = x (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_2.fst
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
t : Option σ
⊢ a₁✝.1 t = a₂✝.1 t

pp: case refine_2.snd
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
t : Option σ
⊢ a₁✝.2 t = a₂✝.2 t

Tactic:
<;>

Goal state after:
case refine_2.fst
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
t : Option σ
⊢ a₁✝.1 t = a₂✝.1 t

case refine_2.snd
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
t : Option σ
⊢ a₁✝.2 t = a₂✝.2 t
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
⊢ ContinuousAt (⇑f) 0

Tactic:
ContinuousAt,

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
⊢ Tendsto (⇑f) (𝓝 0) (𝓝 (f 0))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case h.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ (optionElim m u + optionElim n v) none = (optionElim k x) none

pp: case h.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
val✝ : σ
⊢ (optionElim m u + optionElim n v) (Option.some val✝) = (optionElim k x) (Option.some val✝)

Tactic:
<;>

Goal state after:
case h.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ (optionElim m u + optionElim n v) none = (optionElim k x) none

case h.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
val✝ : σ
⊢ (optionElim m u + optionElim n v) (Option.some val✝) = (optionElim k x) (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (optionElim 0 (single i 1)) none = (single (Option.some i) 1) none

pp: case some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i val✝ : σ
⊢ (optionElim 0 (single i 1)) (Option.some val✝) = (single (Option.some i) 1) (Option.some val✝)

Tactic:
<;>

Goal state after:
case none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (optionElim 0 (single i 1)) none = (single (Option.some i) 1) none

case some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i val✝ : σ
⊢ (optionElim 0 (single i 1)) (Option.some val✝) = (single (Option.some i) 1) (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case none
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) none = (optionElim i x) none

pp: case some
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
val✝ : Fin n
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) (Option.some val✝) = (optionElim i x) (Option.some val✝)

Tactic:
<;>

Goal state after:
case none
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) none = (optionElim i x) none

case some
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
val✝ : Fin n
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) (Option.some val✝) = (optionElim i x) (Option.some val✝)
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ ↑e'.symm ∘ₗ B.ρ h = (MonoidHom.comp A.ρ ↑e.symm) h ∘ₗ ↑e'.symm

Tactic:
rw [LinearEquiv.toLinearMap_symm_comp_eq, ← LinearMap.comp_assoc]
    simp [he, LinearMap.comp_assoc]

Goal state after:
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n ≫
      map (↑e.symm) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n =
    𝟙 (groupHomology A n)

Tactic:
by
    rw [← groupHomology.map_comp, ← groupHomology.map_id]
    exact groupHomology.map_congr e.coe_monoidHom_symm_comp_coe_monoidHom e'.symm_comp n

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
x✝ : ↑(shortComplexH1 A).X₁
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₁) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₁) x✝

pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₂
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₂) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₂) x✝

pp: case h₃
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₃
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₃) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₃) x✝

Tactic:
<;>

Goal state after:
case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₁
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₁) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₁) x✝

case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₂
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₂) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₂) x✝

case h₃
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₃
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₃) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₃) x✝
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : n ≤ i
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

pp: case neg
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : i < n
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

Tactic:
· obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
    rw [ofPowSMul_val_apply _ rfl, ofValEqZero, ofValEqZeroAux_prop]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : i < n
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ Injective val

Tactic:
rintro ⟨a, ha⟩; congr!

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ ↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul = lTensor (C ⧸ I) comul ∘ₗ comul

pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ rTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1

pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ lTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1

Tactic:
<;>

Goal state after:
case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ ↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul = lTensor (C ⧸ I) comul ∘ₗ comul

case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ rTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1

case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ lTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ =
    (lTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ

pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (rTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (lTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
<;>

Goal state after:
case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ =
    (lTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ

case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (rTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (lTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
      ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)) =
    (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm

pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
      ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)) =
    (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm

case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I) =
    ↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm