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

Goal state before:
pp: case inl
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : IsEmpty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
card_inv_mul_sum_char_mul_char_eq_finrank

Goal state after:
case inl
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : IsEmpty (σ.Equiv ρ)
⊢ ↑(finrank k (σ.IntertwiningMap ρ)) = if Nonempty (σ.Equiv ρ) then 1 else 0
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * ρ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
card_inv_mul_sum_char_mul_char_eq_finrank

Goal state after:
case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ ↑(finrank k (ρ.IntertwiningMap ρ)) = if Nonempty (σ.Equiv ρ) then 1 else 0
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_5.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ Integrable (⇑ψ ∘ X 0) μ

Tactic:
· exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

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
g g₁ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a g₁ = 0

Tactic:
simp [indToCoindAux, dif_neg 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
x✝¹ x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ + x✝) g)) ⋯ =
    ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝¹ g)) ⋯ +
      ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
simpa [← Finset.sum_add_distrib, TensorProduct.tmul_add] using
      Finset.sum_congr rfl fun z _ => Quotient.inductionOn z fun _ => by simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀.h
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 b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦a⟧
⊢ ↑(A.indToCoind (⟦b⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)

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

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c r) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * (-1) ^ ↑p)

Tactic:
by
  rw [← mul_one r, ← smul_eq_mul, ← MonoidAlgebra.smul_single, map_smul, d_of]
  simp [Finset.smul_sum]

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ = (f g)⁻¹

Tactic:
← mul_eq_one_iff_eq_inv,

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ * f g = 1
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:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₁₂_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₁.d₁₂_apply x,
        map_zero]

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

Tactic:
simp [he, LinearMap.comp_assoc]

Goal state after:
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✝ : Rep R G
Y✝ : Rep R G
m : ℤ
n : ℕ
hmn : m = -(↑n + 1)
inst✝ : NeZero n
X Y : Rep R G
f : X ⟶ Y
⊢ (tateCohomologyFunctor m).map f ≫ ((tateComplexConnectData Y).homologyIsoNeg n m hmn).hom =
    ((tateComplexConnectData X).homologyIsoNeg n m hmn).hom ≫ (groupHomology.functor R G n).map f

Tactic:
simp [tateCohomologyFunctor,
      CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ (hmn := hmn)]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ↥(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✝ : G ⧸ S
g : G
s : ↥S
⊢ x (g * (g⁻¹ * ↑s * g)) - (A.ρ g) ((A.ρ (g⁻¹ * ↑s * g)) y - y) - (A.ρ g) y + y = x g - (A.ρ g) y + y

Tactic:
simp [eq_sub_of_add_eq' (h1 g (g⁻¹ * s * g)).symm,
          h2 (g⁻¹ * s * g) (Subgroup.Normal.conj_mem' ‹_› _ s.2 _)]

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

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

Tactic:
by
  by_cases h : 0 ∈ B
  · rw [Set.insert_eq_of_mem h]
  · simp [image_leadingTerm_insert_zero]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
i : σ
⊢ (rename f) (X i) = X (f i)

Tactic:
by
  simpa using! rename_monomial f (single i 1) 1

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
⊢ d₂₁ A ≫ d₁₀ A = 0

Tactic:
ext x g
  simp [d₁₀, d₂₁, sum_add_index', sum_sub_index, sub_sub_sub_comm, add_sub_add_comm]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = (↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h) ∘ₗ ↑e'.symm

Tactic:
simp [he, LinearMap.comp_assoc]

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 : ℕ
⊢ restrictScalars R (ofPowSMul I M n).range = (eval I M n).ker

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : x ∈ restrictScalars R (ofPowSMul I M n).range
⊢ x ∈ (eval I M n).ker

case refine_2
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : x ∈ (eval I M n).ker
⊢ x ∈ restrictScalars R (ofPowSMul I M n).range
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
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)
⊢ ∃ a, (ConcreteCategory.hom (H1CoresCoinf A S).g) a = (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x

Tactic:
rcases chains₁ToCoinvariantsKer_surjective
    (res S.subtype A) ⟨d₁₀ A Y, this⟩ with ⟨(Z : S →₀ A), hZ⟩

Goal state after:
case h
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⟩
⊢ ∃ a, (ConcreteCategory.hom (H1CoresCoinf A S).g) a = (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x
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 LinearMap.id)
          ((map (↑(opLinearEquiv R).symm) LinearMap.id)
            ((map ↑(opLinearEquiv R) ↑(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:
map_map,

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_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
left✝ : n ∈ (p * q).support
⊢ (p * q).coeff n ∈ ↑(p.contentIdeal * q.contentIdeal)

Tactic:
simp [coeff_mul, _root_.sum_mem, Submodule.mul_mem_mul, coeff_mem_contentIdeal]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)

Tactic:
intro (h : Function.Injective (DistribSMul.toLinearMap R M r))
  rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h,
    ← LinearMap.lsmul_eq_distribSMultoLinearMap,
    map_comap_eq, LinearMap.range_eq_map]; rfl

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker

Tactic:
rintro ⟨x, hx⟩
    rw [← hx]
    exact Subtype.mk_eq_mk.mpr <| (QuotientGroup.eq_one_iff _).mpr ⟨Units.map (algebraMap R K) x,
      by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩

Goal state after:
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
n : ℕ
x y : M
⊢ ↑(X (n, x + y)) = ∑ k ∈ antidiagonal n, ↑(X (k.1, x)) * ↑(X (k.2, y))

Tactic:
← RingCon.coe_mul,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ↑(X (n, x + y)) = ∑ k ∈ antidiagonal n, ↑(X (k.1, x) * X (k.2, y))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map f (AddSubgroup.map ((toAddMonoidEnd R M) r) ⊤) ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
map_map,

Goal state after:
case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map (f.comp ((toAddMonoidEnd R M) r)) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hx : x✝ ∉ J
⊢ e (hI.dpow n✝ (e.symm x✝)) = 0

Tactic:
by
    rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]
    rwa [symm_apply_mem_of_equiv_iff, h]

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

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
⊢ hJ.IsDPMorphism hK g

Tactic:
by
  apply on_span _ _ heq
  · rintro b ⟨a, ha, rfl⟩
    rw [← RingHom.comp_apply]
    exact hh.1 (mem_map_of_mem _ ha)
  · rintro n b ⟨a, ha, rfl⟩
    rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]

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

Goal state before:
pp: case nil
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) []

Tactic:
| nil N =>

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

Goal state before:
pp: case nil
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsWeaklyRegular (N ⊗[R] M₂) []

Tactic:
| nil N =>

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹

Tactic:
have hlt : (padicValNat p n.factorial : ℤ) < n := by
      exact_mod_cast padicValNat_factorial_lt_of_ne_zero p hn

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ ↑((dividedPowers p).dpow n x) = if x_1 : x ∈ Ideal.span {↑p} then (↑n !)⁻¹ʳ * ↑x ^ n else 0

Tactic:
simp only [dividedPowers_eq, dpow', inverse_eq_inv', dite_eq_ite]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ ↑(if hx : x ∈ Ideal.span {↑p} then ⟨(↑n !)⁻¹ * ↑x ^ n, ⋯⟩ else 0) =
    if x ∈ Ideal.span {↑p} then (↑n !)⁻¹ * ↑x ^ n else 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
x : R[ε]
⊢ IsNilpotent x ↔ ε ∣ x

Tactic:
by
  simp only [isNilpotent_iff_isNilpotent_fst, isNilpotent_iff_eq_zero, fst_eq_zero_iff_eps_dvd]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
⊢ x ∈ I → ε ∣ x

Tactic:
hxI

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
⊢ ε ∣ x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
x : K[ε]
⊢ x ∈ I → x ≠ 0 → ∃ r, ε = r * x

Tactic:
hxI

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
x : K[ε]
hxI : x ∈ I
⊢ x ≠ 0 → ∃ r, ε = r * x
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
L : Type u_8
inst✝³ : AddCommGroup L
inst✝² : Module R L
inst✝¹ : Module.Finite R L
inst✝ : Nontrivial L
x : R
mem : x ∈ maximalIdeal R
⊢ Nontrivial (QuotSMulTop x L)

Tactic:
apply Submodule.Quotient.nontrivial_iff.mpr (Ne.symm _)

Goal state after:
R : Type u_7
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
L : Type u_8
inst✝³ : AddCommGroup L
inst✝² : Module R L
inst✝¹ : Module.Finite R L
inst✝ : Nontrivial L
x : R
mem : x ∈ maximalIdeal R
⊢ ⊤ ≠ x • ⊤
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑S h1Cotangentι ∘ₗ H1Cotangent.map P.toExtendScalars) ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)

Tactic:
LinearMap.restrictScalars_self,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (h1Cotangentι ∘ₗ H1Cotangent.map P.toExtendScalars) ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x x✝ : A
hx : x✝ ∈ s
i : ι
⊢ ↑(((decompose 𝒜) x✝) i) ∈ Subsemiring.closure s

Tactic:
exact Subsemiring.subset_closure <| h i hx

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
⊢ (HahnModule.of R).symm (x • (HahnModule.of R) s.hsum) = x * s.hsum

Tactic:
of_symm_smul_of_eq_mul

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
⊢ x * s.hsum = x * s.hsum
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
⊢ (ofFinsupp f).hsum = f.sum fun x ↦ id

Tactic:
ext g
  simp only [coeff_hsum, coe_ofFinsupp, Finsupp.sum]
  simp_rw [← coeff.addMonoidHom_apply, id]
  rw [map_sum, finsum_eq_sum_of_support_subset]
  intro x h
  simp only [mem_coe, Finsupp.mem_support_iff, Ne]
  contrapose h
  simp [h]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ (antipode R) (C a) = C ((antipode R) a)

Tactic:
by
  rw [← single_eq_C, AddMonoidAlgebra.antipode_single]
  simp

Goal state after: