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 σ
g : G
⊢ ↑φ.symm ∘SL σ g = ρ g ∘SL ↑φ.symm

Tactic:
← cancel_left' (g := φ.toContinuousLinearEquiv.toContinuousLinearMap)
    φ.toContinuousLinearEquiv.injective,

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 σ
g : G
⊢ ↑φ.toContinuousLinearEquiv ∘SL ↑φ.symm ∘SL σ g = ↑φ.toContinuousLinearEquiv ∘SL ρ g ∘SL ↑φ.symm
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.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (X.d 1)) ↑σ = ↑0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
d_succ,

Goal state after:
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.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (ofHom (X.resolutionX (0 + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d 0))) ↑σ = ↑0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
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
⊢ Hom.toModuleCatHom M.norm ≫ d₀₁ M = 0

Tactic:
by
  ext
  simp [Pi.zero_apply _]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
⊢ I.FG

Tactic:
by
    classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)

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
p : MvPolynomial σ R
⊢ (rename f) ↑p = ↑((MvPolynomial.rename f) p)

Tactic:
by
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add P Q hP hQ => simp [hP, hQ]
  | mul_X P n hP => simp only [MvPolynomial.coe_mul, MvPolynomial.coe_X, map_mul, hP, rename_X,
    MvPolynomial.rename_X]

Goal state after:
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 0 = 0

Tactic:
by ext; simp [coeff_killComplFun]

Goal state after:
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 : σ ↪ τ
x✝¹ x✝ : MvPowerSeries τ R
⊢ killComplFun e (x✝¹ + x✝) = killComplFun e x✝¹ + killComplFun e x✝

Tactic:
by ext; simp [coeff_killComplFun]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst✝² : P.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
⊢ UniqueFactorizationMonoid R⟦X⟧

Tactic:
refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
⊢ ∃ x ∈ P, Prime x
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

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 : ℕ
this : TopologicalSpace R := I.adicTopology
⊢ IsOpen[I.adicTopology] (toAddSubgroup (I ^ n)).carrier

Tactic:
convert! (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen

Goal state after:
case e'_3
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := I.adicTopology
⊢ (toAddSubgroup (I ^ n)).carrier = ↑(⋯.openAddSubgroup n)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
n : ℕ
⊢ IsOpen[J.adicTopology] ↑(J ^ n)

Tactic:
exact (J.openAddSubgroup n).isOpen'

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := ⋯
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
· intro s hs
      simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
⊢ V ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V

Tactic:
hV

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1

Tactic:
by_cases! h : n = 0

Goal state after:
case pos
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n = 0
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1

case neg
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n ≠ 0
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (truncTotal n) (p * q) - (truncTotal n) p * (truncTotal n) q ∈ MvPolynomial.idealOfVars σ R ^ n

Tactic:
exact truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars p q

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n)) = (coeff x) p

Tactic:
by
  rw [← coeff_truncTotal _ hx, ← sub_eq_zero, ← MvPolynomial.coeff_sub]
  apply (MvPolynomial.mem_pow_idealOfVars_iff' n _).mp
  · rw [toAdicCompletion_apply_eq_mk_truncTotal, smul_eq_mul]
    nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]
  exact hx

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
x : A[M]
⊢ counit ((domCongr R A e) x) = counit x

Tactic:
induction x using MonoidAlgebra.induction_linear <;> simp [*]

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))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ x.coeff g • single g 1 ∈ span R (Set.range fun x ↦ single x 1)

Tactic:
exact smul_mem _ _ <| subset_span <| Set.mem_range_self _

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ Exact ⇑((map r) f₁) ⇑((map r) f₂)

Tactic:
dsimp [map, mapQLinear]

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ Exact ⇑((r • ⊤).mapQ (r • ⊤) f₁ ⋯) ⇑((r • ⊤).mapQ (r • ⊤) f₂ ⋯)
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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)
⊢ fromUnit.ker = (powMonoidHom n).range

Tactic:
ext ⟨_, _, _, _⟩

Goal state after:
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✝ } ∈ fromUnit.ker ↔
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range
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
a : R
⊢ ↑(C a) = (algebraMap R (DividedPowerAlgebra R M)) a

Tactic:
rw [← MvPolynomial.algebraMap_eq, RingCon.coe_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ ((Finsupp.single i k + n).prod fun i k ↦ dp R k (v i)) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)

Tactic:
← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))

Goal state after:
case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ (dp R ((Finsupp.single i k + n) i) (v i) * (Finsupp.erase i (Finsupp.single i k + n)).prod fun i k ↦ dp R k (v i)) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (∏ i ∈ insert a s, r i) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)

Tactic:
Finset.prod_insert has

Goal state after:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)

Tactic:
rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_sdiff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))

Goal state after:
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
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m x ∈ I

Tactic:
rw [dpow_eq_of_mem hx]

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ (↑m !)⁻¹ʳ * x ^ m ∈ I
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) rs₁ ∧ IsWeaklyRegular (QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤) rs₂ ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
← and_assoc,

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧
      IsWeaklyRegular (QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤) rs₂ ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ TrivSqZeroExt.fst x = 0 ∧ ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
iff_self_and

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 → ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
haux : ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ hI.dpow k z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
exact haux _ hk

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
⊢ x ∈ hI.dpEqualizer hI' ↔ x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x

Tactic:
by
  simp [dpEqualizer, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
    Set.mem_ofPred_eq]

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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
exact H.mk_apply x

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mul
ι : 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 y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i j : ι
x✝¹ : j ∈ DFinsupp.support ((decompose 𝒜) x)
k : ι
x✝ : k ∈ DFinsupp.support ((decompose 𝒜) y)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) (j + k)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) (((decompose 𝒜) y) k))) i) ∈
    Subsemiring.closure s

Tactic:
obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
i✝ : ι
x✝ : S ⊗[R] A
hx : x✝ ∈ baseChange S (𝒜 i✝)
⊢ ((AlgHom.liftEquiv R S A B) ↑f).toRingHom x✝ ∈ ℬ i✝

Tactic:
obtain ⟨x, rfl⟩ := toBaseChange_surjective' _ _ hx
        induction x with
        | zero => simp
        | add => simp_all [add_mem]
        | tmul r x => simpa using smul_mem _ _ <| by exact f.map_mem x.2

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
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₂]
⊢ subst ![subst ![f₀, f₁] F.toPowerSeries, f₂] F.toPowerSeries =
    subst ![f₀, f₁, f₂] (subst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] F.toPowerSeries)

Tactic:
by
      rw [subst_comp_subst_apply aux₁ this]
      congr! 2 with s
      fin_cases s
      · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue,
          Matrix.cons_val_zero, subst_comp_subst_apply HasSubst.X_X this]
        congr! 2 with s
        fin_cases s <;> simp [subst_X this]
      · simp [subst_X this]

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

Goal state before:
pp: case pos.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi : i ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal
⊢ i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset →
    ((PowerSeries.coeff i.snd.1) a * (PowerSeries.coeff i.snd.2) b) • (x ^ i.fst).coeff g = 0

Tactic:
his

Goal state after:
case pos.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi : i ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
⊢ ((PowerSeries.coeff i.snd.1) a * (PowerSeries.coeff i.snd.2) b) • (x ^ i.fst).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (powerSeriesFamily x 0).hsum = 0

Tactic:
by
    simp only [hsum, smulFamily_toFun, map_zero, zero_smul,
      coeff_zero, finsum_zero, mk_eq_zero, Pi.zero_def]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
by
  grw [← lift_uzero (cardSupp _), ← sum_pow_le_max_aleph0, cardSupp_hsum_le, sum_le_sum]
  intro i
  rw [SummableFamily.powers_toFun]
  split_ifs
  · exact cardSupp_pow_le ..
  · cases i <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
F : IdealFilter A
inst✝ : F.IsUniform
I : Ideal A
hI : I ∈ F
⊢ ∃ V ∈ F.addGroupFilterBasis.sets, V * V ⊆ ↑I

Tactic:
exact ⟨I, ⟨I, hI, rfl⟩, Set.mul_subset_iff.mpr fun _ h₁ _ h₂ ↦ mul_mem h₁ h₂⟩

Goal state after: