mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
M : Rep k G
⊢ Limits.IsZero M ↔ Subsingleton ↑M

Tactic:
by
  simp [Limits.IsZero.iff_id_eq_zero, Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff,
    ← ModuleCat.isZero_of_iff_subsingleton (R := k), ModuleCat.hom_ext_iff]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap = d k G (n + 1)

Tactic:
refine MonoidAlgebra.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_
  simp [standardComplex, Action.ofMulAction_V, SimplicialObject.δ, SimplexCategory.δ,
    Fin.succAboveOrderEmb, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ), ← ofHom_smul, ← ofHom_sum,
    Representation.IntertwiningMap.coe_toLinearMap, Representation.IntertwiningMap.sum_apply,
    Representation.IntertwiningMap.smul_apply, (Representation.linearizeMap_single),
    smul_eq_mul, mul_one]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
this : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0
⊢ (Hom.hom ((standardComplex k G).d 1 0 ≫ ε k G)).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝

Tactic:
exact LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).symm.hom ≫ (standardComplex k G).d (j + 1) j =
    (barComplex k G).d (j + 1) j ≫ (diagonalSuccIsoFree k G j).symm.hom

Tactic:
rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 0 (0 + 1)))
      ((ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z) =
    0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 0 (0 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1))) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y
      g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 1 (1 + 1)))
      ((ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z) =
    0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 1 (1 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1))) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)
      g

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y
      g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 1)) ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 1) ∘ₗ ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 2)) ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 2) ∘ₗ ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i j : ℕ
hij : i + 1 = j
⊢ ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousCochains B).d i j =
    (inhomogeneousCochains A).d i j ≫
      ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin j → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)

Tactic:
by
    subst hij
    ext
    simpa [inhomogeneousCochains.d_hom_apply, Fin.comp_contractNth, CochainComplex.of.d]
      using! (hom_comm_apply φ _ _).symm

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ (cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom = (cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
ext x
  simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]
  rfl

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₃).inv) ↑z) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 1 0) ∘ₗ ConcreteCategory.hom (chainsIso₁ X.X₃).inv) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y)) x✝

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0) ∘ₗ ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₃).inv) ↑z) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ X.X₃).inv) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y)) x✝

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y) x✝
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X Y : Rep R G
φ : X ⟶ Y
g✝¹ : Fin 0 → G
x✝ : ↑(ModuleCat.of R ↑X)
g✝ : Fin 0 → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫ (chainsMap (MonoidHom.id G) φ).f 0 ≫ (tateComplexConnectData Y).d₀))
      x✝ g✝ =
    (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Finsupp.lsingle g✝¹) ≫ (tateComplexConnectData X).d₀ ≫ (cochainsMap (MonoidHom.id G) φ).f 0))
      x✝ g✝

Tactic:
simp [Rep.tateNorm_eq, Representation.norm, Rep.hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 :
  (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X =
    η₁.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v

Tactic:
have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 :
  (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X =
    η₁.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (x✝¹ ≫ x✝) n = map (MonoidHom.id G) x✝¹ n ≫ map (MonoidHom.id G) x✝ n

Tactic:
simp only [← HomologicalComplex.homologyMap_comp]
    rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
refine this.trans ?_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ (∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.span (MvPolynomial σ R)
      ((fun x ↦ x.prod fun x1 x2 ↦ X x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ Set.univ}) =
    Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})

Tactic:
simp [monomial_eq, Set.preimage, degree]

Goal state after:
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
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ a • ∑ k, s k * r k ∈ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
range_smul,

Goal state after:
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
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ a • ∑ k, s k * r k ∈ span (a • Set.range i)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ⊥ ∈ kaplanskySet S ∧ ∀ J ∈ ∅, J ≤ ⊥

Tactic:
simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]

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 ((inhomogeneousChains A).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 1 0) ∘ₗ ConcreteCategory.hom (chainsIso₁ A).inv) ↑x = 0
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 ((inhomogeneousChains A).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) = 0

Tactic:
← LinearMap.comp_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ A).inv) ↑x = 0
Module: Mathlib.RingTheory.PowerSeries.Ideal

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

Tactic:
· intro ⟨S, hS⟩
    by_cases hX : X ∈ P
    · have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS
      have : (insert X <| (C (R := R)) '' S).Finite :=
        Finite.insert X <| Finite.image _ S.finite_toSet
      lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT
      exact ⟨T, hT ▸ H.symm⟩
    · obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet
      lift T to Finset R⟦X⟧ using hT₂
      exact ⟨T, hT.symm⟩

Goal state after:
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 • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
rcases H₂ s H with ⟨n, h⟩

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 • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
n : ℕ
h : ↑(J ^ n) ⊆ s
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s
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:
rw [optionFunLeft, PowerSeries.coeff_mk]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ ((coeff x) fun x ↦ (coeff (optionElim n x)) p) = (coeff (optionElim n 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
⊢ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ

Tactic:
ext x
  simp [chainsMap_f, chainsIso₁]

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

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst a ((toMvPowerSeries i) f) = subst (a i) f

Tactic:
rw [toMvPowerSeries_eq_subst, subst, MvPowerSeries.subst_comp_subst_apply
    (HasSubst.const (HasSubst.X _)) ha, MvPowerSeries.subst_X ha, subst]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i k : ℕ
h : i ≤ i + k
⊢ (powSMulQuotInclusion I M ⋯ ⊤) ((transitionMap I (↥(I ^ n • ⊤)) h) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) (i + k))) =
    ↑x (i + n)

Tactic:
← LinearMap.comp_apply,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i k : ℕ
h : i ≤ i + k
⊢ (powSMulQuotInclusion I M ⋯ ⊤ ∘ₗ transitionMap I (↥(I ^ n • ⊤)) h) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) (i + k)) =
    ↑x (i + n)
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
this : Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)
x : AdicCompletion I (↥s →₀ M)
⊢ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)) x =
    (ofPowSMul I M n) ((map I (LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)) x)

Tactic:
← LinearMap.comp_apply,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
this : Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)
x : AdicCompletion I (↥s →₀ M)
⊢ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)) x =
    (ofPowSMul I M n ∘ₗ map I (LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)) x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
g : G
this :
  (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) (((ModuleCat.Hom.hom (d₂₁ A)) W) g) =
    ((ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) (mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W)) g
⊢ ((mapRange.linearMap (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype))) (↑x + (ConcreteCategory.hom (d₂₁ A)) W)) g =
    ((mapRange.linearMap (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype))) ((lmapDomain (↑A) k ⇑S.subtype) Z)) g

Tactic:
simp [← mapDomain_mapRange, hZ, this, hW, hzw, coe_mapCycles₁ S.subtype,
        coe_mapCycles₁ (MonoidHom.id G)]

Goal state after: