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 X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
g : G
⊢ ModuleCat.Hom.hom
      ({ V := ModuleCat.of k ↑X✝, ρ := (ModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp X✝.ρ }.ρ g ≫
        Hom.toModuleCatHom f) =
    ModuleCat.Hom.hom
      (Hom.toModuleCatHom f ≫
        { V := ModuleCat.of k ↑Y✝, ρ := (ModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp Y✝.ρ }.ρ g)

Tactic:
simp [ModuleCat.endRingEquiv, f.hom.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 X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ f = default

Tactic:
ext x; have : x = 0 := Subsingleton.elim _ _; subst this; simp

Goal state after:
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
⊢ ∀ {X : Rep k G} {Y Y' : Rep k H} (f : (indFunctor k φ).obj X ⟶ Y) (g : Y ⟶ Y'),
    (indResHomEquiv φ X Y').toEquiv (f ≫ g) = (indResHomEquiv φ X Y).toEquiv f ≫ (resFunctor φ).map g

Tactic:
intros; rfl

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

Goal state before:
pp: 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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
have : Module.IsTorsionFree A L := by
    rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)

Goal state after:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_1
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
⊢ ↑x g - (A.ρ g) y + y ∈ invariants (MonoidHom.comp A.ρ S.subtype)

Tactic:
intro s
    calc
      _ = x (s * g) - x s - A.ρ s (A.ρ g y) + (x s + y) := by
        simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]
      _ = x (g * (g⁻¹ * s * g)) - A.ρ g (A.ρ (g⁻¹ * s * g) y - y) - A.ρ g y + y := by
        simp only [mul_assoc, mul_inv_cancel_left, map_mul, Module.End.mul_apply, map_sub,
          Representation.self_inv_apply]
        abel
      _ = x g - A.ρ g y + y := by
        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.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3.H.H
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
⊢ 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:
apply Subtype.ext
    simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
⊢ ∀ (X Y : FDRep k G),
    Functor.LaxMonoidal.μ (forget k G).toFunctor X Y ≫ (equivApp g (X ⊗ Y)).hom =
      ((equivApp g X).hom ⊗ₘ (equivApp g Y).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X Y

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝¹ : G
f : ↑rightFDRep.V.obj
x✝ : G
⊢ s⁻¹ * x✝ * x✝¹ = s⁻¹ * (x✝ * x✝¹)

Tactic:
exact mul_assoc ..

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

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

Tactic:
exact ⟨⊥, by simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]⟩

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
a : A
ha : a ∈ MulAction.fixedPoints G A
⊢ IsCycle₁ (single g a)

Tactic:
by
  simp_all [IsCycle₁]

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
⊢ π A 1 ≫ (H1Iso A).hom = (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
by
  simp [H1Iso, isoCycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R

Tactic:
rw [iff_comm, IsAdic.isPrecomplete_iff (by rfl), IsAdic.isPrecomplete_iff (by rfl)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ CompleteSpace R ↔ CompleteSpace S
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 σ
⊢ IsAdicComplete (Ideal.span (Set.range X)) (MvPowerSeries σ R)

Tactic:
by
  have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    (MvPolynomial.idealOfVars σ R).map (algebraMap ..) := by
    simp_rw [Ideal.map_span, ← Set.range_comp]
    congr 2; ext1
    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]
  rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
    IsAdicComplete.map_algebraMap_iff]
  exact AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)

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

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).toLinearMap ∘ₗ
      map (map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ comul)
          ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
        comul =
    map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap)
        (map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ comul) ∘ₗ
      comul

Tactic:
simp [coassoc_simps]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ comul 1 = 1

Tactic:
by
    simp only [one_def, comul_single, Bialgebra.comul_one, Algebra.TensorProduct.one_def,
      TensorProduct.map_tmul, lsingle_apply]

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 : ℕ
x : ↑(ModuleCat.of k (G × G →₀ ↑A))
x✝ : x ∈ cycles₂ A
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ)) x ∈ cycles₂ B

Tactic:
by
      have := congr($((mapShortComplexH2 f φ).comm₂₃) x); simp_all [cycles₂, shortComplexH2]

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1).choose 1) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
← choose_symm_add,

Goal state after:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1).choose n) * hI.dpow (n + 1) a = a ^ (n + 1)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_7
inst✝² : CommSemiring R
r : R
rs : List R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ofList (r :: rs) • N = r • N ⊔ ofList rs • N

Tactic:
by
  rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]

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

Goal state before:
pp: case a
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
h : ∀ (x : M), f (r • x) = s • f x
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
| AddSubgroup.map f ((Ideal.span {r} • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)

Tactic:
ideal_span_singleton_smul,

Goal state after:
case a
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
h : ∀ (x : M), f (r • x) = s • f x
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
| AddSubgroup.map f ((r • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
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
h : ∀ (x : M), f (r • x) = s • f x
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
| (Ideal.span {s} • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
ideal_span_singleton_smul,

Goal state after:
case a
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
h : ∀ (x : M), f (r • x) = s • f x
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
| (s • ⊤).toAddSubgroup ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
x✝ : A
⊢ toRingHom✝¹ x✝ = toRingHom✝ x✝

Tactic:
rw [hh']

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

Goal state before:
pp: 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 : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
| Multiset.count i ↑m

Tactic:
← m.fill_filterNe a

Goal state after:
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 : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
| Multiset.count i ↑(Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: 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 : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
| Multiset.count i ↑m

Tactic:
rw [← m.fill_filterNe a]

Goal state after:
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 : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
| Multiset.count i ↑(Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ Ideal.span {r} • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []

Tactic:
ideal_span_singleton_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
hax : a * x ∈ I
⊢ (if hx : a * x ∈ I then ⋯.choose else 0) = a ^ n * if hx : x ∈ I then ⋯.choose else 0

Tactic:
simpa only [(Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2, dif_pos hax, dif_pos hx,
    ← hf.eq_iff, map_mul, map_pow] using hJ.dpow_mul (hIJ ▸ I.mem_map_of_mem f hx)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ hI.dpow x✝ x ∈ ⊥

Tactic:
by rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

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

Tactic:
· intro hx
    obtain ⟨p, rfl⟩ := hx
    obtain ⟨y, hyI, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb
    obtain ⟨r, hr⟩ := hd' _ hyI hy0
    rw [(commute_eps_left _).eq, hr, ← mul_assoc]
    exact Ideal.mul_mem_left _ _ hyI

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
⊢ Submodule.IsPrincipal I

Tactic:
by
    rcases ideal_trichotomy I with rfl | rfl | rfl
    · exact bot_isPrincipal
    · exact ⟨_, rfl⟩
    · exact top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale R S
inst✝ : WeaklyEtale S T
⊢ WeaklyEtale R T

Tactic:
by
  rw [← ulift_iff.{max u₁ u₂ u₃, max u₁ u₂ u₃}] at *
  refine ⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩
  · have heq : TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T) (ULift R) =
        AlgHom.comp ((TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T)
          (ULift.{max u₁ u₂ u₃} S)).restrictScalars (ULift.{max u₁ u₂ u₃} R))
          (TensorProduct.mapOfCompatibleSMul ..) := by
      ext <;> simp
    rw [heq]
    refine .comp ?_ ?_
    · exact (flat_lmul' (ULift R) (ULift S)).mapOfCompatibleSMul
        (ULift.{max u₁ u₂ u₃} T) (ULift.{max u₁ u₂ u₃} T)
    · exact WeaklyEtale.flat_lmul' (ULift S) (ULift T)

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝ : Algebra.IsIntegral R S
this : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this : Finite (R ⧸ P)
⊢ ∃ σ, IsArithFrobAt R σ Q
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
s : Fin (Nat.succ 1)
⊢ ![f₀, f₁] s = subst ![f₀, f₁, f₂] (![Y₀, Y₁] s)

Tactic:
fin_cases s <;> simp [subst_X this]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯) ^ (d + 1) * ↑(invOneSubPow S (d + 1)) = 1

Tactic:
exact (invOneSubPow S (d + 1)).inv_val

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] F.toPowerSeries = subst ![g, f] F.toPowerSeries

Tactic:
by
  nth_rw 1 [IsComm.comm]
  rw [subst_comp_subst_apply HasSubst.X_X <| hasSubst_of_constantCoeff_nilpotent (by simp [hf, hg])]
  congr! 2 with s
  fin_cases s <;> simp [subst]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
⊢ (Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset

Tactic:
by
  intro _ hab
  simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod,
    Set.mem_ofPred_eq]
  exact ⟨left_ne_zero_of_smul hab, right_ne_zero_of_smul hab⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ PowerSeries.subst F.Xzero F.Xzero = subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

Tactic:
PowerSeries.subst,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ F.Xzero) F.Xzero = subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries