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
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ) = 𝟙 A

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom (𝟙 A)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ) = 0

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom 0
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ) = 0

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom 0
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ) = 𝟙 B

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom (𝟙 B)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
r : k
f : M ⟶ N
g : N ⟶ O
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
r : k
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom ((r • f) ≫ g) = Hom.hom (r • f ≫ g)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
⊢ Hom.hom (α_ X Y Z).hom = ↑(assoc X.ρ Y.ρ Z.ρ)

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
⊢ (Hom.hom (α_ X Y Z).hom).toLinearMap = (↑(assoc X.ρ Y.ρ Z.ρ)).toLinearMap
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ x✝² ◁ 0 = 0

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ Hom.hom (x✝² ◁ 0) = Hom.hom 0
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ 0 ▷ x✝² = 0

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ Hom.hom (0 ▷ x✝²) = Hom.hom 0
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (x✝¹ + x✝) = X✝ ◁ x✝¹ + X✝ ◁ x✝

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ (x✝¹ + x✝)) = Hom.hom (X✝ ◁ x✝¹ + X✝ ◁ x✝)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ (x✝¹ + x✝) ▷ X✝ = x✝¹ ▷ X✝ + x✝ ▷ X✝

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ Hom.hom ((x✝¹ + x✝) ▷ X✝) = Hom.hom (x✝¹ ▷ X✝ + x✝ ▷ X✝)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ x✝⁴ ◁ (x✝¹ • x✝) = x✝¹ • x✝⁴ ◁ x✝

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ Hom.hom (x✝⁴ ◁ (x✝¹ • x✝)) = Hom.hom (x✝¹ • x✝⁴ ◁ x✝)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ (x✝⁴ • x✝¹) ▷ x✝ = x✝⁴ • x✝¹ ▷ x✝

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ Hom.hom ((x✝⁴ • x✝¹) ▷ x✝) = Hom.hom (x✝⁴ • x✝¹ ▷ x✝)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝³ x✝² x✝¹ : Rep k G
x✝ : x✝² ⟶ x✝¹
⊢ x✝³ ◁ x✝ ≫ (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝¹.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝².ρ)).hom ≫ x✝ ▷ x✝³

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝³ x✝² x✝¹ : Rep k G
x✝ : x✝² ⟶ x✝¹
⊢ Hom.hom (x✝³ ◁ x✝ ≫ (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝¹.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm x✝³.ρ x✝².ρ)).hom ≫ x✝ ▷ x✝³)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Rep k G
⊢ x✝¹ ▷ x✝ ≫ (mkIso (Representation.TensorProduct.comm Y✝.ρ x✝.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm X✝.ρ x✝.ρ)).hom ≫ x✝ ◁ x✝¹

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Rep k G
⊢ Hom.hom (x✝¹ ▷ x✝ ≫ (mkIso (Representation.TensorProduct.comm Y✝.ρ x✝.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm X✝.ρ x✝.ρ)).hom ≫ x✝ ◁ x✝¹)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
⊢ Hom.hom ((β_ X Y).hom ≫ (β_ Y X).hom) = Hom.hom (𝟙 (X ⊗ Y))
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z : Action (Type u) G
f : X✝ ⟶ Y✝
⊢ (linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝) =
    ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f)

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z : Action (Type u) G
f : X✝ ⟶ Y✝
⊢ Hom.hom ((linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝)) =
    Hom.hom (ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f))
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom =
    (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom ≫
      (linearization k G).obj X ◁ ofHom (μ Y Z) ≫ ofHom (μ X (Y ⊗ Z))

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ Hom.hom (ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom) =
    Hom.hom
      ((α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom ≫
        (linearization k G).obj X ◁ ofHom (μ Y Z) ≫ ofHom (μ X (Y ⊗ Z)))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ X.d (n + 1 + 1) = 0

Tactic:
rw [d_succ _ (n + 1), Preadditive.comp_sub]

Goal state after:
case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - X.d (n + 1) ≫ (coind₁Functor k G).map (X.d (n + 1)) = 0
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom

Tactic:
ext1

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
          (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (trivial k G k)).f
      0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 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
i j : ℕ
y : (Fin i → G) → ↑X.X₂
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).X₂.d i j))) y

Tactic:
by simpa using! hx

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
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).X₂.d i j))) y

Tactic:
by simpa using! hx

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

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
replace hε := hε.symm
    rw [← h, eq_div_iff_mul_eq] at hε
    · replace hε := congr_arg (t • ·) hε
      rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← g.toAlgHom_apply,
        ← AlgHom.map_smul_of_tower, this] at hε
      apply IsIntegralClosure.algebraMap_injective B A L
      rw [map_mul, ← hε]
      congr 1
      exact algebraMap_galRestrictHom_apply A K L B g a
    · intro e
      rw [(map_eq_zero _).mp e, zero_div] at hε
      rw [hε, Algebra.norm_zero] at hη
      exact zero_ne_one hη

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
i j : ℕ
y : (Fin i → G) →₀ ↑X.X₂
x : (Fin j → G) →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (chainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (chainsFunctor k G)).X₂.d i j))) y

Tactic:
by simpa using! hx

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
i j : ℕ
hij : j + 1 = i
z : (Fin i → G) →₀ ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d i j)) z = 0
y : (Fin i → G) →₀ ↑X.X₂
hy : (ConcreteCategory.hom ((chainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (chainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (chainsFunctor k G)).X₂.d i j))) y

Tactic:
by simpa using! hx

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)

Tactic:
ext1

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ ModuleCat.Hom.hom ((map (f + g)).f (Int.negSucc i)) = ModuleCat.Hom.hom ((map f + map g).f (Int.negSucc i))
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)

Tactic:
ext1
    simp only [CochainComplex.ConnectData.map_f, chainsMap_id_f_hom_eq_mapRange, Rep.add_hom,
      Representation.IntertwiningMap.add_toLinearMap, HomologicalComplex.add_f_apply,
      ModuleCat.hom_add]
    ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
x✝¹ : k
x✝ : G → k
⊢ ∑ s, (x✝¹ • x✝) s • (X.ρ s⁻¹) v = (RingHom.id k) x✝¹ • ∑ s, x✝ s • (X.ρ s⁻¹) v

Tactic:
by simp [smul_sum, smul_smul]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬I.FG}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span ↑G = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : ↑G ⊆ ↑J
⊢ J = sSup C

Tactic:
exact le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
· refine ⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩
    rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]
    intro x hx
    rcases (Submodule.mem_sSup_of_directed ⟨_, hI⟩ hC₂.directedOn).1 hx.1 with ⟨J, hJ₁, hJ₂⟩
    have hx₂ : (J : Set R) ∩ S ≠ ∅ := nonempty_iff_ne_empty.1 ⟨x, hJ₂, hx.2⟩
    exact hx₂ (mem_kaplanskySet_iff.mp (hC hJ₁))

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔ single g.2 a + single g.1 (g.1 • a) = single (g.1 * g.2) (g.1 • a)

Tactic:
← (Finsupp.mapRange_injective (α := G) _ (smul_zero _) (MulAction.bijective g.1⁻¹).1).eq_iff

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔
    mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single g.2 a + single g.1 (g.1 • a)) =
      mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single (g.1 * g.2) (g.1 • a))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ (finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp C) = C

Tactic:
ext1

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : R
⊢ ((finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp C)) x✝ = C 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✝ : ℕ
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:
LinearEquiv.toLinearMap_symm_comp_eq,

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = ↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h ∘ₗ ↑e'.symm
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
⊢ mapShortComplexH1 f 0 = 0

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ rfl

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
⊢ (mapShortComplexH1 f 0).τ₁ = Hom.τ₁ 0

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
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
⊢ mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ rfl

Goal state after:
case refine_1
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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₁ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁

case refine_2
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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₂ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
hf : constantCoeff f = 0
d : σ →₀ ℕ
s : σ
⊢ s ∈ {s | (MvPowerSeries.coeff d) ((PowerSeries.toMvPowerSeries s) f) ≠ 0} → s ∈ ↑d.support

Tactic:
contrapose
    simpa using fun hd ↦ toMvPowerSeries_coeff_eq_zero hd hf

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 : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ ⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv ∘ X =
    ⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ∘ MvPolynomial.X

Tactic:
ext1

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 : ℕ
σ : Type u_3
inst✝ : Finite σ
x✝ : σ
⊢ (⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv ∘ X) x✝ =
    (⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ∘
        MvPolynomial.X)
      x✝
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ (d • a) ⊗ₜ[R] (d • a) = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y

Tactic:
by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1

Tactic:
rw [Finset.sup'_lt_iff]

Goal state after:
case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ ∀ i ∈ p.support, (v.intAdicAbv hb) (p.coeff i) < 1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation (x * inv✝) = v.intValuation 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1

Tactic:
map_one,

Goal state after:
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation (x * inv✝) = 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0 → ⟨a, b⟩ = 0) ↔ ∀ x ∈ N, r • x = 0 → x = 0

Tactic:
by
      simp only [SetLike.mk_smul_mk, Submodule.mk_eq_zero]

Goal state after: