mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span (m.leadingTerm '' B) = span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)

Tactic:
apply le_antisymm

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span (m.leadingTerm '' B) ≤ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)

case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B) ≤ span (m.leadingTerm '' B)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
⊢ ModuleCat.Hom.hom ((chainsMap (MonoidHom.id G) φ).f i) = mapRange.linearMap (Hom.hom φ).toLinearMap

Tactic:
refine lhom_ext fun _ _ => ?_
  simp [chainsMap_f, MonoidHom.coe_id]

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ restrictScalars R (ofPowSMul I M n).range ≤ restrictScalars R (⇑(algebraMap R (AdicCompletion I R)) '' ↑s • ⊤)

Tactic:
restrictScalars_le,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤ ⇑(algebraMap R (AdicCompletion I R)) '' ↑s • ⊤
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
ha : IsGroupLikeElem R a
⊢ ∀ ⦃a₂ : GroupLike R A⦄, ↑{ val := a, isGroupLikeElem_val := ha } = ↑a₂ → { val := a, isGroupLikeElem_val := ha } = a₂

Tactic:
congr!

Goal state after:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    ⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
        ↑(finsuppTensorFinsupp' R ι κ).symm)

Tactic:
congr!

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ (Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      ↑(finsuppTensorFinsupp' R ι κ).symm
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map counit I.mkQ ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

Tactic:
rw [CoassocSimps.map_counit_comp_comul_left]; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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
⊢ Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom
          ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range =
    ⊤

Tactic:
eq_top_iff

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ⊤ ≤
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_2
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
⊢ map counit ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ comul =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
rw [CoassocSimps.map_counit_comp_comul_left]; rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
by_cases h : p.coeff n = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ ↑(span {p.content})

Tactic:
Finset.mem_coe,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : a✝ ∈ p.coeffs
⊢ a✝ ∈ ↑(span {p.content})
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
⊢ (annihilator R M).minimalPrimes ⊆ associatedPrimes R M

Tactic:
intro p hp
  have prime := hp.isPrime
  let Rₚ := Localization.AtPrime p
  have : Nontrivial (LocalizedModule p.primeCompl M) := by
    simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using! hp.1.2
  rcases associatedPrimes.nonempty Rₚ (LocalizedModule p.primeCompl M) with ⟨q, hq⟩
  have q_prime : q.IsPrime := IsAssociatedPrime.isPrime hq
  simp only [← preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule p.primeCompl
    Rₚ (LocalizedModule.mkLinearMap p.primeCompl M), Set.mem_preimage] at hq
  have ann_le : Module.annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q :=
    le_of_eq_of_le Submodule.annihilator_top.symm (IsAssociatedPrime.annihilator_le hq)
  have le : Ideal.comap (algebraMap R Rₚ) q ≤ p := by
    have := (IsLocalization.disjoint_under_iff p.primeCompl Rₚ q).mpr q_prime.ne_top
    simpa only [Ideal.primeCompl, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      Set.disjoint_compl_left_iff_subset] using! this
  simpa [Minimal.eq_of_le hp.out ⟨IsAssociatedPrime.isPrime hq, ann_le⟩ le] using! hq

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (b • a) = b ^ n • hI.dpow n a

Tactic:
simp only [smul_eq_mul, hI.dpow_mul, ha]

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

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow n (x + y)

Tactic:
hJ.dpow_add (mul_le_right hx) (mul_le_right hy)

Goal state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y = ∑ k ∈ antidiagonal n, hJ.dpow k.1 x * hJ.dpow k.2 y
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
zero2 : IsZero (AddCommGrpCat.of (Ext N M (i + 1)))
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)

Tactic:
exact AddCommGrpCat.subsingleton_of_isZero <| ShortComplex.Exact.isZero_of_both_zeros
        ((Ext.covariant_sequence_exact₃' N (hx.pow k).smulShortComplex_shortExact) i (i + 1) rfl)
        (zero1.eq_zero_of_src _) (zero2.eq_zero_of_tgt _)

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

Goal state before:
pp: 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) = ⊤
⊢ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) = ⊤

Tactic:
eq_top_iff

Goal state after:
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) = ⊤
⊢ ⊤ ≤ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: 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
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M₂ ⊗[R] M) rs

Tactic:
by
  induction h with
  | nil N => exact nil R (M₂ ⊗[R] N)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Goal state after:
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)
x✝ : A
hx : x✝ ∈ I
⊢ (if hx : x✝ ∈ I then ⋯.choose else 0) = x✝

Tactic:
by
    simpa only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2]
      using hJ.dpow_one (hIJ ▸ Ideal.mem_map_of_mem f hx)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J

Tactic:
refine ⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩
  · have hab' : a - b ∈ I := I.sub_mem ha hb
    rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_add_one, sum_insert notMem_range_self,
      tsub_self, hI.dpow_zero hab', mul_one, add_sub_cancel_left]
    exact J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
      (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))
  · refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
    rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
    exact hIJ ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {Coe.ringHom ↑p} = ⊤

Tactic:
map_natCast

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} = ⊤
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
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ (dividedPowers hI2).dpow n a = 0

Tactic:
simp only [dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]
  intro ha
  rw [Ideal.pow_eq_zero_of_mem hI2 hn ha, mul_zero]

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
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : ∃ (_ : J ∈ (fun J ↦ J.carrier) '' S), a ∈ J
⊢ a ∈ ↑I

Tactic:
exists_prop

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : J ∈ (fun J ↦ J.carrier) '' S ∧ a ∈ J
⊢ a ∈ ↑I
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
⊢ CompleteLattice hI.SubDPIdeal

Tactic:
refine Function.Injective.completeLattice (fun J : SubDPIdeal hI ↦ (J : Set.Iic I))
    (fun J J' h ↦ by simpa only [SubDPIdeal.ext_iff, Subtype.mk.injEq] using h)
    .rfl .rfl (fun J J' ↦ by rfl) (fun J J' ↦ by rfl) (fun S ↦ ?_) (fun S ↦ ?_) rfl rfl

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⟨(sSup S).carrier, ⋯⟩ = ⨆ a ∈ S, ⟨a.carrier, ⋯⟩

case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⟨(sInf S).carrier, ⋯⟩ = ⨅ a ∈ S, ⟨a.carrier, ⋯⟩
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
inst✝² : IsSepClosed k
inst✝¹ : EssFiniteType k R
inst✝ : FormallyEtale k R
⊢ IsFiniteSplit k R

Tactic:
have := FormallyUnramified.finite_of_free k R

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
inst✝² : IsSepClosed k
inst✝¹ : EssFiniteType k R
inst✝ : FormallyEtale k R
this : Module.Finite k R
⊢ IsFiniteSplit k R
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ autoParam (Module.Flat R S) flat._autoParam ∧ (TensorProduct.lmul' (ULift.{u₁, u_1} R)).Flat ↔
    autoParam (Module.Flat R S) flat._autoParam ∧ (TensorProduct.lmul' R).Flat

Tactic:
congr!

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (TensorProduct.lmul' (ULift.{u₁, u_1} R)).Flat ↔ (TensorProduct.lmul' R).Flat
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
⊢ Function.Injective ⇑(map P.toExtendScalars)

Tactic:
rw [← LinearMap.ker_eq_bot, H1Cotangent.map, LinearMap.ker_restrict,
    ← cotangentExtendScalarsEquiv_symm_toLinearMap, LinearEquiv.ker,
    Submodule.comap_bot, Submodule.ker_subtype]

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
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier = span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
apply le_antisymm

Goal state after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal := ⋯
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal := ⋯
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)

Tactic:
map_natCast

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ (hI.dpow n✝ a)) = ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a)

Tactic:
hI.dpow_comp hn ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (↑(m✝.uniformBell n✝) * hI.dpow (m✝ * n✝) a) = ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a) = ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a)

Tactic:
map_natCast

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a) = ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a)
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)
⊢ ∑ i_1 ∈ DFinsupp.support ((decompose 𝒜) y),
      ↑(((of (fun i ↦ ↥(𝒜 i)) (j + i_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) (((decompose 𝒜) y) i_1))) i) ∈
    Subsemiring.closure s

Tactic:
refine sum_mem fun k _ ↦ ?_

Goal state after:
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
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case intro
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)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 := iterateFrobeniusEquiv (S ⧸ Q) p ↑k;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ : (Ideal.Quotient.stabilizerHom Q P G) σ = l
x : S
⊢ (Ideal.Quotient.mk Q) ((MulSemiringAction.toAlgHom R S ↑σ) x) =
    (Ideal.Quotient.mk Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case intro
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)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 := iterateFrobeniusEquiv (S ⧸ Q) p ↑k;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ : (Ideal.Quotient.stabilizerHom Q P G) σ = l
x : S
⊢ (Ideal.Quotient.mk Q) ((MulSemiringAction.toAlgHom R S ↑σ) x) =
    (Ideal.Quotient.mk Q) (x ^ Fintype.card (R ⧸ Ideal.under R Q))
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ (1 - X) ^ (d + e) * ↑(invOneSubPow S e) = (1 - X) ^ d

Tactic:
by
  simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]

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

Goal state before:
pp: case pos.refine_1
Γ : 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 : Γ
⊢ Set.MapsTo (fun x ↦ ⟨x.1 + x.2, x⟩) ↑⋯.toFinset
    ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)

Tactic:
intro ij hij
      simp only [coe_sigma, coe_image, Set.mem_sigma_iff, Set.mem_image, Prod.exists, mem_coe,
        HasAntidiagonal.mem_antidiagonal, and_true]
      use ij.1, ij.2
      simp_all

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✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ (¬∃ i, g ∈ (s i).support) → g ∉ Function.support fun g ↦ ∑ᶠ (i : α), (s i).coeff g

Tactic:
not_exists,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ (∀ (x : α), g ∉ (s x).support) → g ∉ Function.support fun g ↦ ∑ᶠ (i : α), (s i).coeff g