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

Goal state before:
pp: k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y

Tactic:
have hγ (s : S) (g : G) : γ (s.1 * g) = s * γ g := by ext; simp [mul_assoc, γ, hmk]

Goal state after:
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
x✝¹ x✝ : ↥(Representation.coindV φ A.ρ)
⊢ ∀ (h : H),
    (Hom.hom
            (ofHom
              { toLinearMap := linearCombination k ↑(x✝¹ + x✝) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                isIntertwining' := ⋯ })).toLinearMap
        (MonoidAlgebra.single h 1) =
      (Hom.hom
            (ofHom
                { toLinearMap := linearCombination k ↑x✝¹ ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                  isIntertwining' := ⋯ } +
              ofHom
                { toLinearMap := linearCombination k ↑x✝ ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                  isIntertwining' := ⋯ })).toLinearMap
        (MonoidAlgebra.single h 1)

Tactic:
simp [Rep.add_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₁ →ⁱL π₂
⊢ ∀ (g : G), (-f.toContinuousLinearMap) ∘SL π₁ g = π₂ g ∘SL (-f.toContinuousLinearMap)

Tactic:
by simp [f.2]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : Rep k G
X✝ Y✝ : Action (ModuleCat k) G
f : X✝ ⟶ Y✝
g : G
⊢ ModuleCat.Hom.hom f.hom ∘ₗ (X✝.V.endRingEquiv.toMonoidHom.comp X✝.ρ) g =
    (Y✝.V.endRingEquiv.toMonoidHom.comp Y✝.ρ) g ∘ₗ ModuleCat.Hom.hom f.hom

Tactic:
simpa using ModuleCat.hom_ext_iff.1 (f.comm g)

Goal state after:
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
⊢ Hom.hom
      ({ pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.fst ≫
          { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inl +
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.snd ≫
          { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inr) =
    Hom.hom
      (𝟙
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.pt)

Tactic:
simp [Rep.add_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : f ≠ 0
this : Epi (Abelian.image.ι f)
⊢ Epi f

Tactic:
by
        rw [← Abelian.image.fac f]
        exact epi_comp _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
α : Type u'
A : Rep k G
f g : free k G α ⟶ A
h : ∀ (i : α), (Hom.hom f) (single i (MonoidAlgebra.single 1 1)) = (Hom.hom g) (single i (MonoidAlgebra.single 1 1))
⊢ f = g

Tactic:
by
  exact (freeLiftLEquiv k G α A).injective (funext_iff.2 h)

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

Tactic:
simp [μ_comp_assoc _]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Tactic:
· simp [indToCoindAux_of_not_rel (h := h)]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
⊢ A.indToCoind ∘ₗ A.coindToInd = LinearMap.id

Tactic:
ext g a

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑((A.indToCoind ∘ₗ A.coindToInd) g) a = ↑(LinearMap.id g) a
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
| ↑(A.indToCoind (A.coindToInd g)) a

Tactic:
coindToInd_apply

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
| ↑(A.indToCoind (∑ g_1, g_1.liftOn (fun g_2 ↦ (IndV.mk S.subtype A.ρ g_2) (↑g g_2)) ⋯)) a
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
⊢ A.coindToInd ∘ₗ A.indToCoind = LinearMap.id

Tactic:
ext g a

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ ((AlgebraTensorModule.curry
            ((A.coindToInd ∘ₗ A.indToCoind) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle g)
        1)
      a =
    ((AlgebraTensorModule.curry
            (LinearMap.id ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle g)
        1)
      a
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
⊢ (fun f ↦
        ofHom
          {
            toLinearMap :=
              Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                (TensorProduct.lift
                  (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)))
                ⋯,
            isIntertwining' := ⋯ })
      ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ }) f) =
    f

Tactic:
ext h a

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
h : H
a : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom
                  ((fun f ↦
                      ofHom
                        {
                          toLinearMap :=
                            Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                              (TensorProduct.lift
                                (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                                  ↑(MonoidAlgebra.coeffLinearEquiv k)))
                              ⋯,
                          isIntertwining' := ⋯ })
                    ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
                      f))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom f).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y / ↑y = x⁻¹
⊢ ↑y / g ↑y = x

Tactic:
rw [IsUnit.div_eq_iff y.isUnit] at hy

Goal state after:
case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y = x⁻¹ * ↑y
⊢ ↑y / g ↑y = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ ∀ (g h : G ⧸ S),
    Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
      ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

Tactic:
intro g h

Goal state after:
case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g h : G ⧸ S
⊢ Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
    ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
      Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e✝ e : σ ↪ τ
⊢ killComplFun e 1 = 1

Tactic:
by simpa using! killComplFun_monomial_embDomain 0 1

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
d : τ →₀ ℕ
x : σ
⊢ x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0} → x ∈ ⋃ i ∈ ↑d.support, f ⁻¹' {i}

Tactic:
contrapose; intro _ _; classical simp_all [coeff_X]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R

Tactic:
by
  refine UniqueFactorizationMonoid.of_exists_prime_factors fun a ha ↦ ?_
  have ha₂ := span_notMem_kaplanskySet ha H
  rw [mem_kaplanskySet_iff] at ha₂
  rcases nonempty_iff_ne_empty.2 ha₂ with ⟨x, hx, hx₂⟩
  obtain ⟨b, hb⟩ := mem_span_singleton'.1 hx
  rw [← hb, mul_comm] at hx₂
  have hsubset : closure {r : R | Prime r} ≤ closure {r : R | IsUnit r ∨ Prime r} :=
    closure_mono (by grind)
  have := divisor_closure_eq_closure _ _ (hsubset hx₂)
  clear ha ha₂ hx hb hx₂
  induction this using closure_induction with
  | mem z hz =>
      rcases hz with h | h
      · exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩
      · exact ⟨{z}, by simpa⟩
  | one => exact ⟨∅, by simp⟩
  | mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>
      obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ
        (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom =
    ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ LinearMap.id).toAddMonoidHom

Tactic:
ext g a

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (Multiplicative.toAdd
        (((AddMonoidHom.toMultiplicativeRight
                ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ
                    (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom).comp
            Abelianization.of)
          g))
      a =
    (Multiplicative.toAdd
        (((AddMonoidHom.toMultiplicativeRight
                ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ LinearMap.id).toAddMonoidHom).comp
            Abelianization.of)
          g))
      a
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case 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
⊢ IsAdic J

Tactic:
apply IsTopologicalAddGroup.ext

Goal state after:
case mpr.tg
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
⊢ IsTopologicalAddGroup R

case tg'
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
⊢ IsTopologicalAddGroup R

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
⊢ 𝓝 0 = 𝓝 0
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⟩
        exact ⟨n, trivial, h⟩

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ Quotient.out ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)) - (truncTotal n) p ∈
    MvPolynomial.idealOfVars σ R ^ n

Tactic:
nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]

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
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : (powSMulQuotInclusion I M ⋯ ⊤) (↑x i) = 0
⊢ ↑x i = ↑0 i

Tactic:
LinearMap.map_eq_zero_iff _ (powSMulQuotInclusion_injective ..)

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 : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑x i = 0
⊢ ↑x i = ↑0 i
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
⊢ mapCycles₁ (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapCycles₁ f φ ≫ mapCycles₁ g ψ

Tactic:
rw [← cyclesMap'_comp, ← mapShortComplexH1_comp]

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

Goal state before:
pp: case neg
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
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Tactic:
simp only [gaussNorm, hsupp_nonempty, ↓reduceDIte, one_pow, mul_one, contentIdeal, Ideal.span_le,
    Set.subset_def, SetLike.mem_coe, ← v.intAdicAbv_lt_one_iff hb]

Goal state after:
case neg
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
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1 ↔ ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case toIsPrime
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ p.IsPrime

Tactic:
refine (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩

Goal state after:
case toIsPrime
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ p ≠ ⊤
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ hI.dpow (n a✝) a * ∏ x ∈ s✝, hI.dpow (n x) a = ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a

Tactic:
hrec,

Goal state after:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ hI.dpow (n a✝) a * (↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a) =
    ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case inr
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = if n = 0 then 1 else 0

Tactic:
rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]

Goal state after:
case inr
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ dp R (n a✝) m * ∏ x ∈ s✝, dp R (n x) m = ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m

Tactic:
hrec,

Goal state after:
case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ dp R (n a✝) m * (↑(multinomial s✝ n) * dp R (s✝.sum n) m) =
    ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m