mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ (↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv) ∘SL ρ g =
    τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv

Tactic:
comp_assoc,

Goal state after:
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
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv ∘SL ρ g =
    τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: 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
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ (Hom.hom (X.d (0 + 1))) ↑⟨ContinuousMap.const G x, h⟩ = ↑0

Tactic:
simp [d_succ, hom_sub, ContIntertwiningMap.sub_apply, d_zero]

Goal state after:
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:
dsimp
  ext1
  simpa using! (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm

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

Goal state before:
pp: case refine_1
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
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
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) η
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
h : IsLocalization.mk' L 0 b = ↑ε
this : t • IsLocalization.mk' L 0 b = (algebraMap B L) 0
⊢ False
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ˣ
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
hε : (algebraMap B L) η * g (IsLocalization.mk' L a b) = IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a

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

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ coboundaries₁ A = ⊥

Tactic:
simp_rw [coboundaries₁, d₀₁_eq_zero]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (ModuleCat.Hom.hom 0).range = ⊥
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

Tactic:
rw [Set.insert_eq_of_mem h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P

Tactic:
obtain ⟨P, hP⟩ := zorn_le₀ (kaplanskySet S) (fun _ ↦ exists_mem_kaplanskySet_le hS)
  exact ⟨P, hP.1, fun _ hI H ↦ le_antisymm (hP.2 hI H) H⟩

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✝
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
hx : IsBoundary₀ G x
⊢ x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)

Tactic:
rcases (isBoundary₀_iff G x).1 hx with ⟨y, rfl⟩
    exact Submodule.finsuppSum_mem _ _ _ _ fun g _ => Coinvariants.mem_ker_of_eq g (y g) _ rfl

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

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

Tactic:
ext; simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

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

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

Tactic:
ext; simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

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

Goal state before:
pp: case intro
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n : ℕ
S : Type u_3
inst✝² : CommRing S
inst✝¹ : IsNoetherianRing S
inst✝ : Finite σ
val✝ : Fintype σ
⊢ IsNoetherianRing (MvPowerSeries σ S)

Tactic:
have := isNoetherianRing_fin S (Fintype.card σ)

Goal state after:
case intro
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n : ℕ
S : Type u_3
inst✝² : CommRing S
inst✝¹ : IsNoetherianRing S
inst✝ : Finite σ
val✝ : Fintype σ
this : IsNoetherianRing (MvPowerSeries (Fin (Fintype.card σ)) S)
⊢ IsNoetherianRing (MvPowerSeries σ S)
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
by simpa [SModEq.zero] using hx

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

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
inst✝³ : IsNoetherianRing R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
by simpa [SModEq.zero] using hx

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

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∑ᶠ (d_1 : ℕ), (coeff d_1) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ d_1) = 0

Tactic:
finsum_eq_zero_of_forall_eq_zero

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ 0 = 0

σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), (coeff x) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ x) = 0
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
x : S
hx : IsAlgebraic ℤ x
⊢ (Algebra.denominator ℤ x).natAbs ≠ 0

Tactic:
Int.natAbs_ne_zero

Goal state after:
S : Type u_2
inst✝ : CommRing S
x : S
hx : IsAlgebraic ℤ x
⊢ Algebra.denominator ℤ x ≠ 0
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
a : A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R 0
⊢ False
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 : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
this : (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
Z : ↥S →₀ ↑A
hZ : (ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) Z = ⟨(ConcreteCategory.hom (d₁₀ A)) Y, this⟩
⊢ (ConcreteCategory.hom (d₁₀ A)) (Y - mapDomain (⇑S.subtype) Z) = 0

Tactic:
simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, -LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using! Subtype.ext_iff.1 hZ.symm

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) LinearMap.id))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ)
        ((map (comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R))
            (LinearMap.id ∘ₗ LinearMap.id ∘ₗ ↑(opLinearEquiv R)))
          (comul ((opLinearEquiv R).symm x✝)))) =
    (map (↑(opLinearEquiv R))
        ((map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ ↑(opLinearEquiv R)))
      (comul ((opLinearEquiv R).symm x✝))

Tactic:
comp_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) LinearMap.id))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ)
        ((map (comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R))
            (LinearMap.id ∘ₗ LinearMap.id ∘ₗ ↑(opLinearEquiv R)))
          (comul ((opLinearEquiv R).symm x✝)))) =
    (map (↑(opLinearEquiv R))
        (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
      (comul ((opLinearEquiv R).symm x✝))
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : p.coeff n ∈ p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
Submodule.IsPrincipal.mem_iff_eq_smul_generator

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : ∃ s, p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal = ⊤

Tactic:
rw [← Ideal.radical_eq_top]
  apply le_antisymm le_top
  calc
    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
⊢ x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)

Tactic:
simpa using this.notMem_span_of_insert h

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ single ((mapDomainOfBialgHom f) g) (r • 1) = f (single g (r • 1))

Tactic:
← smul_single,

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = f (single g (r • 1))
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = f (single g (r • 1))

Tactic:
← smul_single,

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = f (r • single g 1)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * x✝ = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if x✝ = 0 ∧ n = 0 then 1 else 0

Tactic:
mem_bot.mp hx

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * 0 = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if 0 = 0 ∧ n = 0 then 1 else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
⊢ ((if x = 0 ∧ m = 0 then 1 else 0) * if x = 0 ∧ n = 0 then 1 else 0) =
    ↑((m + n).choose m) * if x = 0 ∧ m + n = 0 then 1 else 0

Tactic:
mem_bot.mp hx

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
⊢ ((if 0 = 0 ∧ m = 0 then 1 else 0) * if 0 = 0 ∧ n = 0 then 1 else 0) =
    ↑((m + n).choose m) * if 0 = 0 ∧ m + n = 0 then 1 else 0
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case H
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
hx :
  maximalIdeal (Localization.AtPrime p) = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective ⇑i
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np : Nₚ
⊢ to_res np = 0

Tactic:
apply inj1

Goal state after:
case H
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := ⋯
p' : PrimeSpectrum R := ⋯
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := ⋯
Nₚ : Type (max u_1 u_3) := ⋯
Mₚ : Type (max u_1 u_2) := ⋯
Nₚ' : Type (max u_1 u_3) := ⋯
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := ⋯
x✝ : Module p.ResidueField Nₚ' := ⋯
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField := ⋯
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := ⋯
hx :
  maximalIdeal (Localization.AtPrime p) = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker
i : p.ResidueField →ₗ[Rₚ] Mₚ := ⋯
inj1 : Function.Injective ⇑i
f : Nₚ →ₗ[Rₚ] Mₚ := ⋯
eq0 : f = 0
np : Nₚ
⊢ i (to_res np) = i 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
⊢ P f

Tactic:
induction f using Quot.induction_on with

Goal state after:
case h
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial (ℕ × M) R
⊢ P (Quot.mk (⇑(ringCon R M).toSetoid) F)
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]
    rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
⊢ dpow n ((insert a s).sum x) = ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
| insert a s ha ih =>

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₁ : rs₀ ++ b :: a :: t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) ([b, a] ++ t)
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) ([a, b] ++ t)

Tactic:
isWeaklyRegular_append_iff

Goal state after:
case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₁ : rs₀ ++ b :: a :: t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [b, a] • ⊤) t
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m.uniformBell k * k ! ^ m * m !) = ↑k ! ^ m * (↑m ! * ↑(m.uniformBell k))

Tactic:
push_cast

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m.uniformBell k) * ↑k ! ^ m * ↑m ! = ↑k ! ^ m * (↑m ! * ↑(m.uniformBell k))